Existentially quantitative class type

Question

What is a type class equivalent to the following existentially quantized dictionary inspired by the Pipe type:

 {-# LANGUAGE ExistentialQuantification, PolymorphicComponents #-} data PipeD p = forall cat . PipeD { isoI :: forall abmr . Iso (->) (pabmr) (cat mrab), categoryI :: forall mr . (Monad m) => CategoryI (cat mr) , monadI :: forall abm . (Monad m) => MonadI (pabm) , monadTransI :: forall ab . MonadTransI (pab) } 

The rough idea I'm going to try to say is that with the constraint (PipeLike p) we can infer (MonadTrans (pab), Monad (pabm) and (using pseudo-code) (Category "\ab -> pabmr") .

CategoryI and MonadI are simply the vocabulary equivalents of the type classes that I use to express the idea that Category , Monad and MonadTrans are (sort of) superclasses of this PipeLike type.

The Iso type is simply the following dictionary storing isomorphism:

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

Answer 1

If it is truly a type class, the value of the dictionary is determined only by type p . In particular, the type cat is defined only by p . This can be expressed using the data type associated with it. In a class definition, the associated data type is written as the data definition without the right side.

Once you express cat as a type, other members can easily be changed for class classes, as shown in Monad and MonadTrans . Note that I prefer to use explicit labels for complex types.

 {-# LANGUAGE TypeFamilies, FlexibleInstances, UndecidableInstances #-} class Pipe (p :: * -> * -> (* -> *) -> * -> *) where data Cat p :: (* -> *) -> * -> * -> * -> * isoI :: forall abm r. Iso (->) (pabmr) (Category pmrab) categoryI :: forall ab m. Monad m => CategoryI (Category pmr) instance (Pipe p, Monad m) => Monad (pabm) instance Pipe p => MonadTrans (pab)