haskell – 证明产品组件的约束条件适用于产品的实际情况

2023年4月1日 240次阅读

我有一个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

最佳答案 一种方法是在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类型反映你的实例的结构.

点赞