7

ヴァイナルライブラリには型RecAllファミリがあります。型レベル リストのすべての型に対して、部分的に適用された制約が真であることを確認してみましょう。たとえば、次のように記述できます。

myShowFunc :: RecAll f rs Show => Rec f rs -> String

そして、それはすべて素敵です。ここで、が不明な制約RecAll f rs cがあり、(ekmett のcontstraintsパッケージから言葉を借りるために)含意を知っている場合、どうすれば を取得できますか?cc xd xRecAll f rs d

私が尋ねる理由は、いくつかの型クラスの制約を満たす必要があるいくつかの関数でレコードを扱っているからです。これを行うために、 existsパッケージのControl.Constraints.Combineモジュールの:&:コンビネーターを使用しています。(注: の非常に古いバージョンに依存しているため、他のものがインストールされている場合、パッケージはビルドされません。ただし、言及した 1 つのモジュールをコピーするだけでかまいません。) これにより、最小化しながら、いくつかの本当に美しい制約を取得できますタイプクラスのブロイラープレート。例えば：contravariant

RecAll f rs (TypeableKey :&: FromJSON :&: TypeableVal) => Rec f rs -> Value

しかし、この関数の本体内で、より弱い制約を要求する別の関数を呼び出します。次のようになります。

RecAll f rs (TypeableKey :&: TypeableVal) => Rec f rs -> Value

GHC は、2 番目のステートメントが最初のステートメントから続くことを認識できません。そうなのだろうと思いました。私が見ることができないのは、それを具体化して GHC を助けるためにそれを証明する方法です。これまでのところ、私はこれを持っています：

import Data.Constraint

weakenAnd1 :: ((a :&: b) c) :- a c                                                                    
weakenAnd1 = Sub Dict -- not the Dict from vinyl. ekmett's Dict.

weakenAnd2 :: ((a :&: b) c) :- b c                                                                    
weakenAnd2 = Sub Dict

これらは正常に動作します。しかし、これは私が立ち往生しているところです：

-- The two Proxy args are to stop GHC from complaining about AmbiguousTypes
weakenRecAll :: Proxy f -> Proxy rs -> (a c :- b c) -> (RecAll f rs a :- RecAll f rs b)
weakenRecAll _ _ (Sub Dict) = Sub Dict

これはコンパイルされません。私が探している効果を得る方法を知っている人はいますか。エラーが参考になる場合は、ここにエラーがあります。また、私はDict実際のコードに修飾されたインポートを持っているので、それが言及されている理由Constraint.Dictです:

Table.hs:76:23:
    Could not deduce (a c) arising from a pattern
    Relevant bindings include
      weakenRecAll :: Proxy f
                      -> Proxy rs -> (a c :- b c) -> RecAll f rs a :- RecAll f rs b
        (bound at Table.hs:76:1)
    In the pattern: Constraint.Dict
    In the pattern: Sub Constraint.Dict
    In an equation for ‘weakenRecAll’:
        weakenRecAll _ _ (Sub Constraint.Dict) = Sub Constraint.Dict

Table.hs:76:46:
    Could not deduce (RecAll f rs b)
      arising from a use of ‘Constraint.Dict’
    from the context (b c)
      bound by a pattern with constructor
                 Constraint.Dict :: forall (a :: Constraint).
                                    (a) =>
                                    Constraint.Dict a,
               in an equation for ‘weakenRecAll’
      at Table.hs:76:23-37
    or from (RecAll f rs a)
      bound by a type expected by the context:
                 (RecAll f rs a) => Constraint.Dict (RecAll f rs b)
      at Table.hs:76:42-60
    Relevant bindings include
      weakenRecAll :: Proxy f
                      -> Proxy rs -> (a c :- b c) -> RecAll f rs a :- RecAll f rs b
        (bound at Table.hs:76:1)
    In the first argument of ‘Sub’, namely ‘Constraint.Dict’
    In the expression: Sub Constraint.Dict
    In an equation for ‘weakenRecAll’:
        weakenRecAll _ _ (Sub Constraint.Dict) = Sub Constraint.Dict
4

1 に答える 1

12

Dictとがどのように使用されることを意図しているかを確認することから始めましょう(:-)。

ordToEq :: Dict (Ord a) -> Dict (Eq a)
ordToEq Dict = Dict

Dicttypeの値に対するパターン マッチングDict (Ord a)は、制約Ord aをスコープに持ち込み、そこからEq a推測できます (Eqは のスーパークラスであるOrdため) Dict :: Dict (Eq a)。

ordEntailsEq :: Ord a :- Eq a
ordEntailsEq = Sub Dict

