两个向量的串联 - 为什么长度不被视为可交换的？

Question

我正在和 Idris 一起玩，我遇到了一些让我有点困惑的事情：

以下类型检查：

conc : Vect n a -> Vect m a -> Vect (n+m) a
conc [] ys = ys
conc (x :: xs) ys = x :: (conc xs ys)

但这不是：

conc : Vect n a -> Vect m a -> Vect (m+n) a
conc [] ys = ys
conc (x :: xs) ys = x :: (conc xs ys)

出现以下错误：

When checking right hand side of conc with expected type
        Vect (m + 0) a

Type mismatch between
        Vect m a (Type of ys)
and
        Vect (plus m 0) a (Expected type)

Specifically:
        Type mismatch between
                m
        and
                plus m 0

等效于 xs++ys 类型检查，但 ys++xs 不检查，即使它们都匹配长度为 n+m 的类型定义。

这让我有点吃惊，因为加法是可交换的。我可以对函数签名做些什么（可能有约束吗？）来获得 xs++ys 和 ys++xs 表达式类型检查？

Answer 1

这是 Idris 初学者经常混淆的话题。本例中第二个 conc 版本的问题：

conc : Vect n a -> Vect m a -> Vect (m+n) a
conc [] ys = ys

Idris 不能应用加法交换律，因为 Nat 加交换律 从编译器的角度来看是一个定理。这是它的类型：

Idris> :t plusCommutative 
plusCommutative : (left : Nat) -> (right : Nat) -> left + right = right + left

没有一般规则可以告诉您选择和应用哪个定理。当然，对于一些简单的情况可以做一些启发式的，比如Nat commutativity。但这也会使其他一些情况难以理解。

您需要考虑的另一件事是 plus:

的定义

Idris> :printdef plus 
plus : Nat -> Nat -> Nat
plus 0 right = right
plus (S left) right = S (plus left right)

函数 plus 以在第一个参数上进行模式匹配的方式定义。 Idris 实际上可以在类型中执行这种模式匹配。所以在第一个版本中，

conc : Vect n a -> Vect m a -> Vect (n+m) a
conc [] ys = ys

你的类型是 (0 + m) 并且 Idris 可以用 m 替换 plus 0 m 并且所有内容都会进行类型检查。如果您通过第二个参数的模式匹配来定义 + 运算符， plus m 0 将起作用。例如，这个编译：

infixl 4 +.
(+.) : Nat -> Nat -> Nat
n +. Z = n
n +. (S m) = S (n +. m)

conc : Vect n a -> Vect m a -> Vect (m +. n) a
conc [] ys = ys
conc (x :: xs) ys = x :: (conc xs ys)

但很明显，为您需要的每种情况编写 new 运算符是很糟糕的。因此，要使您的第二个版本可编译，您应该在 Idris 中使用 rewrite ... in 语法。你需要下一个定理：

Idris> :t plusZeroRightNeutral 
plusZeroRightNeutral : (left : Nat) -> left + 0 = left
Idris> :t plusSuccRightSucc 
plusSuccRightSucc : (left : Nat) -> (right : Nat) -> S (left + right) = left + S right
Idris> :t sym
sym : (left = right) -> right = left

这里是编译的版本：

conc : Vect n a -> Vect m a -> Vect (m + n) a
conc         {m} []        ys = rewrite plusZeroRightNeutral m        in ys
conc {n=S k} {m} (x :: xs) ys = rewrite (sym $ plusSuccRightSucc m k) in x :: (conc xs ys)

我不是在这里解释 rewriting 和定理证明是如何工作的。如果您不了解某些内容，这是另一个问题的主题。但是您可以在教程中阅读相关内容（或等待 The Book 发布 :)。

两个向量的串联 - 为什么长度不被视为可交换的？

Concatenation of two vectors - why are lengths not treated as commutative?

idris