пост-монады

[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

[juan_gandhi]

Ну поздравляю!

Насчет же хендлеров - странно звучит. Мне кажется, что ZIO все это покрывает. Как и любая монада с частичными функциями в качестве Клайсли.

[amarao]

Я не могу говорить авторитетно и могу сослаться только на срачик по ссылке на форуме раста, где это всё упоминается (где-то с середины треда и дальше)

Но, ряд умных работ именно по effect handlers выглядит как что-то новое и exciting. Например, https://effekt-lang.org/, https://koka-lang.github.io/koka/doc/book.html

И вот рандомное из двухколоночного: https://kcsrk.info/papers/system_effects_feb_18.pdf

Вот что они пишут:

Effect handlers provide a modular alternative to monads [25, 35] for structuring effectful computations. They achieve the separation between operations and their handlers through the use of delimited continuations, allowing them to pause, resume and switch between different computations. They provide a structured interface for programming with delimited continuations [10], and can implement common abstractions such as state, generators, async/await, promises, non-determinism, exception handlers and backtracking search.

Я бы рад обсудить суть написанного, но не могу. Приходится ориентироваться на внешние признаки - "есть куча движухи".

Чёрт, я первый раз в жизни вижу "delimited continuations", а это целая большая тема.

[juan_gandhi]

Delimited continuations - странная штука, я не раз видел, как оно зверски помогает (скажем, секьюрити в твитерском коде, лет 10+ назад) - но сам никогда так и не освоил этот трюк.

Спасибо за линки; почитаю. Для меня, как для категорщика, монады очевидны, там математика и логика. А вот трюки я бы сначала перевел на категорный язык, а потом бы уже разбирал. Тем более, Карри-Хауард-Ламбек говорят нам, что больше ничего и нету, одни категории.

[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

[permeakra]

Монадки вполне удобны в использовании, они неудобны в сборке. Там нужно либо писать руками кастомную монадку для каждого набора эффектов, либо собирать из модулей-трансформеров и страдать, что общего метода композиции трансформеров не существует и для многих пар нужно писать кастомный код композиции. Т.е. к n трансформерам нужно n^2 бойлерплейта про их композицию.

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