存在量化类型类

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和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)