This is perhaps obvious to anyone who has thoroughly studied category theory, but the similarities between Monoid, MonadPlus, and Category, have really struck me lately. I’m going to take a smidgeon of artistic license to present this train of thought.
class Monoid (a :: *) where mempty :: a (<>) :: a -> a -> a class MonadPlus (m :: * -> *) where mzero :: forall x. m x (<+>) :: forall x. m x -> m x -> m x class Category (c :: * -> * -> *) where id :: forall x. c x x (>>>) :: forall x y z. c x y -> c y z -> c x z
These classes all come with the same set of laws.
id >>> x = x -- left identity x >>> id = x -- right identity (x >>> y) >>> z = x >>> (y >>> z) -- associativity
I’d like to present three structures, which correspond to some sort of “free” instance. Notice how they all have the same shape. (I added a superfluous unit to the Nat to make the parallel just a little clearer.) I put “free” in quotes because I do not claim to actually understand what this means in category theory, nor do I claim to be using that term correctly in the category theoretic sense. I’m pretty sure I’m somewhat close to that definition, though.
My “free” Monoid is the natural numbers. Inexplicably, I’m going to do something weird and hide an arbitrary value inside the succ constructor. Just pretend that “v” isn’t there if it confuses you. It’s just the nats.
data Nat where Zero :: Nat Succ :: v -> Nat -> Nat instance Monoid Nat where mempty = Zero Zero y = y Succ v x <> y = Succ v (x <> y)
My “free” MonadPlus is homogeneous lists.
data List x where Nil :: List x Cons :: x -> List x -> List x instance MonadPlus List where mzero = Nil Nil my = my Cons x mx <+> my = Cons x (mx <+> my)
My “free” category is… a little more abstract than the last two. It’s extending any type relation with reflexivity and transitivity (regardless of whether the original relation includes reflexivity and transitivity).
data ReflTrans (rel :: * -> * -> *) :: * -> * -> * where Refl :: ReflTrans rel x x Trans :: rel x y -> ReflTrans rel y z -> ReflTrans rel x z instance Category (ReflTrans rel) where id = Refl Refl >>> yz = yz Trans rwx xy >>> yz = Trans rwx (xy >>> yz)
Also note an added similarity between the three:
unity :: v -> Nat unity v = Succ v Zero singleton :: x -> List x singleton x = Cons x Nil liftRel :: rel x y -> ReflTrans rel x y liftRel r = Trans r Refl infinity :: () -> Nat infinity () = Succ () (infinity ()) repeat x :: x -> List x repeat x = List x (repeat x) wat :: rel x x -> ReflTrans rel x x wat r = Trans r (iterate r)
So what’s my point? If you erase all of the types, then the code I have written for all three of these is identical modulo alpha renaming.
data Nat data List data ReflTrans
Zero Nil Refl
Succ v Nat Cons x List Trans r ReflTrans
Succ v x <> y = Succ v (x <> y)
Cons x xs <+> ys = Cons x (xs <+> ys)
Trans rwx xy >>> yz = Trans rwx (xy >>> yz)
And this begs the question: why should I write this code over and over, just to appease the type system? Is there a good way to unify these abstractions instead? How might we adjust Haskell’s type system to alleviate this redundancy?