同様に、Sub引数の期間中、その入力制約をスコープに持ち込み、これDict :: Dict (Eq a)も適切に型付けできるようにします。

ただし、パターン マッチング onDictは制約をスコープに取り込みますが、パターン マッチング onSub Dictは何らかの新しい制約変換規則をスコープに取り込みません。実際、入力制約が既にスコープ内にない限り、パターン マッチはまったくできませんSub Dict。

-- Could not deduce (Ord a) arising from a pattern
constZero :: Ord a :- Eq a -> Int
constZero (Sub Dict) = 0

-- okay
constZero' :: Ord a => Ord a :- Eq a -> Int
constZero' (Sub Dict) = 0

これで最初の型エラーが説明"Could not deduce (a c) arising from a pattern"されました: でパターン マッチを試みましSub Dictたが、入力制約a cはまだスコープ内にありませんでした。

もちろん、もう 1 つのタイプ エラーは、スコープに入るために管理した制約が、制約を満たすのに十分ではなかったということRecAll f rs bです。では、どの部品が必要で、どの部品が不足しているのでしょうか? の定義を見てみましょうRecAll。

type family RecAll f rs c :: Constraint where
  RecAll f [] c = ()     
  RecAll f (r : rs) c = (c (f r), RecAll f rs c)

あはは！RecAllは型ファミリーであり、そのままでは評価されず、完全に抽象化されているためrs、制約RecAll f rs cはブラック ボックスであり、小さなピースのセットからは満たすことができません。またはに特化rsすると、必要な部分が明確になります。[](r : rs)

recAllNil :: Dict (RecAll f '[] c)
recAllNil = Dict

recAllCons :: p rs
           -> Dict (c (f r))
           -> Dict (RecAll f rs c)
           -> Dict (RecAll f (r ': rs) c)
recAllCons _ Dict Dict = Dict

より柔軟性があるため、p rs代わりに を使用しています。Proxy rsRec f rsp ~ Rec f

(:-)次に、代わりにを使用して上記のバージョンを実装しましょうDict。

weakenNil :: RecAll f '[] c1 :- RecAll f '[] c2
weakenNil = Sub Dict

weakenCons :: p rs
           -> c1 (f r) :- c2 (f r)
           -> RecAll f rs c1 :- RecAll f rs c2
           -> RecAll f (r ': rs) c1 :- RecAll f (r ': rs) c2
weakenCons _ entailsF entailsR = Sub $ case (entailsF, entailsR) of
    (Sub Dict, Sub Dict) -> Dict

SubRecAll f (r ': rs) c1関数の本体の残りの部分を含めるように手配した引数の期間中、その入力制約をスコープに持ち込みます。型ファミリの式は にRecAll f (r ': rs) c1展開され(c1 (f r), RecAll f rs c1)、両方ともスコープに含まれます。それらがスコープ内にあるという事実により、2 つの でパターン マッチングが可能にSub Dictなり、これら 2Dictつがそれぞれの制約をスコープ内にもたらします: c2 (f r)、およびRecAll f rs c2。これら 2 つはまさにターゲット制約がRecAll f (r ': rs) c2展開されるものなので、Dict右側は適切に型付けされています。

の実装を完了するには、作業をまたはに委譲するかどうかを決定するために、weakenAllRecon でパターン マッチする必要があります。しかし、はタイプ レベルであるため、直接パターン マッチすることはできません。Hasochismペーパーでは、型レベルでパターン マッチングを行うために、ラッパー データ型を作成する必要があることを説明しています。その仕組みは、各コンストラクターが対応するコンストラクターによってインデックス付けされるため、コンストラクターの値レベルでパターン マッチを行うと、対応するコンストラクターが型レベルでも暗示されます。などの型レベルのリストに対してそのようなラッパーを定義できますが、たまたまrsweakenNilweakenConsrsNatNattyNattyNatNattyrsRec f rsにはすでに と に対応するコンストラクタが[]あり(:)、 の呼び出し元weakenAllRecはいずれにせよ 1 つを持っている可能性があります。

weakenRecAll :: Rec f rs
             -> (forall a. c1 a :- c2 a)
             -> RecAll f rs c1 :- RecAll f rs c2
weakenRecAll RNil       entails = weakenNil
weakenRecAll (fx :& rs) entails = weakenCons rs entails
                                $ weakenRecAll rs entails

の型は、単に ではなくでentailsなければならないことに注意してください。なぜなら、それが呼び出し元の選択のいずれに対しても機能すると主張したくないからです。forall a. c1 a :- c2 ac1 a :- c2 aweakenRecAllac1 ac2 aa

于 2015-04-28T04:08:12.920 に答える