|
| |||
|
|
Monad transformers for exp-polynomial monads II The goal is to find exp-poly monads M that are transformable. A monad M is transformable if, for any monad L, we have a natural transformation L(M x) ~> M(L x). For these monads M, we can write a monad transformer as TML = M°L. To build an exp-poly monadic functor inductively, we need to consider how to combine simpler functors while keeping the property of being transformable. It turns out that Lemma M. The following properties hold: 1. A constant functor, M t = c, is transformable if M is itself a monad. 2. The identity functor, M t = t, is transformable. 3. If M and N are transformable then M × N is also transformable. 4. If M is transformable and S is any contrafunctor then S t -> M t is transformable. 5. If M is transformable then M + Id is transformable, where M + Id is a monad defined similarly to 1 + Id. Proof. 1. For a constant functor, we need the transformation L c ~> c. We cannot assume that L is co-pointed. However, M is a monad, therefore we have a transformation t -> M t; hence we have t -> c for any t, so set t = L c and we have Lc ~> c. 2. The identity functor, M t = t, is trivially transformable. 3. In case M and N are transformable, we need to transform L°(M × N) ~> M°L × N°L. Due to L being a functor, we have L°(M × N) ~> L°M × L°N. By assumption that M and N are transformable, we also have L°M ~> M°L and L°N ~> N°L. This yields L°M × L°N ~> M°L × N°L as required. 4. In case M is transformable and S is a contrafunctor, we need to transform L°(S -> M) ~> (S°L -> M°L). Since L is a monad, we have Id ~> L. Since S is a contrafunctor, we have S°L ~> S°Id = S. Thus, it is sufficient to transform L°(S -> M) ~> (S -> M°L), or more verbosely, to find a natural morphism L(S t -> M t) -> S t -> M(L t). Since L is a functor, we can transform L(x ->y) -> x -> L y. Hence, we get L(M t). By assumption, M is transformable, hence L(M t) ~> M(L t) exists, and we get finally L(S t -> M t) -> S t -> M(L t) as required. Alternatively, under an additional assumption that S allows us to have a natural transformation S°L ~> L°S, we get L°(S -> M) ~> (L°S -> L°M) using the applicative property of L, that is, L(x -> y) -> L x -> L y, and finally sequence L°M -> M°L. 5. In case M is transformable and M + Id is a monad, we need to transform L°(M + Id) ~> M°L + L, or more verbosely, L(M t + t) ~> M(L t) + L t. First we transform M t + t ~> M t using the M-point t ~> M t; then we sequence the functors L°M ~> M°L by assumption of transformability of M. Note that this always yields the left variant of M(L t) + L t. Q.E.D. Lemma M lists five operations that build up a monad out of simpler functors. As long as a monad M is constructed via these operations, its monad transformer TM will exist as TML = M°L. Perhaps not all exp-polynomial monads can be constructed in this way. It remains to be seen whether a different trick can be used in order to construct monad transformers for a wider class of exp-polynomial monads. I haven't seen any examples of that yet. The Haskell Wikibook mentions specific monad transformers for the State monad and for the Continuation monad. State t = c -> (c×t) where c is a constant type; Cont t = (t -> r) -> r where r is a constant type. Both of these monads are exp-polynomial and covered by Lemma M, but their transformers are not constructed according to the systematic recipe I outlined: they are neither TML = M°L nor TML = L°M. According to the Wikibook: Transformer for State is TStateL = c -> L(c×t). Transformer for Cont is TContL = (t -> L r) -> L r. It remains to be seen why these transformers are chosen in that way, and whether transformers created with the systematic recipe TML = M°L work differently or not at all. At the moment, I don't understand why the Haskell Wikibook's defines these transformers in this way (which it doesn't explain). |
||||||||||||||