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

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

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

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

Сообщества

Настроить S2

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



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


Previous Entry  Add to memories!  Tell a Friend!  Next Entry
Monad transformers and free monads
Monads do not always compose: if M and L are arbitrary monads then neither ML nor LM will be a monad in the general case. However, being able to compose monads is very useful: for example, one monad may describe database transactions while another represents reading from the Web, and so we would like to write monadic code that reads from the Web and writes the results into a database. The type of this program would be some sort of composition of the two monads, because the code must express an arbitrary combination of both effects. In order to be able to write such code, ideally we would like to be able to compose two arbitrary monads.

One way to compose monads is through monad transformers. A monad transformer for a monad M is a functor of functors TM that, for any monad L, yields a natural transformation L ~> TML, which creates a new monad TML such that there exists a natural embedding transformation L ~> TML. (These natural transformations must commute with the monads' defining natural transformations, in an appropriate sense; see https://en.wikipedia.org/wiki/Monad_transformer for precise conditions.) 

It is not obvious how to construct a monad transformer TM for a given monad M. I couldn't find a general construction. All "nice" monads have a monad transformer; is there an example of a monad for which no monad transformer exists? Here is a paper with a more abstract view of monad transformers; but it also does not seem to offer a systematic derivation of transformers from monads.

So far, I found four specific classes of monads M for which a monad transformer can be constructed systematically. I call these transformers Outside, Inside, Free, and Adjoint transformers.

1. The Outside transformer exists for any (recursive-)polynomial monad M and is defined as the composition TML = LM, with the "foreign" monad L on the outside of the type expression.

The List monad,

List t = 1 + t × List t,

and the Maybe (a.k.a. Option) monad, M t = 1 + t, are classic examples of (recursive-)polynomial monads, and the Outside transformer is standard for them.

2. The Inside transformer exists for a certain limited class of of exponential-polynomial monads M, and is defined as the composition TML = ML, with the "foreign" monad L on the inside.

Examples of suitable monads are Reader, Writer, and State monads, as well as any monad of the form S t -> t where S is a contrafunctor. The product of any two such monads is again a monad of the same class; I studied their properties in more detail in a previous post.

It is interesting that the Continuation monad (t -> r) -> r does not have an Inside transformer. The (practically extremely useful) "Future" monad can be seen formally as a particular case of the Continuation monad with r = 0, and so it does not have an Inside transformer. (Neither does it have an Outside transformer.)

3. The Free monad transformer exists for the free A-monad, where A is any functor (see http://www.haskellforall.com/2012/07/free-monad-transformers.html and https://github.com/ekmett/free/issues/3).
The free A-monad is defined recursively as the functor F = Id + AF, or if we write this type equation using an explicit type parameter t,
F t = t + A(F t).

Statement. The Free transformer defined recursively as

TFL = L(Id + A∘TFL)

defines a monad for any monad L.

Proof.
Writing out the type parameter t and denoting TFL for brevity by T, we have the recursive type equation

T t = L (t + A(T t)),

where the occurrence of T in the right-hand side can be already assumed to have the monadic properties by induction.

The embedding transformation L ~> T is defined by embedding into L(Id + 0). To establish the monadic property TT~>T, we use the existing natural transformations LL~>L and Id ~> L, and consider that we would like to obtain the following chain of natural transformations

TT = L(T t + A(T(T t))) ~> L(t + A(T t)).

Note that we can transform T(T t) ~> T t by using the inductive assumption. The difficult part is the argument of L, which is a disjunction. We cannot transform L(x+y)~> ... + ... because L is not necessarily co-distributive. Instead, we need to map this disjunction to some other type. We use the following trick: transform

A (T t) = 0 + A(T t) ~> L(0 + A(T t))

where the last step uses the L-point transformation (r ~> L r). The result is that we have transformed A(T t) into a value of type T t. Therefore we can write the transformation

T t + A(T t) ~> T t + T t ~> T t (this is just the disjunction of identity transformations T t ~> T t),

and finally we obtain the chain of natural transformations

TT = L(T t + A(T(T t))) ~> L(T t + A(T t)) ~> L(T t + T t) ~> L(T t) = L(L(t + A(T t)) ~> L(t + A(T t)) = T t.

Hence we have transformed TT~>T as required.
Q.E.D.

Note that the Free A-monad transformer is not itself a free monad of any functor. (Also, neither the free AL-monad nor the free LA-monad yields monad transformers that satisfy the required laws!) The resulting transformed monad TFL does not itself automatically have a monad transformer. As a result, it is not clear how to combine two monads that have been transformed with two different Free transformers.

As an aside - it has been fashionable recently to combine free monads using co-products (disjnctions) of functors. For two functors A and B, one combines the free A-monad and the free B-monad by considering the free (A+B)-monad. In this way, we can compose any number of free monads; but the old problems return as soon as we need to mix in a few non-free monads.

4. Finally, the Adjoint transformer exists for monads that are obtained from adjunctions. An adjunction is a pair of functors (F, U) that satisfy certain properties (which I still need to study in more detail before I can translate them into the language of functional type theory). Among those properties are these: the composition FU is a monad, and the reverse composition UF is a comonad. So, if M is a monad for which we know the explicit adjunction (F, U) such that FU = M, then the Adjoint monad transformer for M is defined by

TML = FLU.

[ https://oleksandrmanzyuk.files.wordpress.com/2012/02/calc-mts-with-cat-th1.pdf ]

The monadic property (TML)(TML)~>(TML) is easy to verify since we have natural transformations UF ~> Id (since UF is a comonad) and LL ~> L (since L is a monad). Thus we find a chain of natural transformations
(TML)(TML) = FLUFLU ~> FLLU ~> FLU = TML.

It appears plausible that the transformers of the first three types are particular cases of the fourth, once we find an appropriate adjunction. For instance, examples of adjunctions often involve a forgetful functor. In the language of bare types (when we forget all subcategories), a forgetful functor is simply an identity functor. So, an adjunction (F, U) with F = Id means that U is itself a monad (and a comonad), and that the Adjoint monad transformer for F is TUL = FLU=LU. This is exactly the same as the Outside monad transformer. Similarly, an Inside monad transformer is obtained from an adjunction (F, U) with U = Id.

This level of generality is elegant but does not give us a systematic procedure for writing a monad transformer corresponding to a given specific monad, such as M t = 1 + t or M t = (1 + t -> r) -> t.

For instance, what adjunction (F, U), if any, underlies the Continuation monad?

Another open question is whether monad transformers are unique. The Inside monad transformer for the State monad, s -> s × M(t),  is not the same as the Adjoint transformer s -> M(s × t). In this case, the Outside transformer is stronger (can be mapped onto the Adjoint transformer, but not vice versa). What is the significance of this?


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