4

我有一个类C，其中包含一种类型和元组的实例。

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

一种方法是将所有祖先字典存储在您的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 的答案的一个开放变体将使用 aTypeFamily让实现该类的每种类型指定它需要的上下文。

{-# 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函数强制上下文遵循C并提供一种方法来获取底层 Ctxs 而无需将它们包含在Ctx例如产品中。

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

然后ACDict是 a Dict，它既包含约束，也包含类型需要的C 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 回答