# Implementing a category-theoretic Hask-monad in Haskell

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).

## Categories

Let’s dive in to it! A *category C* is comprised of

- A collection of things called
*C-objects* - A collection of things called
*C-arrows* - Operations assigning to each
*C*-arrow*f*a pair of*C*-objects representing the domain and co-domain of*f*

such that

- for each
*C*-object*a*, the identity arrow*i*:*a → a*is a*C*-arrow - composition of
*C*-arrows is associative ((*f*∘*g)*∘*h*=*f*∘ (*g*∘*h)*for all*C*-arrows*f*,*g*, and*h*) - the collection of
*C*-arrows is transitively closed under composition (*g*∘*f*is a*C*-arrow for all*C*-arrows*f*and*g*such that the co-domain of*f*is the domain of*g*)

Here are two categories to serve as examples:

**Set**, the category whose objects are sets and whose arrows are functions between sets**Grp**, the category whose objects are groups and whose arrows are group homomorphisms

*Hask* is the category of Haskell types and functions. If you wish, you can think of the objects in this category - Haskell types - as analogous to the objects in the category **Set, **in that they “contain” elements (Haskell values). The definition of a category does not require arrows to be unique, and this is mirrored in *Hask* by the existence of separate functions of the same type — for example, both the functions

`f :: Int -> Int`

f x = x + 1

and

`g :: Int -> Int`

g 0 = 142857

g _ = 0

are between the same *Hask-*objects, given that they have identical type signatures, but are separate arrows (and, indeed, are separate functions).

## 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

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*:

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 **List**s 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:

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 **Int**s. 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 **a**s, 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 **List**s or **Maybe**s 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 *h*s and *a*s 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 *functor*s, 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

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 **HaskellValue**s, 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! :)