Gabriella Gonzalez
Gabriella Gonzalez

Reputation: 35099

Existentially quantified type class

What is the type-class equivalent to the following existentially quantified dictionary, inspired by the Pipe type:

{-# 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)               }

The rough idea I'm going for is trying to say that given the (PipeLike p) constraint, we can then infer (MonadTrans (p a b), Monad (p a b m) and (using pseudo-code) (Category "\a b -> p a b m r").

The CategoryI and MonadI are just the dictionary equivalents of those type-classes that I use to express the idea that Category, Monad, and MonadTrans are (sort of) super-classes of this PipeLike type.

The Iso type is just the following dictionary storing an isomorphism:

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

Upvotes: 4

Views: 323

Answers (1)

Heatsink
Heatsink

Reputation: 7761

If this is indeed a type class, then the dictionary value is determined solely by the type p. In particular, the type cat is determined solely by p. This can be expressed using an associated data type. In a class definition, an associated data type is written like a data definition without a right-hand side.

Once you express cat as a type, the other members can easily be changed to type classes, as I've shown for Monad and MonadTrans. Note that I prefer to use explicit kind signatures for complicated kinds.

{-# 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)

Upvotes: 5

Related Questions