Implementing a category-theoretic Hask-monad in Haskell

13 min readJun 28, 2015

Hi! In this post, we’ll build up monads from their components (functors and natural transformations), consider a monad in a specific category, and verify the monad laws in QuickCheck, which is interesting in itself because it involves modeling both types and values within values. It’ll be useful to be comfortable with categories, functors, and natural transformations, though we’ll define everything from scratch — the first nineteen pages of Stefan Klinger’s monad guide are perfect for this if you’re up for the reading.

Defining monads

Our goal is to implement (in Haskell) a monad in the category Hask, so we should define what a monad looks like. This won’t make much sense until we define some more terms, but it’s motivation for why we’ll define them. Without further ado, a monad in a category C is a 3-tuple (µ, η, F) where

F is an endofunctor into C
µ is a natural transformation from F^2 to F
η is a natural transformation from the identity endofunctor I in C to F

such that the following laws hold:

Monad law 1: µ • (µ . F) = µ • (F . µ)
Monad law 2: µ • (η . F) = µ • (F . η) = I

where (.) is both arrow composition and function composition (sometimes we will use (∘)), and (•) is composition of natural transformations (vertical composition).

Functors

Let’s proceed to define and code the three functors we’ve said are needed to construct a monad: I, F, and F^2! Let C and D be categories. Informally speaking, A functor F : C → D is a mapping from C-objects to D-objects and C-arrows to D-arrows that has the homomorphic property with respect to arrow composition (F (f ∘ g) = F f ∘ F g, where on the left-hand side of the equality ∘ is composition in C, and on the right-hand side it’s composition in D). An endofunctor into C is a functor from C to C. I is the identity functor, and its implementation for the category Hask is trivial:

 — | The identity functor on Hask as it behaves on objects.
iObj :: a -> a
iObj = id — | The identity functor on Hask as it behaves on arrows.
iArr :: (a -> b) -> (a -> b)
iArr = id

F’s implementation requires Applicative, not Functor:

 — | F, a Hask endofunctor, as it behaves on objects.
fObj :: (Applicative f) => a -> f a
fObj = pure — | F, a Hask endofunctor, as it behaves on arrows.
fArr :: (Applicative f) => (a -> b) -> (f a -> f b)
fArr = fmap

This is because in Haskell, the Functor typeclass only requires implementation of fmap (see AMP for more information on these issues), which is how functors lift arrows into their target categories; it unfortunately is missing a function for how to lift objects. However, the subtype Applicative defines pure, which lifts objects.

F^2 is the composition of F and F:

— | F^2 = F . F, a Hask endofunctor, as it behaves on objects.
f2Obj :: (Applicative f) => a -> f (f a)
f2Obj = fObj . fObj— | F^2 = F . F, a Hask endofunctor, as it behaves on arrows.
f2Arr :: (Applicative f) => (a -> b) -> (f (f a) -> f (f b))
f2Arr = fArr . fArr

Aside: what are a and b, here? Hask-arrows are Haskell functions; they operate on Haskell values. The values on which they operate have types: the types in the type signature of the arrow in question. So, a and b will be Hask-objects.

Natural transformations

Fig. 1. A transformation (not natural without condition shown in Fig. 2)

Let’s move on to the remaining two components of a monad: the two natural transformations µ and η! Let C and D be categories, and F and G be functors from C to D. A natural transformation γ : F →. G (the dot should be above the arrow), is a nicely behaved function from C-objects to D-morphisms. Specifically, it maps a C-object a to an arrow in D from F a to G a, formally represented by the above commutative diagram. Additionally, when h : a → b is an arrow in C, γ a : F a→ G a is such that the following diagram commutes (see here for more on what that means):

Let’s define the first natural transformation, µ : F^2 →. F:

Fig. 3. µ : F^2 →. F, a natural transformation

Different functors will implement this function differently. Here’s what the definition looks like for the List functor:

µ :: a -> ([[a]] -> [a])
µ _ = concat

And for Maybe, it’s

µ :: a -> (Maybe (Maybe a) -> Maybe a)
µ _ (Just (Just a)) = Just a
µ _ (Just Nothing) = Nothing
µ _ Nothing = Nothing

Notice that we’re ignoring the first argument; this is because the implementations don’t depend on it: flattening two levels of Lists is same if it’s [[Int]] or [[String]]. Why, then, do we differentiate µ a and µ b in the math? This is because µ a and µ b are *separate arrows*. It’s merely an implementation detail that they happen to be implemented identically. Thankfully, the fact that we mark the type signature of the function as µ :: Applicative f => a -> (f (f a) -> f a) instead of µ ::Applicative f => b -> (f (f a) -> f a) means that the type system will enforce the distinctness of these two arrows.

