Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.
Sign up to join this community
Most resource regarding categorical notions in programming describe monads, but I've never seen a categorical description of monad transformers.
How could monad transformers be described in the terms of category theory?
In particular, I'd be interested in:
According to Oleksandr Manzuk, they are "translation of a monad along an adjunction", see "Calculating Monad Transformers with Category Theory". By the way, that's the third hit on Google for "monad transformer categorically". The first is a Stackoverflow question about this and the second is your question.
Augmenting Andrej's answer:
There is still no widespread agreement on the appropriate interface monad transformers should support in the functional programming context. Haskell's MTL is the de-facto interface, but Jaskelioff's Monatron is an alternative.
One of the earlier technical reports by Moggi, an abstract view of programming languages, discusses what should be the right notion of transformer to some extent (section 4.1). In particular, he discusses the notion of an operation for a monad, which he (20 years later) revisits with Jaskelioff in monad transformers as monoid transformers.
(This notion of operation is different from Plotkin and Power's notion of an algebraic operation for a monad, which amounts to a Kleisli arrow.)
I would highly recommend the book book by Bartosz Milewski "Category Theory for Programmers" which goes into some detail about Monads from a Category Theoretic perpective. And it's also available freely online :
https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/
How could monad transformers be described in the terms of category theory?
There are two definitions: the "weak" and the "functorial" one.
The "functorial" definition is that a monad transformer is "just a pointed endofunctor in the category of monads, what's the problem?".
This definition, however, does not describe the known transformers for the continuation monad, the codensity monad, and some other rarely used monads, because those transformers are not functors. Full details are worked out in Chapter 14 of the book "The Science of Functional Programming". https://github.com/winitzki/sofp
The "weak" definition is that a monad transformer should give a lawful monad T(M) for any monad M, and that there must exist a monad morphism M -> T(M). I will argue below that this definition is too weak to be adequate.
Let me expand on the "functorial" definition and answer the three questions posed initially.
What is a "pointed endofunctor in the category of monads"?
It is an endofunctor T that transforms an arbitrary monad M into another monad T(M) and an arbitrary monad morphism f : M -> N into another monad morphism T(f): T(M) -> T(N). (This function is sometimes called hoist.) The laws of monad and monad morphisms must hold.
In addition, T is “pointed”, meaning that there is a natural transformation lift: ID -> T, where ID is the identity endofunctor that maps each monad to itself: ID(M) = M.
The laws of functors and of natural transformations must hold for T and lift respectively.
Let us see how the natural transformation ID -> T works. This natural transformation's component at monad M is a morphism lift(M): ID(M) -> T(M) or equivalently M -> T(M), and this must be a lawful monad morphism since we are in the category of monads. The monad morphism M -> T(M) embeds the effects of M into the bigger monad T(M).
This expresses the intent of a monad transformer: to add some features to arbitrary monads M and obtain new “bigger” monads T(M) that have all the features of M and in addition some other features. Right now we have embedded M into T(M).
What is the "base monad" corresponding to T? Let us apply T to the identity monad (Id). The identity monad is defined by Id a = a. So, T(Id) is some other monad, which we may denote by L for brevity. This is what we call the "base monad" of T. Why? Because, as we will now see, there is a monad morphism L -> T(M) for any monad M.
Indeed, for any monad M we have a monad morphism Id -> M. (This is the “return” method.) Applying the functor T to this morphism, we get a monad morphism T(Id) -> T(M), or equivalently L -> T(M). In this way, we have embedded the base monad L into T(M).
To summarize, we have an endofunctor T and two monads L, M such that we can embed L -> T(M) and M -> T(M) via monad morphisms. So, in this sense, the “bigger” monad T(M) supports all the effects of L and also all the effects of M. We have succeeded in combining the effects of a monad L and an arbitrary monad M in a “bigger” monad T(M).
Now, the monad L is fixed for a given T but the monad M is arbitrary. So, if we want to be able to combine the effects of any two monads, we should have for any monad L the corresponding T such that T(Id) = L.
In practice, we have a certain limited set of known monads L for which we know how to construct the corresponding T. However, there is no general method for finding T given L.
Because transformers are pointed functors (in the category of monads), the functor composition of transformers is again a transformer. This explains why monad transformers compose even though monads do not.
What is a "monad transformer stack"? It is a composition of two or more monad transformers, acting on a monad M as T1(T2(T3(M))). The result is a functor that transforms a foreign monad M into a complicated, big monad T1(T2(T3(M))).
Suppose that each monad L has a single, fixed, designated transformer LT such that LT(Id) = L. Then we can pretend that we are able to mix any two monads L and M. Define the binary operation ** on monads by L ** M = LT(M). The operation (L **) is (for fixed L) the same as the endofunctor T in the category of monads, but it allows us to avoid writing T explicitly. Then we also find that the operation ** is associative. The associativity of ** means that we define the transformer of L1 ** L2 as L1T(L2T(M)). Then we can write monad stacks simply as K ** L ** M ** N without parentheses.
There are some remaining questions:
T where the morphisms M -> T(M) exist but L -> T(M) does not exist. Those transformers T are not actually endofunctors in the category of monads because there is no functor map T(f) on monad morphisms f: M -> N. Examples are the continuation monad and the codensity monad as well as some other rarely used monads.There are specific practical implications of the fact that some monads do not have functorial transformers. The implications are that those monads cannot be used at arbitrary places in monad stacks, because their effects cannot be lifted into the stack. To be able to use the monad stack, the continuation monad needs to be at the deep end of the stack (K ** L ** M ** Cont). The same applies to any monad that does not have a transformer.
This also implies that monad stacks may contain at most one monad that doesn't have a functorial transformer. Otherwise, programmers will be quite constrained in how effects are combined and lifted into the stack.
M -> T(M); the morphism L -> T(M) is not required. According to the "weak" definition, the continuation monad and the codensity monad do have transformers. In fact, there are no explicitly known monads that have no transformers by the "weak" definition.However, the requirement of having just M -> T(M) seems too weak. As a counterexample, let us define T(M) = Unit for all M. Then we will always have a monad morphism M -> T(M). So, the "weak" definition allows us to have nonsensical transformers (such as, transform all monads into the Unit type).
It is not clear how to relax the "functorial" definition of the monad transformer so that nonsensical transformers are excluded.
Is it really true that each monad L (defined by explicit purely functional code) has at least one corresponding transformer? This is an open research question but so far there are no known examples of monads without transformers, at least according to the "weak" definition.
How to construct a monad transformer for a given monad? The answer is a collection of 6 or 7 different recipes. There is no general construction that works in all cases. Manzuk's paper (referenced above) defines monad transformers via adjunctions but this does not actually give a working recipe in most cases.
There are several examples of monads with more than one transformer according to the "weak" definition. However, there are no examples of monads with more than one "functorial" transformer.
