haskell - 存在量化类型类

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 的(某种)父类(super class)类型。
Iso type 只是以下存储同构的字典:

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

Answer 1

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

一旦您 express 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)