пост-монады

[amarao]

Говорят, монадки уже не модны (ибо IRL крайне неудобны в использовании), а вместо них грядут ещё более головоломные effect handler'ы. Я попытался послушать про них, но там уровень, на котором не хватает базового бэкграунда, чтобы понимать punch line у докладчиков.

Если пересказать в режиме "мойша напел", то effect handler'ы - это обобщение теории типов на сайд-эффекты, в которых эксепшены (и прочие сайд-эффекты) описываются в рамках модели (видимо, уже не типов), и позволяют компилятору делать выводы относительно происходящего, а авторам кода - накладывать ограничения на то, что именно происходит. Они покрывают собой эксепшены, но не только, и являются обобщением понятия.

Всё остальное надо слушать не в моём исполнении.

А ещё, мне первый раз объяснили, что такое монады. И я первый раз понял.

Это не rust-код (т.к. Self не может иметь типопараметр), но суть передаёт.

trait Monad<A> {

fn flat_map<B>(self, f: fn(A) -> Self<B>) -> Self<B>;

fn new(a: A) -> Self<A>;

}

(отсюда: https://users.rust-lang.org/t/please-tell-me-yeet-is-not-a-thing-in-rust/84843/47)

Comments

[yurikhan]

Монадка — это не только наличие методов return и (bind или flatmap). Это ещё немножко аксиом, которым они должны удовлетворять.

[amarao]

Они - это методы или монадки?

Я думал, что всё что нужно для практических целей выписано в сигнатурах, а если речь про теоретические доказательства, что так можно делать, то оно осталось в головах (и умных двух-трёхколоночных статьях), а все остальные наслаждаются результатами.

А что такое "аксиома" в коде?

[yurikhan]

Они — это реализации методов.

Аксиома в коде — это требования. Проще всего, наверно, объяснить на примере сортировки. Алгоритм сортировки в стандартных библиотеках многих языков принимает аргументом массив элементов и предикат сравнения. Формальная сигнатура предиката — (T, T) → bool, но это не вся история. В документации на алгоритм сказано, что предикат должен вести себя по меньшей мере как строгий слабый порядок:

1. Аксиома нерефлексивности: ни для какого x типа T не выполняется less(x, x).
2. Аксиома антисимметричности: если для двух x, y типа T выполнено less(x, y), то не может быть одновременно less(y, x).
3. Аксиома транзитивности: если для трёх x, y, z типа T less(x, y) и less(y, z), то less(x, z).
4. Аксиома транзитивности эквивалентности: если для трёх x, y, z типа T !less(x, y) && !less(y, x) && !less(y, z) && !less(z, y), то !less(x, z) && !less(z, x).

Если предикат не удовлетворяет какой-нибудь из аксиом строгого слабого порядка, то задача сортировки по нему не имеет смысла и алгоритм не гарантирует предсказуемого поведения, в частности, может зацикливаться.

Аналогично, технически можно определить контейнер, return и flatmap и попробовать заявить, что это монада, но если return(x).flatmap(f) != f(x), или xs.flatmap(return) != xs, или (xs.flatmap(g)).flatmap(h) != xs.flatmap(lambda x: g(x).flatmap(h)), то пользователи и сторонние библиотеки, ожидающие монаду, будут сильно удивлены и, может быть, даже потрясены.

(вольный пересказ с https://wiki.haskell.org/Monad_laws)

[sab123]

Я про монад уже двно объяснял популярными словами: https://babkin-cep.blogspot.com/2014/07/monads.html