7

私のデータ型には常に少なくとも 2 つのパラメーターがあり、最後の 2 つのパラメーターは常にそれぞれ「q」と「m」です。

{-# 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

このプログラムはエラーになります

Could not deduce (bBase ~ D2 t0) (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 は Bar のパラメーターではなく、Bar のパラメーターにしたくないため、これは機能しません。

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 が型を分解する方法を教えてください。

ありがとう！

4

1 に答える 1

1

あなたが説明しb' :: * -> * -> *たことから、適用を制限したいタイプがありますb' t :: * -> *（すべての場合t）。

要約すると、型を分解する必要があります。これはb :: * -> *、型 application の結果であると想定されているものから開始する試みであるb = b' tか、開始点からではなく、「より適用された」型に制約を適用する必要があります。のb' :: * -> * -> *。

b型を分解することはできません。これは、型が「分解可能」であるかどうかをコンパイラが認識していないためです。実際、そうではないかもしれません。例えば、私はインスタンスを作成できますinstance Bar Maybeが、タイプといくつかのタイプMaybeに分解することはできません。b' :: * -> * -> *t :: *

代わりに type から始めb' :: * -> * -> *て、 の適用に関する制約をb'、変数が量化されるクラスの本体に移動できます。

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

D2あなたの例では、もう1つのしわがあります.q1とq2には、制約が必要なインスタンスなど、独自の制約がある場合がありIntegralます。ただし、すべてのインスタンスの制約をBar修正します (この場合は空の制約)。解決策は、インスタンスが独自の制約を指定できるようにする「制約種類の型ファミリ」を使用することです。q1q2

  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)

D2次に、インスタンスを作成できます。

   instance Bar (D2 t) where
      type Constr (D2 t) q = Integral q
      g (D2 q) = D2 $ fromIntegral q
于 2013-01-30T13:45:22.697 に答える