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?

You are looking for “ornaments.”

http://gallium.inria.fr/~remy/stages/ornaments.html

So, when you say something is a “free X” for some X, that is incomplete. Instead, the free structure is generated from something. For example, Nat is a free monoid, and in particular, it’s the free monoid on one generator (i.e. generated from a singleton set.) [Bool] would be the free monoid on two generators, and in general [T] is the free monoid generated by T. In category theory, this is witnessed by the fact that the functor to the free object (the left adjoint of the “forgetful” functor) is from some category to another. For monoids, it’s from the category of sets to the category of monoids. You can have free functors from other categories even to the same category. For example, there is a free functor from the category of semigroups to the category of monoids that simply adjoins a formal unit. This what Option does in the semigroups package.

Skipping to the Category case, this is another case where you need to be clear about the category you are generating from. There is a free functor from the category of sets to the category of categories, namely the discrete category functor. This is not the free construction you are using. Instead, you are starting with binary relations (actually, that’s not true, I’ll return to this.) There is, however, different perspective you can take on binary relations. They are (directed) graphs. In that light, your construction could be viewed as the free category generated from a graph. rel’s kind is not that of a type relation. That would be * -> * -> Bool. There are a few directions you could go to explain it. The most in line with your description is that it is a multirelation, and then your construction would be the free category generated from a multigraph. You could also say that rel is a category or a profunctor, but that would not lead to free constructions.

Jumping back to MonadPlus. To be a MonadPlus also requires being a monad. So it doesn’t make sense to talk about being a “free MonadPlus” without also providing the Monad structure. Typically for free monads we think of them as generated from (endo)functors. In this case the functor represents the signature of the operations in our algebra. So, supporting MonadPlus would just lead to the “free MonadPlus” functor adding, in addition to a formal Return, a formal Fail and Amb (mzero/mplus). However, these would be subject to laws (e.g. associativity of mplus) that would not hold with respect to this representation. A similar thing happens with lists as free monoids, and there the problem is finessed by identifying the equivalence classes of syntactic terms with a canonical representative (namely the fully right associated sequence).

Anyway, I may make another post on other aspects of this that are a little more oriented to your questions. This was mostly background.

Cool! Thanks for the reply. I was intentionally ignoring the fact that MonadPlus requires Monad.

Regarding the “relations” thing. Usually when correlating types with propositions, we say the proposition is true if the type is inhabited. So `rel a b` is “true” only if there is `proof :: rel a b`. It’s true that I was fast and loose with my examples in this post, but I still think it accurate to call something of kind `* -> * -> *` a “relation.”

Looking at it as a graph is indeed exactly how I was first going to describe it. The original paths are all of the inhabitants of `rel a b`, and then the `Refl` and `Trans` constructors create new paths by composing the originals. But for whatever reason I decided to describe it as Refl/Trans over “relations” instead of over “paths.” They’re sort of the same thing, I guess.

This feels a lot like a Coq tactic.