Reputation: 35099
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
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