What is a monad morphism (in Haskell)?

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:

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.