在函数类型中加上vs S.

Question

以下向量声明 cons

cons : a -> Vect n a -> Vect (n + 1) a
cons x xs = x :: xs

因错误而失败

Type mismatch between
                S n
        and
                plus n 1

而以下矢量append编译和工作

append : Vect n a -> Vect m a -> Vect (n + m) a
append xs ys = xs ++ ys

为什么plus第二种情况接受类型级别,而第一种情况不接受.有什么不同？

Answer 1

为什么会x :: xs : Vect (n + 1) a导致类型错误？

(+)由第一个参数的归纳定义,因此n + 1被卡住(因为n是一个卡住的表达式,在这种情况下是一个变量).

(::)用类型定义a -> Vect m a -> Vect (S m) a.

所以Idris需要解决统一问题n + 1 =? S m,因为你有一个卡住的术语而不是带有头部构造函数的表达式,这两件事情根本就不会统一.

1 + n另一方面,如果你曾写过,伊德里斯会将这种表达减少到S n并且统一会成功.

为什么xs ++ ys : Vect (n + m) a成功？

(++)用类型定义Vect p a -> Vect q a -> Vect (p + q) a.

假设xs : Vect n a和ys : Vect m a,你将不得不解决约束:

• Vect n a ?= Vect p a(xs是传递给的第一个参数(++))
• Vect m a ?= Vect q a(ys是传递给的第一个参数(++))
• Vect (n + m) a ?= Vect (p + q) a(xs ++ ys是结果append)

前两个约束导致n = p并m = q分别使第三个约束成立:一切都解决了.

考虑append : Vect n a -> Vect m a -> Vect (m + n) a.

请注意我(+)在这一个中如何交换这两个参数.那么你就会遇到类似于你的第一个问题的情况:经过一段时间的统一,你最终会得到一个约束m + n ?= n + m,即伊德里斯,不知道那(+)是可交换的,也无法解决.

解决方案？解决？

无论什么时候,使用与其类型中发生的计算相同的重复模式定义函数是非常方便的.实际上,在这种情况下,类型将通过函数定义的各个分支中的计算来简化.

如果不能,您可以rewrite证明两个事物是相等的(例如,n + 1 = S n对所有人而言n)来调整术语类型与预期类型之间的不匹配.即使这看起来比重构代码以使其具有不同的重复模式更方便,并且有时是必要的,但它通常是充满陷阱的路径的开始.