パラメータ化された型の同義語のインスタンスを宣言する

Question

私は、ベクトルに作用する一連の関数、つまりタイプ強制長のリストを持っています。私は、私はちょうどfoo :: NList v Integer => ...

（簡体字）クラスを書くことができます書くことが簡単に自分の型を作ることを試み、すなわちの代わりに、私は新しいクラスNListを宣言してい

foo :: (Fold Integer v, Map Integer Integer v v, ...) => ... 

を書いて

あなたが見ることができるように、私は（「アイテム」タイプとは別の「ベクター」タイプを維持する必要があり

class (Fold (v i) i 
     , Map i i (v i) (v i) 
     , Map i (Maybe i) (v i) (v (Maybe i)) 
    ) => NList v i 

すなわち：次のようになります私がMapのようなことをMaybeベクター上に行うことができるように、私はから別のをiと分離しています。

このように、vは* -> *、である必要があります。

しかし、私はそうのようなベクターを用いて、それをインスタンス化しようとすると：

instance NList Vec2 Integer 
instance NList Vec3 Integer 
... 

私は次のエラーを取得：今

Type synonym `Vec2' should have 1 argument, but has been given none 
In the instance declaration for `NList Vec2 Integer' 

が、私はプログラミングレベル型に非常に新しいです、私はこれを非常に後方に行っている可能性が高いことを理解しています。このような型同義語をインスタンス化することは可能ですか？どのタイプ・ウィザードにも、私の目標を達成するためのより良い方法の提案がありますか？

Answer 1

ここでの問題はVec2とVec3は、おそらくこのようなものとして宣言されていることである。

type Vec2 a = Vec (S (S Z)) a 
type Vec3 a = Vec (S (S (S Z))) a 

型シノニムは、彼らはタイプレベルのラムダ、につながる（様々な不可解な理由のために、部分的に適用することができませんインスタンスの解決と推論に関連するあらゆる種類の事件で大惨事 - あなたがtype Id a = aを定義してMonadのインスタンスにすることができると想像してください）。 はVec2を* -> *のフル・フロッダ型コンストラクタであるかのように使用することができないため、何かのインスタンスにすることはできません。つまり、Vec2をインスタンス化することはできません。実質的に完全にしか適用できないタイプレベルの「マクロ」です。

ただし、は部分アプリケーション自体として型シノニムを定義することができます。

type Vec2 = Vec (S (S Z)) 
type Vec3 = Vec (S (S (S Z))) 

は、これらはあなたのインスタンスが許可されることを除いて、等価です。あなたのVec3タイプが実際に

type Vec3 a = Cons a (Cons a (Cons a Nil))) 

または類似のように見える場合

、あなたは運の出ています。インスタンスを与える場合は、newtypeラッパーを使用する必要があります。（一方で、あなたは完全にあなたがインスタンスとしてVec3を使用することができ、代わりにNilとConsのインスタンスを与えることによって、これらのタイプに直接インスタンスを定義避けることができるはずです。）

なお、GHC 7.4の新しいとconstraint kinds、あなたは全く別のタイプを避け、単に制約同義語を定義することができます。

type NList v i = 
    (Fold (v i) i 
    , Map i i (v i) (v i) 
    , Map i (Maybe i) (v i) (v (Maybe i)) 
    ) 

限り、一般的にあなたのアプローチが行くように、それは基本的に正常に動作する必要があります。同じ一般的な考え方がパッケージで使用されています。膨大な数のクラスと大きなコンテキストは、エラーメッセージを非常に混乱させ、コンパイルを遅くする可能性がありますが、これはタイプレベルのハッカーの性質です。あなたはいつものGADTとして定義された基本Vecタイプを持っている場合は、：

data Vec n a where 
    Nil :: Vec Z a 
    Succ :: a -> Vec n a -> Vec (S n) a 

は、あなたが実際にまったく型クラスは必要ありません。これは、あなたが完全にコンテキストを排除できるようにする必要があり

data Proxy s = Proxy 

class Nat n where 
    natElim 
     :: ((n ~ Z) => r) 
     -> (forall m. (n ~ S m, Nat m) => Proxy m -> r) 
     -> Proxy n 
     -> r 

が、操作を定義します：それは他の方法で定義されていますが、それでも天然型レベルにparametrisedされている場合は、1とすべてのクラスを置き換えることができますベクトル上で少しトリッキーです。