2016-11-05 4 views
3

私は、イドリスで簡単な依存ペアのSemigroupインターフェイスを実装しようとしている中に依存ペアのための半群が、これはコンパイルされません:エラー実装イドリス

Type mismatch between 
    ty 
and 
    Nat 

Semigroup (n ** Vect n f) where 
    (<+>) (_ ** xs) (_ ** ys) = (_ ** xs ++ ys) 

しかし、このコンパイル:

myPair:Type -> Type 
myPair f = (n ** Vect n f) 

Semigroup (myPair f) where 
    (<+>) (_ ** xs) (_ ** ys) = (_ ** xs ++ ys) 

なぜですか?これを達成する最良の方法は何ですか?

答えて

4

イドリスFAQ

あなたは小文字で始まるタイプに名前を使用し、これを任意の引数に適用されていない場合は、イドリスは暗黙的にバインド引数として扱います。問題を解決するための

一つのアプローチは、いくつかのシンタックスシュガーを取り除くと、明示的にこのようなnをバインドを取得するために、次のようになります。

Semigroup (DPair Nat (\n => Vect n f)) where 
    (<+>) = (_ ** xs) (_ ** ys) = (_ ** xs ++ ys) 

別のアプローチは、ベクトルの長さのために大文字を使用することです:ここでは

Semigroup (N ** Vect N f) where 
    (<+>) = (_ ** xs) (_ ** ys) = (_ ** xs ++ ys) 

NSemigroup実装にバインドされ、これはにDPair糖衣構文を許可されません。最初の変種と同様にNを蹴り込みます。

myPairの例は、例が上記の例のDPairと本質的に同等であるため、コンパイルします。砂糖を単に取り除くと、すべてがクリアになります:

myPair:Type -> Type 
myPair f = DPair Nat (\n => Vect n f)