## Archive for September, 2008

### Exponentials of containers (again)

Friday, September 5th, 2008 by Thorsten

I presented a simple derivation of Paul’s construction of the exponential of containers. I used the opportunity to discuss the exponential of functors and the Yoneda lemma. My derivation is based on the observation that writing for the exponentiation of functors and is a Napieran functor.
This can be shown using the Yoneda lemma. Then given a container and a functor we can reason as follows:

This shows that one can exponentiate any functor with a container (predicatively) and that exponent of containers is a container, since we know that is a container and containers are closed under composition and products. Expanding the definition gives rise to Paul’s definition.

Thursday, September 4th, 2008 by Mauro Jaskelioff

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.