On the applicative structures of monads

by oleksandrmanzyuk

In the paper “Lifting Operators and Laws”, Ralf Hinze identified an interesting class of applicative functors, so called strongly extensional applicative functors with K-combinators, that have a remarkable property: they satisfy every lifted base-level identity. An applicative functor m is called extensional if it satisfies the following property for each pair of values mf, mg :: m (a -> b): if for each mx :: m a holds mf <*> mx == mg <*> mx, then mf == mg. In other words, the function

(<*>) :: m (a -> b) -> (m a -> m b)

is injective. If furthermore the function

(. pure) . (<*>) :: m (a -> b) -> (a -> m b)

is injective, then m is called strongly extensional. Clearly, a strongly extensional applicative functor is also extensional. For example, the environment monad, Maybe, and the list monad are strongly extensional. The reader is referred to the paper for the definition of what it means for an applicative functor to have K-combinators.

At the very end of the paper Ralf Hinze asked the following question: Is every extensional applicative functor also strongly extensional? When I saw this question, I thought immediately: “This must be true for monads.” I argued as follows: Suppose m is a monad that is also an extensional applicative functor. Let us show that it is also strongly extensional. Let mf, mg :: m (a -> b) and suppose that

(mf <*>) . pure == (mg <*>) . pure.

The functions (mf <*>) and (mg <*>) have type m a -> m b, where the types m a and m b are free m-algebras. It is natural to ask: Are these functions compatible with the m-algebra structure? In other words, are the functions (mf <*>) and (mg <*>) m-algebra morphisms? I trusted my intuition, which suggested that was indeed the case. Applying the following well known fact from category theory I concluded that (mf <*>) == (mg <*>), and hence mf == mg by extensionality.

Lemma. Let a be a type and let g :: m b -> b be an m-algebra. There is a one-to-one correspondence between m-algebra morphisms h :: m a -> b from the free m-algebra join :: m (m a) -> m a to g :: m b -> b and functions a -> b. The correspondence is defined as follows: an m-algebra morphism h :: m a -> b is mapped to the composite h . return; conversely, a function k :: a -> b is extended to an m-algebra morphism h = g . liftM k.

However, a more careful analysis given below shows, somewhat unexpectedly, that whether my guess that (mf <*>) and (mg <*>) are m-algebra morphisms is correct depends on which of the two applicative structures of m we consider.

The point is, any Monad can be made Applicative in two different ways: by taking pure = return and (<*>) = ap, where

ap :: Monad m => m (a -> b) -> m a -> m b
ap mf mx = do  f  <-  mf
               x  <-  mx
               return (f x)

or by taking (<*>) to be the variant of ap, which we denote by pa, that performs the computations mf and mx in the opposite order:

pa :: Monad m => m (a -> b) -> m a -> m b
pa mf mx = do  x  <-  mx
               f  <-  mf
               return (f x)

There are no obvious reasons to prefer ap over pa, except that it appears more natural to perform the computations in the order they are supplied, which is probably why the applicative structure given by pa is overlooked.

Proposition. The function pa mf :: m a -> m b is an m-algebra morphism, for each mf :: m(a -> b). If m is a commutative monad, then also ap mf :: m a -> m b is an m-algebra morphism.

Before giving the proof of the proposition, which is straightforward, let me briefly recall the relevant notions.

An m-algebra is a type a together with a function f :: m a -> a, called the action, such that

f . return == id  and  f . lift f == f . join.

Given two m-algebras f :: m a -> a and g :: m b -> b, an m-algebra morphism is a function h :: a -> b such that

h . f == g . liftM h.

For any type a, the type m a is an m-algebra whose action is given by join :: m (m a) -> m a. m-algebras of this form are called free. A function g :: m a -> m b is an m-algebra morphism if

join . liftM g == g . join,

or equivalently, if for any mmx :: m (m a) holds

join (liftM g mmx) == g (join mmx)

For completeness, we also recall the definitions of join and liftM:

join :: Monad m => m (m a) -> m a
join mmx = mmx >>= id

liftM :: Monad m => (a -> b) -> m a -> m b
liftM f mx = mx >>= \x -> return (f x)

