兩個向量的連接 - 爲什麼長度不被視爲可交換的？

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 ++ y s類型檢查，但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> :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）可與m，一切typechecks更換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和定理證明在這裏工作。如果你不瞭解某些事情，這是另一個問題的話題。但是你可以在教程中閱讀（或者等待The Book版本:)。