Is there a monad that doesn't have a corresponding monad transformer (except IO)?
HaskellMonadsMonad TransformersCategory TheoryHaskell Problem Overview
So far, every monad (that can be represented as a data type) that I have encountered had a corresponding monad transformer, or could have one. Is there such a monad that can't have one? Or do all monads have a corresponding transformer?
By a transformer t
corresponding to monad m
I mean that t Identity
is isomorphic to m
. And of course that it satisfies the monad transformer laws and that t n
is a monad for any monad n
.
I'd like to see either a proof (ideally a constructive one) that every monad has one, or an example of a particular monad that doesn't have one (with a proof). I'm interested in both more Haskell-oriented answers, as well as (category) theoretical ones.
As a follow-up question, is there a monad m
that has two distinct transformers t1
and t2
? That is, t1 Identity
is isomorphic to t2 Identity
and to m
, but there is a monad n
such that t1 n
is not isomorphic to t2 n
.
(IO
and ST
have a special semantics so I don't take them into account here and let's disregard them completely. Let's focus only on "pure" monads that can be constructed using data types.)
Haskell Solutions
Solution 1 - Haskell
I'm with @Rhymoid on this one, I believe all Monads have two (!!) transformers. My construction is a bit different, and far less complete. I'd like to be able to take this sketch into a proof, but I think I'm either missing the skills/intuition and/or it may be quite involved.
Due to Kleisli, every monad (m
) can be decomposed into two functors F_k
and G_k
such that F_k
is left adjoint to G_k
and that m
is isomorphic to G_k * F_k
(here *
is functor composition). Also, because of the adjunction, F_k * G_k
forms a comonad.
I claim that t_mk
defined such that t_mk n = G_k * n * F_k
is a monad transformer. Clearly, t_mk Id = G_k * Id * F_k = G_k * F_k = m
. Defining return
for this functor is not difficult since F_k
is a "pointed" functor, and defining join
should be possible since extract
from the comonad F_k * G_k
can be used to reduce values of type (t_mk n * t_mk n) a = (G_k * n * F_k * G_k * n * F_k) a
to values of type G_k * n * n * F_k
, which is then further reduces via join
from n
.
We do have to be a bit careful since F_k
and G_k
are not endofunctors on Hask. So, they are not instances of the standard Functor
typeclass, and also are not directly composable with n
as shown above. Instead we have to "project" n
into the Kleisli category before composition, but I believe return
from m
provides that "projection".
I believe you can also do this with the Eilenberg-Moore monad decomposition, giving m = G_em * F_em
, tm_em n = G_em * n * F_em
, and similar constructions for lift
, return
, and join
with a similar dependency on extract
from the comonad F_em * G_em
.
Solution 2 - Haskell
Here's a hand-wavy I'm-not-quite-sure answer.
Monads can be thought of as the interface of imperative languages. return
is how you inject a pure value into the language, and >>=
is how you splice pieces of the language together. The Monad laws ensure that "refactoring" pieces of the language works the way you would expect. Any additional actions provided by a monad can be thought of as its "operations."
Monad Transformers are one way to approach the "extensible effects" problem. If we have a Monad Transformer t
which transforms a Monad m
, then we could say that the language m
is being extended with additional operations available via t
. The Identity
monad is the language with no effects/operations, so applying t
to Identity
will just get you a language with only the operations provided by t
.
So if we think of Monads in terms of the "inject, splice, and other operations" model, then we can just reformulate them using the Free Monad Transformer. Even the IO monad could be turned into a transformer this way. The only catch is that you probably want some way to peel that layer off the transformer stack at some point, and the only sensible way to do it is if you have IO
at the bottom of the stack so that you can just perform the operations there.
Solution 3 - Haskell
Previously, I thought I found examples of explicitly defined monads without a transformer, but those examples were incorrect.
The transformer for Either a (z -> a)
is m (Either a (z -> m a)
, where m
is an arbitrary foreign monad. The transformer for (a -> n p) -> n a
is (a -> t m p) -> t m a
where t m
is the transformer for the monad n
.
- The free pointed monad.
The monad type constructor L
for this example is defined by
type L z a = Either a (z -> a)
The intent of this monad is to embellish the ordinary reader monad z -> a
with an explicit pure
value (Left x
). The ordinary reader monad's pure
value is a constant function pure x = _ -> x
. However, if we are given a value of type z -> a
, we will not be able to determine whether this value is a constant function. With L z a
, the pure
value is represented explicitly as Left x
. Users can now pattern-match on L z a
and determine whether a given monadic value is pure or has an effect. Other than that, the monad L z
does exactly the same thing as the reader monad.
The monad instance:
instance Monad (L z) where
return x = Left x
(Left x) >>= f = f x
(Right q) >>= f = Right(join merged) where
join :: (z -> z -> r) -> z -> r
join f x = f x x -- the standard `join` for Reader monad
merged :: z -> z -> r
merged = merge . f . q -- `f . q` is the `fmap` of the Reader monad
merge :: Either a (z -> a) -> z -> a
merge (Left x) _ = x
merge (Right p) z = p z
This monad L z
is a specific case of a more general construction, (Monad m) => Monad (L m)
where L m a = Either a (m a)
. This construction embellishes a given monad m
by adding an explicit pure
value (Left x
), so that users can now pattern-match on L m
to decide whether the value is pure. In all other ways, L m
represents the same computational effect as the monad m
.
The monad instance for L m
is almost the same as for the example above, except the join
and fmap
of the monad m
need to be used, and the helper function merge
is defined by
merge :: Either a (m a) -> m a
merge (Left x) = return @m x
merge (Right p) = p
I checked that the laws of the monad hold for L m
with an arbitrary monad m
.
This construction gives the free pointed functor on the given monad m
. This construction guarantees that the free pointed functor on a monad is also a monad.
The transformer for the free pointed monad is defined like this:
type LT m n a = n (Either a (mT n a))
where mT
is the monad transformer of the monad m (which needs to be known).
- Another example:
type S a = (a -> Bool) -> Maybe a
This monad appeared in the context of "search monads" here. The paper by Jules Hedges also mentions the search monad, and more generally, "selection" monads of the form
type Sq n q a = (a -> n q) -> n a
for a given monad n
and a fixed type q
. The search monad above is a particular case of the selection monad with n a = Maybe a
and q = ()
. The paper by Hedges claims (without proof, but he proved it later using Coq) that Sq
is a monad transformer for the monad (a -> q) -> a
.
However, the monad (a -> q) -> a
has another monad transformer (m a -> q) -> m a
of the "composed outside" type. This is related to the property of "rigidity" explored in the question https://stackoverflow.com/questions/39649497/is-this-property-of-a-functor-stronger-than-a-monad?rq=1 Namely, (a -> q) -> a
is a rigid monad, and all rigid monads have monad transformers of the "composed-outside" type.
- Generally, transformed monads don't themselves automatically possess a monad transformer. That is, once we take some foreign monad
m
and apply some monad transformert
to it, we obtain a new monadt m
, and this monad doesn't have a transformer: given a new foreign monadn
, we don't know how to transformn
with the monadt m
. If we know the transformermT
for the monadm
, we can first transformn
withmT
and then transform the result witht
. But if we don't have a transformer for the monadm
, we are stuck: there is no construction that creates a transformer for the monadt m
out of the knowledge oft
alone and works for arbitrary foreign monadsm
.
However, in practice all explicitly defined monads have explicitly defined transformers, so this problem does not arise.
- @JamesCandy's answer suggests that for any monad (including
IO
?!), one can write a (general but complicated) type expression that represents the corresponding monad transformer. Namely, you first need to Church-encode your monad type, which makes the type look like a continuation monad, and then define its monad transformer as if for the continuation monad. But I think this is incorrect - it does not give a recipe for producing a monad transformer in general.
Taking the Church encoding of a type a
means writing down the type
type ca = forall r. (a -> r) -> r
This type ca
is completely isomorphic to a
by Yoneda's lemma. So far we have achieved nothing other than made the type a lot more complicated by introducing a quantified type parameter forall r
.
Now let's Church-encode a base monad L
:
type CL a = forall r. (L a -> r) -> r
Again, we have achieved nothing so far, since CL a
is fully equivalent to L a
.
Now pretend for a second that CL a
a continuation monad (which it isn't!), and write the monad transformer as if it were a continuation monad transformer, by replacing the result type r
through m r
:
type TCL m a = forall r. (L a -> m r) -> m r
This is claimed to be the "Church-encoded monad transformer" for L
. But this seems to be incorrect. We need to check the properties:
TCL m
is a lawful monad for any foreign monadm
and for any base monadL
m a -> TCL m a
is a lawful monadic morphism
The second property holds, but I believe the first property fails, - in other words, TCL m
is not a monad for an arbitrary monad m
. Perhaps some monads m
admit this but others do not. I was not able to find a general monad instance for TCL m
corresponding to an arbitrary base monad L
.
Another way to argue that TCL m
is not in general a monad is to note that forall r. (a -> m r) -> m r
is indeed a monad for any type constructor m
. Denote this monad by CM
. Now, TCL m a = CM (L a)
. If TCL m
were a monad, it would imply that CM
can be composed with any monad L
and yields a lawful monad CM (L a)
. However, it is highly unlikely that a nontrivial monad CM
(in particular, one that is not equivalent to Reader
) will compose with all monads L
. Monads usually do not compose without stringent further constraints.
A specific example where this does not work is for reader monads. Consider L a = r -> a
and m a = s -> a
where r
and s
are some fixed types. Now, we would like to consider the "Church-encoded monad transformer" forall t. (L a -> m t) -> m t
. We can simplify this type expression using the Yoneda lemma,
forall t. (x -> t) -> Q t = Q x
(for any functor Q
) and obtain
forall t. (L a -> s -> t) -> s -> t
= forall t. ((L a, s) -> t) -> s -> t
= s -> (L a, s)
= s -> (r -> a, s)
So this is the type expression for TCL m a
in this case. If TCL
were a monad transformer then P a = s -> (r -> a, s)
would be a monad. But one can check explicitly that this P
is actually not a monad (one cannot implement return
and bind
that satisfy the laws).
Even if this worked (i.e. assuming that I made a mistake in claiming that TCL m
is in general not a monad), this construction has certain disadvantages:
- It is not functorial (i.e. not covariant) with respect to the foreign monad
m
, so we cannot do things like interpret a transformed free monad into another monad, or merge two monad transformers as explained here https://stackoverflow.com/questions/18364808/is-there-a-principled-way-to-compose-two-monad-transformers-if-they-are-of-diffe - The presence of a
forall r
makes the type quite complicated to reason about and may lead to performance degradation (see the "Church encoding considered harmful" paper) and stack overflows (since Church encoding is usually not stack-safe) - The Church-encoded monad transformer for an identity base monad (
L = Id
) does not yield the unmodified foreign monad:T m a = forall r. (a -> m r) -> m r
and this is not the same asm a
. In fact it's quite difficult to figure out what that monad is, given a monadm
.
As an example showing why forall r
makes reasoning complicated, consider the foreign monad m a = Maybe a
and try to understand what the type forall r. (a -> Maybe r) -> Maybe r
actually means. I was not able to simplify this type or to find a good explanation about what this type does, i.e. what kind of "effect" it represents (since it's a monad, it must represent some kind of "effect") and how one would use such a type.
- The Church-encoded monad transformer is not equivalent to the standard well-known monad transformers such as
ReaderT
,WriterT
,EitherT
,StateT
and so on.
It is not clear how many other monad transformers exist and in what cases one would use one or another transformer.
- One of the questions in the post is to find an explicit example of a monad
m
that has two transformerst1
andt2
such that for some foreign monadn
, the monadst1 n
andt2 n
are not equivalent.
I believe that the Search
monad provides such an example.
type Search a = (a -> p) -> a
where p
is a fixed type.
The transformers are
type SearchT1 n a = (a -> n p) -> n a
type SearchT2 n a = (n a -> p) -> n a
I checked that both SearchT1 n
and SearchT2 n
are lawful monads for any monad n
. We have liftings n a -> SearchT1 n a
and n a -> SearchT2 n a
that work by returning constant functions (just return n a
as given, ignoring the argument). We have SearchT1 Identity
and SearchT2 Identity
obviously equivalent to Search
.
The big difference between SearchT1
and SearchT2
is that SearchT1
is not functorial in n
, while SearchT2
is. This may have implications for "running" ("interpreting") the transformed monad, since normally we would like to be able to lift an interpreter n a -> n' a
into a "runner" SearchT n a -> SearchT n' a
. This is possibly only with SearchT2
.
A similar deficiency is present in the standard monad transformers for the continuation monad and the codensity monad: they are not functorial in the foreign monad.
Solution 4 - Haskell
My solution exploits the logical structure of Haskell terms etc.
I looked at right Kan extensions as possible representations of the monad transformer. As everyone knows, right Kan extensions are limits, so it makes sense that they should serve as universal encoding of any object of interest. For monadic functors F and M, I looked at the right Kan extension of MF along F.
First I proved a lemma, "rolling lemma:" a procomposed functor to the Right kan extension can be rolled inside it, giving the map F(Ran G H) -> Ran G(FH) for any functors F, G, and H.
Using this lemma, I computed a monadic join for the right Kan extension Ran F (MF), requiring the distributive law FM -> MF. It is as follows:
Ran F(MF) . Ran F(MF) [rolling lemma] =>
Ran F(Ran F(MF)MF) [insert eta] =>
Ran F(Ran F(MF)FMF) [gran] =>
Ran F(MFMF) [apply distributive law] =>
Ran F(MMFF) [join Ms and Fs] =>
Ran F(MF).
What seems to be interesting about this construction is that it admits of lifts of both functors F and M as follows:
(1) F [lift into codensity monad] =>
Ran F F [procompose with eta] =>
Ran F(MF).
(2) M [Yoneda lemma specialized upon F-] =>
Ran F(MF).
I also investigated the right Kan extension Ran F(FM). It seems to be a little better behaved achieving monadicity without appeal to the distributive law, but much pickier in what functors it lifts. I determined that it will lift monadic functors under the following conditions:
-
F is monadic.
-
F |- U, in which case it admits the lift F ~> Ran U(UM). This can be used in the context of a state monad to "set" the state.
-
M under certain conditions, for instance when M admits a distributive law.