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 (
put), and the environment monad (
Reader in Haskell) comes with operations for reading the environment and performing a computation in a modified environment (
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
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
join is the multiplication of the monad
join = (>>= id).
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,
(++) 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
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.
local is not an algebraic for
Reader but can become algebraic if we implement the environment monad with
local' is algebraic for
Reader', we get a liftable operation
localL. The apparently arbitrary move from
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.