The second natural transformation, η : I →. F, is defined as follows:

Fig. 4. η : I →. F, a natural transformation

And here's how it’s implemented by List and Maybe:

η :: a -> (a -> [a])
η _ = \a -> [a]η :: a -> (a -> Maybe a)
η _ = \a -> Just a

Both of these implementations look pretty similar. In fact, we can coalesce them:

η :: (Applicative f) => a -> (a -> f a)
η _ = fObj

In fact, η _ *has* to be equal to fObj, because the diagram on the left has to be commutative by definition. That is, (i ∘ η a) a = F a. Thus, η is definable in terms of F. We’ll see later that it’s included in the monad definition anyway for convenience of phrasing the second monad law.

Great! Now let’s write some tests for this code.

Interlude: QuickCheck

QuickCheck is a package for unit testing in Haskell. Its primary selling point is that it can generate random inputs as test cases, so you can frame your tests in a declarative manner by stating invariants and it’ll give you a bunch of inputs and tell you if the property holds for all of them. For example, let’s say you wrote a function plus to add two Ints. You might test the commutativity of your function as follows:

> ghci
λ let plus :: Int -> Int -> Int; plus x y = x + y
λ quickCheck (\x y -> x `plus` y == y `plus` x)
+++ OK, passed 100 tests.

Testing naturality

It’s not obvious that the code for and µ and η will accurately model the commutativity of the diagrams in Fig. 3 and Fig. 4. Let’s test the naturality:

