在函数类型中加上 vs S

Question

下面vector的声明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

(+) 是通过对其 first 参数的归纳定义的，因此 n + 1 被卡住了（因为 n 是一个卡住的表达式，一个变量在这种情况下）。

(::) 定义为 a -> Vect m a -> Vect (S m) a.

类型

所以 Idris 需要解决统一问题 n + 1 =? S m 并且因为你有一个卡住的术语与一个带有 head 构造函数的表达式，所以这两件事根本不会统一。

另一方面，如果您写的是 1 + n，Idris 会将该表达式缩减为 S n，并且统一会成功。

(++) 定义为 Vect p a -> Vect q a -> Vect (p + q) a.

类型

在xs : Vect n a和ys : Vect m a的假设下，你将不得不解决约束：

前两个约束分别导致 n = p 和 m = q，这使得第三个约束成立：一切正常。

请注意我如何将这两个参数交换为 (+)。然后你会遇到类似于你的第一个问题的情况：经过一些统一，你最终会得到约束 m + n ?= n + m ，而 Idris 不知道 (+) 是可交换的，将无法解决。

只要有可能，使用与其类型中发生的计算相同的循环模式来定义函数会更加方便。事实上，在这种情况下，类型将通过函数定义的各个分支中的计算得到简化。

当你不能时，你可以rewrite证明两件事是平等的（例如 n + 1 = S n 对所有 n）来调整术语类型和预计一个。尽管这看起来比重构代码以具有不同的重复模式更方便，而且有时是必要的，但它通常是充满陷阱的路径的开始。

Plus vs S in a function type