为什么Idris的Refl有时不会打字？

Question

我正在阅读伊德里斯的书,我正在进行第一次证明练习.

通过练习证明same_lists,我能够像这样实现它,作为匹配Refl力量x和y统一:

total same_lists : {xs : List a} -> {ys : List a} ->
    x = y -> xs = ys -> x :: xs = y :: ys
same_lists Refl Refl = Refl

但是,当我试图以同样的方式证明其他东西时,我会遇到不匹配的问题.例如:

total allSame2 : (x, y : Nat) -> x = y -> S x = S y
allSame2 x y Refl = Refl

编译器说:

Type mismatch between
   y = y (Type of Refl)
and
   x = y (Expected type)

如果我在=显式或lambda 之后匹配大小写,它按预期工作:

total allSame2 : (x : Nat) -> (y : Nat) -> x = y -> S x = S y
allSame2 x y = \Refl => Refl

这有什么区别？

另一个有效的修改是隐含有问题的参数:

total allSame2 : {x : Nat} -> {y : Nat} -> x = y -> S x = S y
allSame2 Refl = Refl

Answer 1

我不知道所有的细节,但我可以给你一个粗略的想法.在Idris中,命名函数的参数列表是特殊的,因为它是依赖模式匹配的一部分.模式匹配时,它还会重写其他参数.

same_lists x y Refl = Refl我粗略猜测是无效的,因为Idris正在重写x并且y是相同的,并且你不允许给这个单一的值赋予不同的名字 - 我希望有人可以更好地解释这个机制.相反,您可以使用same_lists x x Refl = Refl- 并注意名称x并不重要,只是在两个站点中使用相同的名称.

lambda参数与命名参数列表分开.因此,由于您在lambda中进行匹配,因此Idris仅在此时重写其他参数.关键是,在第一个例子中,Idris希望一次完成所有操作,因为它是同一参数列表的一部分.

在最后一个示例中,唯一的变化是您没有为参数指定不同的名称.使用它也是有效的all_same _ _ Refl = Refl.当参数是隐式的时,Idris会为您正确填充它们.

最后你可以考虑same_lists = \x, y, Refl => Refl哪个也有效.这是因为Idris不会在未命名的参数列表(即lambda参数)中重写.