存在量化类型类

Question

受Pipe 类型启发，与以下存在量化字典等效的类型类是什么：

{-# LANGUAGE ExistentialQuantification, PolymorphicComponents #-}

data PipeD p = forall cat . PipeD {
    isoI        :: forall a b   m r . Iso (->) (p a b m r) (cat m r a b),
    categoryI   :: forall       m r . (Monad m) => CategoryI (cat m r)  ,
    monadI      :: forall a b   m   . (Monad m) => MonadI (p a b m)     ,
    monadTransI :: forall a b       . MonadTransI (p a b)               }

我的粗略想法是尝试说，鉴于(PipeLike p) 约束，我们可以推断(MonadTrans (p a b), Monad (p a b m) 和（使用伪代码）(Category "\a b -> p a b m r")。

CategoryI 和 MonadI 只是我用来表达Category、Monad 和Monad 和MonadTrans 是（某种）超类的想法的那些类型类的字典等价物这个PipeLike 类型。

Iso 类型只是以下存储同构的字典：

data Iso (~>) a b = Iso {
    fw :: a ~> b ,
    bw :: b ~> a }

Answer 1

如果这确实是一个类型类，则字典值仅由类型p 确定。特别是，cat 类型仅由p 确定。这可以使用关联的数据类型来表示。在类定义中，关联数据类型的编写方式类似于没有右侧的数据定义。

一旦您将cat 表达为一个类型，就可以轻松地将其他成员更改为类型类，正如我为Monad 和MonadTrans 展示的那样。请注意，对于复杂的种类，我更喜欢使用显式种类签名。

{-# LANGUAGE TypeFamilies, FlexibleInstances, UndecidableInstances #-}

class Pipe (p :: * -> * -> (* -> *) -> * -> *) where
  data Cat p :: (* -> *) -> * -> * -> * -> *
  isoI      :: forall a b m r. Iso (->) (p a b m r) (Category p m r a b)
  categoryI :: forall a b m.   Monad m => CategoryI (Category p m r)

instance (Pipe p, Monad m) => Monad (p a b m)

instance Pipe p => MonadTrans (p a b)