idris - 函数类型中的 Plus 与 S

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 而第一种情况不接受。有什么不同？

最佳答案

为什么x :: xs : Vect (n + 1) a会导致类型错误？
(+) 由其第一个参数的归纳定义，因此 n + 1 被卡住(因为 n 是一个卡住的表达式，在这种情况下是一个变量)。
(::) 定义为 a -> Vect m a -> Vect (S m) a 类型。

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

另一方面，如果您编写了 1 + n，Idris 会将表达式简化为 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，Idris 不知道 (+) 是可交换的，因此无法解决该约束。

解决方案？变通？

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

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

关于idris - 函数类型中的 Plus 与 S，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/45744130/