2つのベクトルの連結 - なぜ長さは可換性として扱われないのですか？

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 ys ++ xsは長さn + mの型定義に一致するにもかかわらず、型チェックはしません。さらには可換であるよう

これは私を少し驚き。 xs ++ ysとys ++ xsの両方の式の型チェックを取得するために、関数のシグネチャに（おそらく制約がありますか？

Answer 1

これはイドリスで初心者のための混乱の共通の話題です。第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 commutativityのようなヒューリスティックを作成することもできます。しかし、これはまた、他のいくつかの場合を理解することを困難にする可能性があります。

あなたが考慮する必要がある他の事はplusの定義です：

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

パターンは、最初の引数に一致しないされ、このような方法で定義された関数plus。 Idrisは実際にタイプでこのパターンマッチングを実行できます。だから、最初にあなたがタイプで（0 + m）を持っている

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

バージョン、およびイドリスにm、すべてのtypechecksでplus 0 mを置き換えることができます。 plus m 0は、+演算子を第2引数のパターンマッチングで定義すると機能します。たとえば、これは次のようにコンパイルされます。

しかし、必要な場合に新しい演算子を書くことは恐ろしいことです。だから、第2版をコンパイルできるようにするには、rewrite ... inの構文をのIdrisに使うべきです。あなたは、次の定理が必要になります。

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と定理証明がここでどのように機能するかをここで説明していないよ：

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 

そしてここでは、コンパイルしたバージョンです。あなたが何かを理解していなければ、これは別の質問の話題です。しかし、チュートリアルでそれについて読むことができます（またはThe Book releaseを待つ:)。