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

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

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

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

Сообщества

Настроить S2

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



Пишет Journal de Chaource ([info]lj_chaource)
@ 2018-03-04 07:49:00


Previous Entry  Add to memories!  Tell a Friend!  Next Entry
The ubiquitous premonads: The simplest way to formulate monad laws
Monad laws are usually formulated in terms of the `bind` function that has 3 laws together with the `return` function. However, this formulation is both unintuitive (it's hard to remember the laws) and too strong: the `return` function is not necessary in most practical cases.

Consider the `join` function instead. The `join` has the type `M (M a) -> M a` and needs to be a natural transformation.

It turns out that this single requirement (what I earlier called "pre-monadic") is actually sufficient for practical purposes. There is no need to introduce `return` or to require any more laws.

The associativity law for `join` states that reducing `M (M (M a))` to `M (M a)` and then to `M a` gives the same results whether we first reduce the outer pair of `M`'s or the inner pair.

fmap join . join = join . join

I always thought that this was a separate law.
However, now it seems that it is a consequence of naturality for `join`:

fmap h . join = join . h

I will need to check some examples to become fully convinced, but so far this seems to be correct.
If so, this significantly simplifies checking the laws for monads. It is quite cumbersome to check the associativity law because of the (usually) complicated type `M (M (M a))`. On the other hand, naturality is perfectly obvious in most cases.

In my previous posts I have found that a large class of functors admits a natural transformation with the type signature of `join`. I thought that I would have to check associativity additionally. Now it appears that it is not necessary.

For instance, all polynomial functors admit a natural transformation with the type signature of `join` (the type can be inhabited). It follows that all polynomial functors are pre-monadic, with the associativity law holding automatically. It's a great simplification that the associativity law does not need to be proved.

Update: This is a mistake! Associativity does not follow from naturality. I mixed up the types of functions in the naturality property. It must be fmap (fmap h) . join = join . fmap h; also I found a counterexample where naturality holds but associativity does not.

The reason for not including `return` is that, in many practical cases, `return` is not directly useful for coding. Most monads have several additional constructors and methods necessary for using them; having just `return` would be far insufficient.

For instance, the `List` monad has constructors from any number of values (not just one), and also methods such as `append` or `concat`. Having `return` for a `List` means constructing a list of one element only; this would be insufficient for practical use of `List`.

Any "validation-like" monad has constructors for success and failure; having only `return` as a constructor for success values would be insufficient for practical use.

Therefore, insisting on `return` but omitting any other constructors does not serve much practical purpose. It is perhaps mathematically more elegant because it makes connection with monoids, but that's about it.

A proper premonad that has only `join` but no `return` is related to a Kleisli semigroupoid (as opposed to a Kleisli category for full monads).

I found some use cases for premonads. The simplest one is the `Writer` premonad.

The standard `Writer` monad is the type constructor `W m a = (m, a)`, considered as a functor in `a`, where `m` is a monoid type. Now, replace monoid with semigroup. Then we can still define `join` as before, with all properties holding since `join` is a natural transformation in `a`:

join (m1, (m2, a)) = (m1 `combine` m2, a)

The `combine` method must obey semigroup laws but may not be a monoid if it does not admit an identity element. A simple example of the `combine` method that gives a semigroup but not a monoid is

combine1 m1 m2 = m1

or

combine2 m1 m2 = m2

It is easy to see that no identity element can be found here.

A use case for this is a chain of computations that need to trace the time spent in the entire chain.
The values `m` represent timestamps, and "combining" them using `combine1` or `combine2` will trace the initial time or the final time. This is certainly a useful example of using a premonad that cannot be made into a full monad.


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