haskell - 从约束对产品成立的事实证明约束对产品的某个组成部分成立

Question

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

class C a

instance C Int

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

使用普通的 Dict GADT 来捕获约束

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

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

是否可以从C (a, b)证明C a？

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

我怀疑立即的答案是“否”，因为 fstDict Dict = Dict 还不够，而且几乎没有其他可能性。有没有办法改变C，以便可以从产品的约束中恢复对产品组件的约束？

我试图完成与 the most closely related question 相同的事情，也许是错误的。 ，但是我有幸从类别的一端或两端要求一份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

Answer 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 类型反射(reflect)实例的结构。