タイプの脱構築

Question

私のデータ型は、常に、少なくとも2つのパラメータを持つことになりますし、最後の2つのパラメータはそれぞれ、「Q」と「M」は常にあります。エラー

Could not deduce (bBase ~ D2 t0) (LINE 1) 

で

{-# LANGUAGE TypeFamilies, FlexibleContexts, UndecidableInstances, TypeOperators, DataKinds, ConstraintKinds, FlexibleInstances #-} 

data D1 q m = D1 q 
data D2 t q m = D2 q 

class Foo a where -- a has kind * -> * 
    f :: a x -> a x 

class (Foo b) => Bar b where -- b has kind * -> * 
    -- the purpose of g is to change ONE type parameter, while fixing the rest 
    -- the intent of the equality constraints is to decompose the parameter b into 
    -- its base type and 'q' parameter, then use the same base type with a *different* 
    -- `q` parameter for the answer 
    g :: (b ~ bBase q1, b' ~ bBase q2) => b m -> b' m 

instance (Foo (D2 t q), Integral q) => Bar (D2 t q) where 
    g (D2 q) = D2 $ fromIntegral q -- LINE 1 

このプログラムの結果

私がインスタンスを書いたとき、私は確かにbBase ~ D2 tを意図しました。私はtが何とか結ばれていないと思うので（t0の導入）、GHCがこのタイプをまったく解体できないかどうかわかりません。あるいは、私はちょっとばかげたことをやっているかもしれません。

さらに、Barにパラメータをkind * - > * - > *にすると、この種の型の平等/型の解体は必要ありません。しかし、私はFooの制約を強制することができませんでした：

class (Foo (b q)) => Bar b where -- b has kind * -> * -> * 
    g :: b q m -> q b' -- this signature is now quite simple, and I would have no problem implementing it 

qはバーにパラメータではありませんので、これは動作しません、と私はがバーにパラメータににそれを望んでいません。

私は2つの余分な「ダミー」の関連タイプを使用して解決策を見つけたが、私は本当に周りにそれらを持つように私はそれらを必要としないしない場合：これは動作します

class (Foo b, b ~ (BBase b) (BMod b)) => Bar b where -- b has kind * -> * 
    type BBase b :: * -> * -> * 
    type BMod b :: * 

    g :: (Qux (BMod b), Qux q') => b m -> (BBase b) q' m 

instance (Foo (D2 t q), Integral q) => Bar (D2 t q) where 
    type BBase (D2 t q) = D2 t 
    type BMod (D2 t q) = q 

    g (D2 q) = D2 $ fromIntegral q 

、それが明示的になります単純な型のインスタンスがあれば、型を解体する必要はありません。

どちらのアプローチにも解決策を探しています：「より適用された」タイプのクラス制約を適用する方法を教えてください。あるいは、GHC解体型を作成する方法を教えてください。

ありがとうございます！

Answer 1

説明した内容から、適用されたb' t :: * -> *（すべてt）を拘束するタイプのb' :: * -> * -> *があります。

あなたがsummiseとして、あなたのどちらかがb :: * -> *から始まるここ あなたの試みであるタイプを、解体する必要はタイプ アプリケーションb = b' tの結果であると仮定し、または「より多くの適用」の制約を強制します代わりに、b' :: * -> * -> *の開始点から を入力します。

コンパイラは、bが "deconstructable"であるかどうかをコンパイラが知りませんので、型を分解することはできません。実際、例えばinstance Bar Maybeのインスタンスを作成することはできませんが、Maybeを分解してb' :: * -> * -> *のタイプとt :: *のタイプにすることはできません。タイプb' :: * -> * -> *から代わりに起動する

は、b'のアプリケーション上の制約は変数が定量化されているクラスの体内に移動することができます：あなたたとえば

class Bar (b :: * -> * -> *) where 
     g :: (Foo (b q1), Foo (b q2)) => b q1 m -> b q2 m 

つの更なるシワがあります： q1とq2にはそれぞれ独自の制約があります。 D2インスタンスの場合は、Integralという制約が必要です。ただし、Barは、すべてのインスタンス（この場合は空の制約）の制約をq1とq2に修正しています。

：次に、あなたの D2インスタンスを書くことができます

class Bar (b :: * -> * -> *) where 
     type Constr b t :: Constraint 
     g :: (Foo (b q1), Foo (b q2), Constr b q1, Constr b q2) => b q1 m -> b q2 m 

（{-# LANGUAGE ConstraintKinds #-}を含めるとGHC.Primをインポート）

：ソリューションは、インスタンスは、独自の制約を指定することができ、「制約kindedタイプファミリ」を使用することです

instance Bar (D2 t) where 
     type Constr (D2 t) q = Integral q 
     g (D2 q) = D2 $ fromIntegral q