Is there a monad that doesn't have a correspon

问题:

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.)

回答1:

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.

回答2:

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.

回答3:

My solution exploits the logical structure of Haskell terms. Everyone knows that a function in Haskell with return type t can be turned into a monadic function with return type (Monad m) => m t. Therefore if the "bind" function could have its program text "monadified" appropriately, the result would be a monad transformer.

The sticking point is that there is no reason why the "monadification" of the "bind" operator should satisfy the laws, particularly associativity. This is where cut-elimination comes in. The cut elimination theorem has the effect on a program text of inlining all let-bindings, case-analyses, and applications. Also, all computations on a particular term end up being performed in one place.

Since the type parameters of "bind" are rigid, the uses of the right-hand side of "bind" are indexed by their return values. The terms end up in positions in the returned structure that make "bind" associate, therefore the uses of the right-hand side must be associative in the "monadified" "bind," and the resulting structure is a monad.

This is really wooly, so here is an example. Consider the following strict list monad:

rseq x y = case x of
    x:xs -> (x:xs) : y
    [] -> [] : y


evalList (x:xs) = rseq x (evalList xs)
evalList [] = []

instance Monad [] where
    return x = [x]
    ls >>= f = concat (evalList (map f ls))

This order of evaluation leads to the standard ListT (not really a monad). However, by cut elimination:

instance Monad [] where
    return x = [x]
    ls >>= f = case ls of
        [] -> []
        x:xs -> case f x of
            y:ys -> (y:ys) ++ (xs >>= f)
            [] -> [] ++ (xs >>= f)

This provides the exact evaluation order to be "monadified."

---

In response to Petr Pudlak:

If the type of the monad in question is some function type (it is convenient to Church-encode all data types), then the function type is converted by decorating all return values of the type with the transformed monad. This is the type portion of monadification. The value portion of monadification lifts pure functions using "return," and combines them with uses of inhabitants of the monad type using "bind," preserving the evaluation order of the original program text.

The strict list monad was given as an example of an evaluation order that does not compose associatively, as witnessed by the fact that ListT uses the same evaluation order as the strict list monad.

To complete the example, the Church encoding of the list monad is:

data List a = List (forall b. b -> (a -> List a -> b) -> b)

Monadified, it becomes:

data ListT m a = ListT (forall b. m b -> (a -> List a -> m b) -> m b)

cons x xs = \_ f -> f x xs

nil = \x _ -> x

instance (Monad m) => Monad (ListT m) where
    return x = cons x nil
    ls >>= f = ls nil (\x xs -> f x >>= \g ->
        g (liftM (nil ++) (xs >>= f)) (\y ys -> liftM (cons y ys ++) (xs >>= f))

To elaborate on the above, the cut elimination step forces all values to be consumed using a stack discipline, ensuring that the order of results in the structure matches the evaluation order -- this comes at the price of potentially running the same action many times.

[Technically, what you need is a cut elimination of approximants: A is a cut elimination (of approximants) of B, iff for every finite approximant of B, there is a finite approximant of A such that A is a cut elimination of B.]

I hope that helps.