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

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 plus 交换性 是一个定理。这里是它的类型:

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

没有一般规则可以告诉您选择和应用哪个定理。当然，可以针对一些简单的情况进行一些启发式，例如 Nat 可交换性。但这也可能使其他一些情况难以理解。

你需要考虑的另一件事是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)

但很明显，为您需要的每种情况编写新的运算符是可怕的。因此，为了使您的第二个版本可编译，您应该在 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 和定理证明是如何工作的。如果您不了解某些内容，这是另一个问题的主题。但是您可以在教程中阅读相关内容(或等待本书发布 :)。