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

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

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

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

Сообщества

Настроить S2

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



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


Previous Entry  Add to memories!  Tell a Friend!  Next Entry
The center-of-mass monad
While studying monads, I stumbled upon the following functor:

G t = (t -> r) -> t

This functor can be interpreted as giving a "center of mass" of a space according to a weight function: assume that t comes from a vector space, that f : t -> r is a weight function where r is a number, and that we compute the center of mass by integrating over all vector space with the weight function f. The result is a certain point t in the space, which is the result of evaluating G t on a weight function f.

Regardless of the usefulness of this interpretation, it was fascinating to find that G t is actually a monad.

To see this, we need to define two natural transformations:

pure : t ~> G t

join : G (G t) ~> G t

Defining "pure" is straightforward: just return a constant function _ -> t that ignores its argument.

Defining "join" is more difficult. The type of "join" is written out as

join : ((((t->r)->t) -> r) -> (t->r)-> t) -> (t->r) -> t

We are required to produce a value of t, given a function h of type (((t->r)->t) -> r) -> (t->r)->t and a function f of type t->r. The only way of producing a value of t would be to use h on two arguments: one of type ((t->r)->t) -> r and another of type t->r. We already have a value f of type t->r. It remains to produce a function of type ((t->r)->t) -> r; in other words, to produce r given a value g of type (t->r)->t. We now evaluate g f to obtain a value of type t, and finally apply f to that value. Hence, f (g f) has type r as required.

All this verbiage is equivalent to the terse Haskell syntax

join gg = \f -> gg (\g -> f (g f)) f

It remains to verify that the monadic laws hold. There are three laws: left unit, right unit, and associativity, which are roughly written as.

pure . join = id
join . G(pure) = id
join . G(join) = join . join -- that is, G(G(G t))) can be reduced to G t via "join" in two different ways, which must be equivalent.

Here G(f) is the lifting of a function f into the functor G.

Verifying these laws is a somewhat tedious calculation that involves substituting "join" into itself several times.

As a generalization of these calculations, we can also show that the functor (M t -> r) -> M t is a monad if M is a monad.

This suggests a "monad transformer"

G : M t ~> (M t -> r) -> M t

As simpler cases, consider also that c -> M t and M(c -> t) are monads if M is one.


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