连接两个向量 - 为什么长度不被视为可交换？

Question

我正在玩伊德里斯,我遇到了一些令我困惑的事:

以下类型检查:

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类型检查,但是即使它们都匹配长度为n + m的类型定义,ys ++ xs也不会.

这让我感到惊讶,因为添加是可交换的.有什么我可以做的(可能有约束？)函数签名,以获得xs ++ ys和ys ++ xs表达式类型检查？

Answer 1

这是伊德里斯初学者混淆的常见话题.在这种情况下第二个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交换性,可以进行一些启发式方法.但这也可能使其他一些案例难以理解.

您需要考虑的另一件事是定义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)型和伊德里斯可以代替plus 0 m用m一切typechecks.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和定理证明在这里工作.如果您不理解某些内容,这是另一个问题的主题.但是你可以在教程中阅读(或者等待The Book release :).