Proof of Proposition. Let us show that for each mf :: m (a -> b), the function pa mf :: m a -> m b is an m-algebra morphism. As explained above, we need to show that for each mmx :: m (m x), the equation

join (liftM (pa mf) mmx) == pa mf (join mmx)

holds true. Let us transform the left hand side:

    join (liftM (pa mf) mmx)

==  {- definition of join -}

    (liftM (pa mf) mmx) >>= id

==  {- definition of liftM -}

    (mmx >>= \mx -> return (pa mf mx)) >>= id

==  {- "associativity" monad law -}

    mmx >>= \mx -> return (pa mf mx) >>= id

==  {- "left identity" monad law -}

    mmx >>= \mx -> pa mf mx

==  {- definition of pa -}

    mmx >>= \mx -> mx >>= \x -> mf >>= \f -> return (f x)

The right hand side can be written as follows:

    pa mf (join mmx)

==  {- definition of join -}

    pa mf (mmx >>= id)

==  {- definition of pa -}

    (mmx >>= id) >>= \x -> mf >>= \f -> return (f x)

==  {- "associativity" monad law -}

    mmx >>= \mx -> id mx >>= \x -> mf >>= \f -> return (f x)

==  {- definition of id -}

    mmx >>= \mx -> mx >>= \x -> mf >>= \f -> return (f x)

The obtained expressions are identical, hence the assertion.

Suppose that m is a commutative monad. Let us show that the function ap mf :: m a -> m b is also an m-algebra morphism. Again, we have to prove that for each mmx :: m (m a), the equation

join (liftM (ap mf) mmx) == ap mf (join mmx)

holds true. On the one hand, we have:

    join (liftM (ap mf) mmx)

==  {- definitions of join -}

    (liftM (ap mf) mmx) >>= id

==  {- definition of liftM -}

    (mmx >>= \mx -> return (ap mf mx)) >>= id

==  {- "associativity" monad law -}

    mmx >>= \mx -> return (ap mf mx) >>= id

==  {- "left identity" monad law -}

    mmx >>= \mx -> ap mf mx

==  {- definition of ap -}

    mmx >>= \mx -> mf >>= \f -> mx >>= \x -> return (f x)

==  {- syntactic sugar -}

    do  mx  <-  mmx
        f   <-  mf
        x   <-  mx
        return (f x)

On the other hand:

    ap mf (join mmx)

==  {- definition of join -}

    ap mf (mmx >>= id)

==  {- definition of ap -}

    mf >>= \f -> (mmx >>= id) >>= \x -> return (f x)

==  {- "associativity" monad law -}

    mf >>= \f -> mmx >>= \mx -> id mx >>= \x -> return (f x)

==  {- definition of id -}

    mf >>= \f -> mmx >>= \mx -> mx >>= \x -> return (f x)

==  {- syntactic sugar -}

    do  f   <-  mf
        mx  <-  mmx
        x   <-  mx
        return (f x)

These expressions are equal because m is commutative, hence the assertion. Q.E.D.

We can now partly answer Ralf Hinze’s question “Is any extensional monad also strongly extensional?”

Proposition. Let m be a monad, and suppose its applicative structure is given by pure = return and (<*>) = pa. If m is extensional, then it is also strongly extensional.

Proof. Suppose m is extensional. Let us show it is also strongly extensional. Let mf, mg :: m (a -> b) and suppose that

pa mf (return x) == pa mg (return x)

for each x :: a. Because pa mf and pa mg are m-algebra morphisms, it follows by the lemma that pa mf == pa mg, which by the extensionality implies mf == mg. Q.E.D.

I find this apparent asymmetry in the properties of ap and pa bizarre. On the one hand, the answer to Ralf Hinze’s question seems to depend on which applicative structure we equip the monad with. Most likely, the answer is affirmative in both cases, but I haven’t found a proof yet. On the other hand, there is probably no asymmetry here, as the function ap produces m-algebra morphisms when partially applied to the second argument, while pa partially applied to the second argument is an m-algebra morphism if and only if m is commutative.

Are there any real world examples in which the applicative structure of monads given by pa has advantages over that given by ap?

About these ads