Войти в систему

Home
    - Создать дневник
    - Написать в дневник
       - Подробный режим

LJ.Rossia.org
    - Новости сайта
    - Общие настройки
    - Sitemap
    - Оплата
    - ljr-fif

Редактировать...
    - Настройки
    - Список друзей
    - Дневник
    - Картинки
    - Пароль
    - Вид дневника

Сообщества

Настроить S2

Помощь
    - Забыли пароль?
    - FAQ
    - Тех. поддержка



Пишет Journal de Chaource ([info]lj_chaource)
@ 2017-03-09 01:32:00


Previous Entry  Add to memories!  Tell a Friend!  Next Entry
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 Twill 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).


(Читать комментарии) (Добавить комментарий)