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 Is this property of a functor stronger than a monad? 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 transformer t to it, we obtain a new monad t m, and this monad doesn't have a transformer: given a new foreign monad n, we don't know how to transform n with the monad t m. If we know the transformer mT for the monad m, we can first transform n with mT and then transform the result with t. But if we don't have a transformer for the monad m, we are stuck: there is no construction that creates a transformer for the monad t m out of the knowledge of t alone and works for arbitrary foreign monads m.
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 monad m and for any base monad Lm 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 Is there a principled way to compose two monad transformers if they are of different type, but their underlying monad is of the same type?
- 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 as m a. In fact it's quite difficult to figure out what that monad is, given a monad m.
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 transformers t1 and t2 such that for some foreign monad n, the monads t1 n and t2 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.
