This post briefly explains what a monad morphism is in the context of Haskell, since I wanted a succinct explanation that I could refer to for other posts. In order to keep things short, I will assume that you are already comfortable with Haskell’s `Monad`

class and `do`

notation.

A monad morphism is:

- … a natural transformation
- … that obeys two laws

… so first I’ll explain what a natural transformation is followed by an explanation of the two monad morphism laws.

#### Natural transformations

A natural transformation in Haskell is a function whose type can be expressed in terms of the following type-level operator:

```
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}
type m ~> n = forall a . m a -> n a
```

In other words, a natural transformation is a function that converts a value of type `m a`

into a value of type `n a`

such that it works for any possible type `a`

.

Here are some examples of natural transformations in the wild whose types could be written in terms of the above `(~>)`

type-level operator:

```
Control.Error.Util.hush :: Either e a -> Maybe a
-- Either e ~> Maybe
Data.Maybe.listToMaybe :: [a] -> Maybe a
-- [] ~> Maybe
UnliftIO.Exception.fromEither :: Exception e => Either e a -> IO a
-- Exception e => Either e ~> IO
Control.Monad.State.UnificationExtras.liftReaderT :: Monad m => ReaderT e m a -> StateT e m a
-- Monad m => ReaderT e m ~> StateT e m
```

#### Laws

Now that we’ve defined what a natural transformation is we can define what a monad morphism is.

A monad morphism is a special case of a natural transformation (which we will denote `nat`

) that satisfies the following two laws, known as the monad morphism laws:

```
return x) = return x
nat (
do { x <- m; f x }) = do { x <- nat m; nat (f x) } nat (
```

In other words, a monad morphism “distributes over” `Monad`

operations, leaving them undisturbed, which is a useful guarantee.

Three of the above example natural transformations (`hush`

, `fromEither`

, and `liftReaderT`

) are also monad morphisms, since they satisfy those two monad morphism laws. In contrast, `listToMaybe`

is an example of a natural transformation that is not a monad morphism.

#### Example proof of laws

Here is an example of how you would prove the monad morphism laws for the `hush`

function, which is defined like this:

```
hush :: Either e a -> Maybe a
Left _) = Nothing
hush (Right x) = Just x hush (
```

We’ll begin by proving the first monad morphism law:

```
return x)
hush (
-- Add a type annotation to note that `hush` only accepts an `Either` as input
= hush (return x :: Either e a)
-- return x :: Either e a = Right x
= hush (Right x)
-- Definition of `hush`
= Just x
-- return x :: Maybe a = Just x
= return x :: Maybe a
-- Drop the type annotation
= return x
```

… and here is how we prove the second monad morphism law:

```
do { x <- m; f x })
hush (
-- Desugar `do` notation
>>= \x -> f x)
hush (m
-- There are two possible cases: `m = Left l` or `m = Right r`
-- Case: `m = Left l`:
↳ = hush (Left l >>= \x -> f x)
-- Definition of `(>>=)` for `Either e` `Monad`
= hush (Left l)
-- Definition of `hush`
= Nothing
-- Definition of `(>>=)` for `Maybe` `Monad`, but in reverse
= Nothing >>= \x -> hush (f x)
-- Definition of `hush`, but in reverse
= hush (Left l) >>= \x -> hush (f x)
-- Resugar `do` notation
= do { x <- hush (Left l); hush (f x) }
-- `m = Left l` in this case
= do { x <- hush m; hush (f x) }
-- Case: `m = Right r`
↳ = hush (Right r >>= \x -> f x)
-- Definition of `(>>=)` for `Either e` `Monad`
= hush (f r)
-- Definition of `(>>=)` for `Maybe` `Monad`, but in reverse
= Just r >>= \x -> hush (f x)
-- Definition of `hush`, but in reverse
= hush (Right r) >>= \x -> hush (f x)
-- Resugar `do` notation
= do { x <- hush (Right r); hush (f x) }
-- `m = Right r` in this case
= do { x <- hush m; hush (f x) }
```

#### Rationale behind the laws

The reason we choose those laws is because they are similar to the functor laws when viewed through the appropriate lens.

