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

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

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

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

Сообщества

Настроить S2

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



Пишет Journal de Chaource ([info]lj_chaource)
@ 2017-03-14 07:30:00


Previous Entry  Add to memories!  Tell a Friend!  Next Entry
Exponential-polynomial monads
Monadic functors represent computational contexts that can be linearly concatenated such that the later computational contexts may depend on the earlier ones. The defining properties of a monadic functor are the existence of two natural transformations
"point": Id ~> M  [that is, t ~> M t]
and
"join": M M ~> M [that is, M (M t) ~> M t].

All polynomial and recursive polynomial functors are monadic as long as they are pointed. (Of course, some monad implementations may be more interesting than others.) What about exp-polynomial functors? It is not easy to characterize those functors, except by building them up from simpler parts.

The simplest exp-polynomial functor is the Reader functor Reader t = c -> t where c is a fixed type. The Reader functor is monadic, and it can be generalized to monads of the form c -> M t where M is another monadic functor.

Statement 1. The functor F t = c -> M t is a monadic functor if M is monadic, where c is a fixed type.
Proof. The "join" map for F must have the type

F (F t) = (c -> M(c -> M t)) ~> F t = c -> M t.

Since we have c, we can obtain M(c -> M t). Now we can also map c -> M t into M t, using modus ponens with the same value of type c. Thus we can map M(c -> M t) into M(M t) and hence, using M-join, into M t.

The map t -> F t = t -> c -> M t is simply the M-point that ignores the "c" argument.
Q.E.D.

More complicated exp-polynomial functors are built as maps from contrafunctors. The simplest example of a contrafunctor is the "contra-representable" S t = t -> c (where c is a fixed type).

If S is a contrafunctor and A is a functor then S t -> A t is again a functor. The next statement uses a map from a contrafunctor to construct a new monad out of a given monad.


Statement 2. S t -> M t is a monadic functor if M is monadic and co-pointed (i.e. we have M t ~> t), and S is any contrafunctor.

Proof.
The natural transformation t ~> S t -> M t is simply the M-point that ignores the S t argument.

It remains to produce a natural transformation (S(S t -> M t) -> M(S t -> M t)) ~> S t -> M t.
The only way to get M t is to map from M(...) to M t. Since we have a value of type S t and no other value of type M(...), the only way to proceed is to obtain a value of M(S t -> M t) and then map to M(M t) using our value of S t. Now it remains to find a value of S(S t -> M t).
Since S is a contrafunctor, we can get S(S t -> M t) only if we can map S t -> M t into some x such that we have S x. The only value we actually have is S t. This value allows us to map (S t -> M t) into M t using modus ponens. By assumption, M is co-pointed, hence we can map M t -> t. Therefore, we can map (S t -> M t) into t. Since S is a contrafunctor, this allows us to map S t -> S(S t -> M t) and hence we obtain the required map.

Q.E.D.

The requirement that M be co-pointed seems to be significant. For example, M t = 1 + t is not co-pointed. The simplest nonconstant contrafunctor is S t = t -> c. Now, if we build the functor F t = S t -> M t = (t -> c) -> 1 + t, we find that F is not a monad (and not even an applicative functor).


Co-pointed monads are few and far between. (One nontrivial example of a co-pointed monad is a "non-empty list" functor.) It appears that there aren't many exp-polynomial monads!

One nontrivial example is the continuation monad Cont t = (t -> r) -> r where r is a fixed type. Note that the Cont monad cannot be derived using Statement 2 because the constant functor r is not a monad. It is significant that both fixed types in Cont are the same type "r": the functor F t = (t -> a) -> b is not a monad when "a" and "b" are different types! So generalizations are not possible in this direction.

Another nontrivial example is the state monad: State t = s -> (t × s). The type is isomorphic to (s->s)×(s -> t), which looks like a product of the Reader monad s -> t and a constant type s -> s. However, the value of type s -> s is used nontrivially in the monadic transformations. It does not seem likely that the State monad can be generalized to a wide class of exp-polynomial monads.

Yet another nontrivial example is the "density" monad D t = (t -> c) -> t and its generalization (M t -> c) -> M t for any monad M. The "density" monad satisfies the conditions of Statement 2 since t is a (trivially) co-pointed monad and S t = t -> c is a contrafunctor.

The reason why (M t -> c) -> M t is a monad is that D is an exp-poly monad of the class that admits a monad transformer that puts the foreign monad M inside,  -- that is, defining the transformed monad as D(M t). 

For the same reason, Cont(M t) = (M t -> c) -> c is always a monad for any monad M. 

Statement 1 can be seen as a particular case of the monad transformer construction for the Reader monad.

P.S.
In the previous post, I gave a construction of applicative functors that used a distributive contrafunctor. Now, I can't actually find examples of nonconstant distributive contrafunctors! Such contrafunctors S would have the property S(a × b) ~> S a × S b, or more simply, S (a × b) ~> S b.

For instance, S t = t -> c is not distributive since the required natural transformation has the type
S(a×b) -> S b= ((a×b) -> c) -> b -> c.
We can inhabit this type only if we can produce a value of "c" given a value of "b" and a function of type (a×b) -> c. However, the only way of producing a "c" is to have a×b, but we only have "b", not "a".

Do nonconstant distributive contrafunctors exist?


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