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

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

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

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

Сообщества

Настроить S2

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



Пишет Journal de Chaource ([info]lj_chaource)
@ 2017-04-15 23:46:00


Previous Entry  Add to memories!  Tell a Friend!  Next Entry
Monads and monad transformers: The errors of my ways
After going to BayHac 2017 and talking to a few knowledgeable people, I identified some errors in my previous understanding of monads and monad transformers.

1. A constant functor cannot be a monad unless it is a constant unit.

Previously I talked about constant monad functors of the form M t = c, where c is a constant monoid type. I did not realize that this can be a monad only if c = 1.

The reason is that the Kleisli arrow for the constant functor has the form a -> M b = a -> c and does not depend on the type b. Therefore, the right identity law cannot be satisfied: the Kleisli identity arrow is a -> c0, and the right composition of this with any Kleisli arrow is again a -> c0, which loses the information in that Kleisli arrow.



2. The Outside monad transformer does not work correctly for recursive polynomial monads. A special "recursive" version of the Outside transformer must be used, similar to the Free monad transformer.

This seems to be a nontrivial discovery made in 2012: the Haskell standard library had an incorrect ListT monad transformer for the List monad. https://wiki.haskell.org/ListT_done_right

The incorrect ListT monad transformer was the Outside transformer constructed for the List monad. While the type of the monadic operation can be inhabited, the monad associativity law does not hold. The correct construction is to put the foreign monad on the outside within the recursion, like in the Free monad transformer.

Here is how it works. The Free monad transformer is defined as

T<sub>F</sub> L = L∘(Id + F∘(T<sub>F</sub> L)

In this construction, the foreign monad L is on the outside of the recursion step, rather than on the outside of the entire recursive monad.

Similarly, the correct monad transformer for a recursive polynomial monad M defined by

M t = Fix<sub>x</sub> G x t

or more briefly M = Fix<sub>x</sub> G x


is

T<sub>M</sub>L = Fix<sub>x</sub> L∘(G x).

3. Adjunctions do not help in producing monad transformers, beyond the special cases of State and Continuation monads.

Any monad M can be seen as coming from an adjunction (F, U) as M = U∘F. However, if we are to represent the functors U and F as type constructors in our programming language, we seem to have only two choices: F and U can be either functors or contrafunctors, and the categories in the adjunction must be either the main category of types of our programming language or its opposite category. The first choice always gives the State monad, the second - the Continuation monad. It seems that adjunctions (understood concretely in terms of type constructors of the programming language, rather than as functors between any two imaginary categories) will not give much more help in constructing monad transformers or monads.


Here is a simple argument to show why only the State monad can be obtained from an adjunction between two functors within the same category.

If F and U are two adjoint functors, we have an isomorphism between Hom-sets (F a -> b) and (a -> U b).
Set a = 1: we get F 1 -> b isomorphic to 1 -> U b = U b. Therefore, U is the "Reader" functor r -> b for some constant type r = F 1. The functor adjoint to Reader is Writer, t×r (this must be checked separately). Since adjoint functors are unique up to isomorphism, F must be the Writer functor F t = t×r. Hence, the monad U∘F is M t = U(F t) = r -> t×r. This is the State monad with the state type r.

The monad transformer for the State monad is indeed obtained as the Adjoint transformer. The Inside monad transformer might exist for the State monad, - the necessary types are inhabited. It remains to be seen whether the Inside transformer for the State monad satisfies the correct laws (which I did not check!).

4. Composable effects and free monads may give a better way of composing monads in practice than monad transformers.

I'd like to investigate this further.
The main paper is "Freer monads, more extensible effects". http://okmij.org/ftp/Haskell/extensible/  
A Scala implementation is https://github.com/ProjectSeptemberInc/freek and https://github.com/ISCPIF/freedsl
https://www.reddit.com/r/scala/comments/4mngtz/free_monads_using_freek/


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