{- 
        I h
  I a -------> I b
  |            |
  | η a        | η b
  |            |
  v            v
  F a -------> F b
        F h
-}
testη :: (Monad' m, Eq (m HV)) => MonadImpl m -> Fun HaskellValue HaskellValue -> [HaskellValue] -> Bool
testη fArr' (Fun _ h) = all
    (\a -> let b = h a in
        (η b . iArr h $ iObj a) == (fArr' h . η a $ iObj a))

and

{-
       F^2 h
  F^2 a ----> F^2 b
  |           |
  | µ a       | µ b
  |           |
  v           v
  F a ------> F b
       F h
-}
testµ :: (Monad' m, Eq (m HV)) => MonadImpl m -> Fun HV HV -> [m (m HV)] -> Bool
testµ _ (Fun _ h) = all
    (\mma ->
        (µ undefined . f2Arr h $ mma) == (fArr h . µ undefined $ mma))

OK. In each test, we take in an arbitrary function h, and a list of possible inputs to it (the as, taken in point-free), and verify that a property holds for each of them. We also take in a MonadImpl parameter — this is a function (fArr’) that is hardcoded to a specific functor — that way, we can run the tests for Lists or Maybes or whatever functor we choose. Don’t worry too much about this parameter.

The Fun data type is also new. It comes from Test.Quickcheck.Function, and can be used to generate arbitrary functions between types, which is awesome! For example, it might generate the following arbitrary function from String to Int:

{"elephant"->1, "monkey"->1, _->0}

Here we use it to generate the function h (see Fig. 2, reproduced to the left). The natural transformation conditions (that this diagram is commutative) apply for *any* h and a, so the best we can do is generate as many possible hs and as as we can with QuickCheck and verify that the condition holds for each a for each h.

Third, we’re passing in undefined to µ. This is because our implementation of µ ignores its first argument (see section on coding µ); undefined is the sole inhabitant of the Bottom type, which is a subtype of every type (so it passes the typechecker, here). We could also pass undefined to η, but since in that test we have actual values for a and b, we use those instead to better mirror the math (in the µ test we might get passed the empty list, so we wouldn’t have an a (or a b), and the empty list is polymorphically parameterized across all types so we couldn’t just pick one anyway).

Fourth, we’ve introduced the type HaskellValue. Again, objects in the category Hask are Haskell *types*, and arrows are functions between those types. Then, why are testing h on things called Haskell*Value*s, and not Haskell*Type*s? h might be an arrow from Int to String, but you feed it values of type Int, not the type Int. It might seem like we’re splitting hairs, here, but levels of indirection are important.

It’d be great if we could have instead written a function of type

testη :: Fun a b -> [a] -> Bool

but I couldn’t find a way to have QuickCheck generate arbitrary values of arbitrary *types*, so we approximate the possible values of types a and b with HaskellValue. Let’s define it as a sum type as follows (see here if you’re not comfortable with Haskell algebraic data types):

data HaskellValue
    = A String
    | B Int
    | C Bool
    | D Char
    | E (Either (Bool, Char, [Bool]) [Maybe (Maybe Int)])
    deriving (Show, Eq)

QuickCheck might generate for us - for example - the following function:

{D 'x'->C True, D 'a'->C True, D 'n'->C False, _->C False}

We’ll need to write Arbitrary, CoArbitrary, and Function instances for HaskellValue in order for QuickCheck to generate the random functions and values. This isn’t as interesting, so we’ll skip over it (see here for implementations of these).

We didn’t write tests to ensure that our functors are really functors, though we did write tests for our natural transformations. This is because any Haskell data type that implements the typeclasses Applicative and Functor is already supposed to obey the functor laws.

Monads

Now we’re ready to build monads! As we said, a monad is a 3-tuple (µ, η, F) (with conditions on µ, η, and F defined in the above sections) such that the following laws hold:

Monad Law 1: µ • (µ . F) = µ • (F . µ)
Monad Law 2: µ • (η . F) = µ • (F . η) = I

Fig. 6. Vertical composition of the functions µ and η

We now know all of these symbols except for one: (•). It represents a kind of function composition called vertical composition, which happens to be how you compose natural transformations. It’s defined by the commutative diagram on the left. We can define it with the following Haskell code:

(•) :: (a -> (ga -> ha)) -> (a -> (fa -> ga)) -> (a -> (fa -> ha))
µ • η = \a -> µ a . η a

Aside on the monad laws: µ a (for a in Hask) is not required to be injective (in fact, no Hask-arrows are monic), so the two laws are *not* identical to requiring commutativity of (.) for (µ, F) and (η, F) (i.e. not the same as requiring µ . F = F . µ and η . F = F . η).

We can test the laws as follows, using QuickCheck to generate arbitrary parameters:

-- Monad law 1: µ • (µ . F) = µ • (F . µ)
testLaw1 :: (Monad' m, Eq (m HV)) => MonadImpl m -> m (m (m HaskellValue)) -> Bool
testLaw1 _ mmma
    = (µ • (µ . fObj)) undefined mmma == (µ • (fArr . µ)) undefined mmma-- Monad law 2: µ • (η . F) = µ • (F . η) = I
testLaw2 :: (Monad' m, Eq (m HV)) => MonadImpl m -> m HV -> Bool
testLaw2 _ ma = and
    [ iObj ma == (µ • (η . fObj)) undefined ma
    , iObj ma == (µ • (fArr . η)) undefined ma ]
    -- (transitively µfη = µηf)

If we run these tests, we’ll see that the laws are satisfied!

As we would hope, the monad definition Haskell requires is phraseable in terms of our definition (and vice versa):

class (Applicative m) => Monad’ m where
    µ :: a -> (m (m a) -> m a)instance (Monad' m) => Monad m where
    return :: (Monad m) => a -> m a
    return = pure -- can also use `η undefined`    (>>=) :: (Monad m) => m a -> (a -> m b) -> m b
    ma >>= f = µ undefined . fmap f $ ma

Haskell has a function for µ undefined; it’s join (in Control.Monad).

Reflections

That’s it — we’ve provided a category-theoretic definition of a monad, coded up its constituent parts, and verified with tests the monad laws for arbitrary monads in the category Hask! Best of all, we now understand very clearly what it is that differentiates functors and monads — monads are functors that implement µ (remember, η was definable in terms of F). This leaves an interesting question — are there any functors for which no sane µ exists? That is, are there functors that can’t be monads? I don’t have an answer for this, but let me know if you come up with a good one ;)

Unfortunately, while QuickCheck can generate arbitrary functions between HaskellValues, it’s not guaranteed to be between the same value constructor each time, which means it doesn’t actually accurately model being a function from type 1 to type 2. For example, in GHCi:

λ (Fun _ h) <- generate (arbitrary :: Gen (Fun HaskellValue HaskellValue))
λ h (B 5)
D ‘f’
λ h (B 6)
C False
λ h (B 7)
B 3
λ h (B 8)
C True

If you have way of writing the tests that avoids this issue, let me know! That’d be awesome.

All the code is available here for running / perusing / modifying as you see fit. Many thanks to Frank Li and Alex Quach for comments on early drafts of this post! :)