by *Mauro Jaskelioff* on **September 4, 2008**.

Tagged as: Lunches.

Monad are an essential tool for functional programmers. When it comes to *combining* monads, the most popular technique is to use monad transformers to add an effect layer to an existing monad. Do you want a new state for your monad? Use the state monad transformer on your monad and voila! it’s done!

Actually, you are not really done. Monads usually come with a set of operations to manipulate the effect they model. For example, the state monad comes with operations for reading and updating the state (`get`

and `put`

), and the environment monad (`Reader`

in Haskell) comes with operations for reading the environment and performing a computation in a modified environment (`ask`

and `local`

). If you want the operations of your monad to be supported by the transformed monad, then you need to show how to lift the operations to the transformed monad. Unless a technology is used for automating these liftings, you need to provide an operation instance for every monad transformer in the library, leading to operation instances. That’s not modular!

The problem is not in monad transformers (other technologies for combining monads such as distributive laws or coproduct of monads suffer from the same problem). The problem is that **many of the operations associated with a monad are not really compatible with the monad**.

Monads have axioms that ensure that `return`

and `bind`

are well-behaved, so it is not unreasonable to think that there should be some axioms associated to its operations. So I propose to require operations to be algebraic. In our context this means that an operation `h`

for a monad `M`

should be of type `forall a . S (M a) -> M a`

for some functor `S`

, such that:

`join . h = h. fmap join`

where `join`

is the multiplication of the monad `join = (>>= id)`

.

For example, `uncurry (++) :: ([a],[a]) -> [a]`

is algebraic for the list monad, with `S a = (a,a)`

. On the other hand, `uncurry local :: (r->r, Reader r a) -> Reader r a`

has the correct type, with functor `S a = (r -> r, a)`

, but is not algebraic, as the condition does not hold. The operation `ask :: Reader r r`

doesn’t seem to have the correct type, but it is isomorphic to a function `ask' :: (r -> Reader r a) -> Reader r a`

, which is algebraic for `Reader r`

with `S a = r -> a`

. It’s convenient to consider algebraic operations up to isomorphism. Then, `ask`

and `(++)`

are algebraic.

So, what’s good about algebraic operations? They can be lifted by **any** monad morphism! Every algebraic operation is isomorphic to a natural transformation in the Kleisli category of the monad.

This means that for every algebraic operation `h :: forall a. S (M a) -> M a`

, monad `N`

, and monad morphism `lift :: forall a. M a -> N a`

, we get an algebraic operation `fromK (lift. toK h) :: forall a. S (N a) -> N a`

, i.e. the lifting of `h`

to `N`

.

Append is algebraic for the list monad, so we get a “liftable” version of append: for every monad morphism out of the list monad, we get a lifted operation.

Of course, not all the usual operations are algebraic for their monad. This does not mean that the operation is incorrect, but that the monad should be more powerful. **The operations determine the appropriate monad**.

The operation `local`

is not an algebraic for `Reader`

but can become algebraic if we implement the environment monad with `State`

:

Since `local'`

is algebraic for `Reader'`

, we get a liftable operation `localL`

. The apparently arbitrary move from `Reader`

into `State`

seems like a big eureka step. Actually, it’s the result of applying a general technique for finding appropriate monads for a given set of operations (paper in process).

Using these ideas, I managed to re-implement the monad transformer library with automatic lifting of operations. I will release the library as soon as I write a minimum of documentation.

comments powered by Disqus