4

C1 つの型とタプルのインスタンスを持つクラスがあります。

class C a

instance C Int

instance (C a, C b) => C (a, b)

制約をキャプチャするための通常のDictGADT の使用

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ConstraintKinds #-}

data Dict c where
    Dict :: c => Dict c

C aから証明できC (a, b)ますか？

fstDict :: Dict (C (a, b)) -> Dict (C a)
fstDict Dict = ???

fstDict Dict = Dict十分ではなく、他の可能性はほとんどないため、すぐに答えは「いいえ」だと思います。C製品の構成要素の拘束を製品の拘束から回復できるように変更する方法はありますか?

私はおそらく間違って、最も密接に関連する質問とDict同じことを達成しようとしていますが、カテゴリの一方または両方の端からを要求する余裕があります。

data DSL a b where
    DSL :: (Dict C a -> DSL' a b) -> DSL a b

data DSL' a b where
    DSL' :: (C a, C b) => ... -> DSL' a b
4

2 に答える 2

1

1 つの方法は、すべての祖先辞書をDict型に格納することです。

data CDict a where
    IntDict :: C Int => CDict Int
    PairDict :: C (a, b) => CDict a -> CDict b -> CDict (a, b)

fstCDict :: CDict (a, b) -> CDict a
fstCDict (PairDict fst snd) = fst

CDictこれには、インスタンスの構造を型に反映させる必要があるという欠点があります。

于 2015-01-09T02:48:44.093 に答える
1

Daniel Wagner の回答のオープン バリアントでは、 a を使用しTypeFamilyて、クラスを実装する各型が必要なコンテキストを指定できるようにします。

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}

import GHC.Exts (Constraint)
import Data.Proxy

data Dict c where
    Dict :: c => Dict c

このクラスにより、各タイプは、Ctx aそのタイプに必要な追加の制約を指定できます。このcdict関数は、コンテキストを強制的に従わせ、基礎となるを for eg プロダクトに含めずCに取得する方法を提供し ます。CtxCtx

class C a where
    type Ctx a :: Constraint
    cdict :: Proxy a -> CDict a

ACDictはDict、制約と型が必要とするC a追加のコンテキストの両方を保持する a です。Ctx aa

type CDict a = Dict (C a, Ctx a)

インスタンスはInt余分なコンテキストを必要としません

instance C Int where
    type Ctx Int = ()
    cdict _ = Dict

タプル インスタンスにはC aとの両方が必要ですC b 

instance (C a, C b) => C (a, b) where
    type Ctx (a, b) = (C a, C b)
    cdict _ = Dict

fstCDictタプルについて書くことができます。

fstCDict :: forall a b. CDict (a, b) -> CDict a
fstCDict Dict = case cdict (Proxy :: Proxy a) of Dict -> Dict

不適切なインスタンス

C魔法のようにインスタンスを呼び出すShowインスタンスの間違ったインスタンスを書き込もうとすると、

instance (C a) => C (Maybe a) where
    type Ctx (Maybe a) = (C a, Show a)
    cdict _ = Dict

コンパイルエラーになります

    Could not deduce (Show a) arising from a use of `Dict'
    from the context (C a)
      bound by the instance declaration ...
    Possible fix:
      add (Show a) to the context of the instance declaration
    In the expression: Dict
    In an equation for `cdict': cdict _ = Dict
    In the instance declaration for `C (Maybe a)'
于 2015-01-09T06:26:34.437 に答える