## Sunday, February 27, 2022

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

:: Monad m => ReaderT e m a -> StateT e m a

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

``````nat (return x) = return x

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

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
hush (Left  _) = Nothing
hush (Right x) = Just x``````

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

``````hush (return x)

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

``````hush (do { x <- m; f x })

-- Desugar `do` notation
hush (m >>= \x -> f x)

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

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

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

``````f . id = 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:

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

… and `return` is the identity of the `(>=>)` operator:

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

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

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

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

(nat .) return = return``````

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

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

-- Reparenthesize things, for clarity:
nat . (f >=> g) = (nat . f) >=> (nat . g)

-- Definition of `(>=>)`:
--
-- f >=> g = \x -> f x >>= \y -> g y
nat . (\x -> f x >>= \y -> g y) = \x -> (nat . f) x >>= \y -> (nat . g) y

-- Apply both sides to `x`
(nat . (\x -> f x >>= \y -> g y)) x = (nat . f) x >>= \y -> (nat . g) y

-- Definition of `(.)`:
--
-- (f . g) x = f (g x)
nat ((\x -> f x >>= \y -> g y) x) = nat (f x) >>= \y -> nat (g y)

-- β-reduce
nat (f x >>= \y -> g y) = nat (f x) >>= \y -> nat (g y)

-- Replace `f x` with `m`
nat (m >>= \y -> g y) = nat m >>= \y -> nat (g y)

-- Resugar using `do` notation
nat (do { y <- m; g y }) = do { y <- nat m; nat (g y) }

-- Rename `y` to `x` and rename `g` to `f`, for consistency with original laws
nat (do { x <- m; f x }) = do { x <- nat m; nat (f x) }``````

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

``````(nat .) return = return

-- Remove unnecessary parentheses
nat . return = return

-- Apply both sides to `x`
(nat . return) x = return x

-- Definition of `(.)`:
--
-- (f . g) x = f (g x)
nat (return x) = return x``````

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