As a recap, the functor laws say that any implementation of Haskell’s `Functor`

class must obey these two laws:

```
fmap (f . g) = fmap f . fmap g
fmap id = id
```

However, the category theory notion of a functor is more general than the Haskell notion of a functor. Specifically, the more general notion of a functor lets you replace `(.)`

with any associative operator, meaning that the following law still holds:

`. g) . h = f . (g . h) (f `

… and also lets you replace `id`

with any expression that is the identity of the corresponding `(.)`

operator, meaning that the following two laws still hold:

```
. id = f
f
id . f = f
```

Once we allow ourselves to introduce more exotic analogs to `(.)`

and `id`

then we can similarly introduce more exotic analogs to `fmap`

that don’t fit into the mold of Haskell’s `Functor`

class.

A monad morphism is one such exotic analog to `fmap`

, where we:

- … substitute
`(.)`

with the`(>=>)`

operator from`Control.Monad`

- … substitute
`id`

with`return`

from the`Monad`

class - … substitute
`fmap`

with`(nat .)`

where`nat`

is any monad morphism

This works out because the `(>=>)`

operator is associative:

`>=> g) >=> h = f >=> (g >=> h) (f `

… and `return`

is the identity of the `(>=>)`

operator:

```
>=> return = f
f
return >=> f = f
```

… so if we restate the functor laws with those substitutions, we get:

```
.) (f >=> g) = (nat .) f >=> (nat .) g
(nat
.) return = return (nat
```

… and those are the monad morphism laws, just stated in a different way.

We can see the correspondence to the original monad morphism laws if we simplify things a bit. We’ll begin by simplifying the first equation to get back the original first monad morphism law:

```
.) (f >=> g) = (nat .) f >=> (nat .) g
(nat
-- Reparenthesize things, for clarity:
. (f >=> g) = (nat . f) >=> (nat . g)
nat
-- Definition of `(>=>)`:
--
-- f >=> g = \x -> f x >>= \y -> g y
. (\x -> f x >>= \y -> g y) = \x -> (nat . f) x >>= \y -> (nat . g) y
nat
-- Apply both sides to `x`
. (\x -> f x >>= \y -> g y)) x = (nat . f) x >>= \y -> (nat . g) y
(nat
-- Definition of `(.)`:
--
-- (f . g) x = f (g x)
-> f x >>= \y -> g y) x) = nat (f x) >>= \y -> nat (g y)
nat ((\x
-- β-reduce
>>= \y -> g y) = nat (f x) >>= \y -> nat (g y)
nat (f x
-- Replace `f x` with `m`
>>= \y -> g y) = nat m >>= \y -> nat (g y)
nat (m
-- Resugar using `do` notation
do { y <- m; g y }) = do { y <- nat m; nat (g y) }
nat (
-- Rename `y` to `x` and rename `g` to `f`, for consistency with original laws
do { x <- m; f x }) = do { x <- nat m; nat (f x) } nat (
```

Similarly, we can simplify the second equation to get back the original second monad morphism law:

```
.) return = return
(nat
-- Remove unnecessary parentheses
. return = return
nat
-- Apply both sides to `x`
. return) x = return x
(nat
-- Definition of `(.)`:
--
-- (f . g) x = f (g x)
return x) = return x nat (
```

In other words, the monad morphism laws are functor laws in disguise.

Nitpick: I don't think `listToMaybe` is a monad homomorphism. Let `f :: Int -> [Int]` be defined by `f x = if x == 0 then [] else [x]` and let `m = [0, 1]`. Then `listToMaybe (do { x <- m; f x })` is `Just 1` but `do { x <- listToMaybe m; listToMaybe (f x) }` is `Nothing`. Maybe you were thinking of `MaybeToList` which is a monad homomorphism? On the other hand `listToMaybe` is a homomorphism but for a differnet monoidal structure. It is an applicative homomorphism.

ReplyDeleteYou're right. I updated the post to note that listToMaybe is not a monad morphism

DeleteThanks for this post! I was not familiar with this concept in Haskell. Your explanations are really helpful. It is great to see the connection to functors.

ReplyDelete