Монада получила форму: в монаде разворачивается в разбор до конца разбора

Пункт 3 плана. Полиморфизм сделал монаду выразимой ТИПОМ; здесь сделана
ФОРМА — объявление `монада`, блок `в монаде`, доказательство устройства и
проверка трёх законов связывания на сетке.

    монада «Возможно» от «А»
      возврат «Обернуть»
      соединение «Сплющить»

    тотальная функция «Итог со скидкой»
      принимает номер: число
      возвращает «Возможно» от числа
      в монаде «Возможно»
        пусть цена равно «Цена позиции» от номер
        пусть скидка равно «Скидка по цене» от цена
        возврат цена минус скидка

Обещание плана «функций первого класса ей не нужно, потому что тело известно
синтаксически» выполнено буквально — и оказалось не самоочевидным. Связывание
`связать(м, к) = соединение(отобразить(к, м))` требует, чтобы `к` было
значением, а у продолжения есть свободные имена, которых тег не захватывает
(частичного применения нет). Выход в том, что `к` НЕ СТРОИТСЯ: отображение
эндофунктора печатается НА МЕСТЕ, разбором по вариантам типа, и тело стоит
прямо в ветви. Замыкать нечего, потому что это выражение, а не функция.

Отображение никто не объявляет: у полиномиального функтора законное отображение
ровно одно, и компилятор выводит его из устройства типа. Поэтому строки
`эндофунктор «Возможно»` из контракта здесь нет — она повторяла бы имя строкой
выше и не проверяла ничего, — а функториальность ДОКАЗАНА построением.

Разворачивание сделано внутри разбора, и это главное решение: наружу парсера
форма не выходит вовсе. Печать во все восемь целей, анализ завершаемости и обе
реализации самоприменения получили её даром — `self/parser.flang` и
`self/types.flang` не потребовали НИ ОДНОЙ правки. В `self/lexer.flang` дописаны
четыре поверхности в таблицу слов, потому что таблица сверяется тестом
поверхность в поверхность; разбирать их лексеру не нужно, и он не разбирает —
ровно как с `моноид`.

Новых ключевых слов четыре: `монада`, `возврат`, `соединение`, `в монаде`. Голых
вхождений в 133 исходниках — ноль, и проверено это не только `grep`-ом: все 133
файла размечены новым лексером, ни один новый идентификатор не сработал ни разу.
Слово `вернуть` для строки-результата ОТВЕРГНУТО измерением — `пусть вернуть
равно` стоит голым в examples/rosetta/towers-of-hanoi.flang; роль взял `возврат`,
и это вышло лучше замены: `возврат «Обернуть»` называет η, `возврат выражение`
её применяет.

Граница проведена явно. ДОКАЗЫВАЕТСЯ сличением объявлений: тип параметричен,
параметр у него есть, `возврат` ведёт из «А» в M«А», `соединение` из M(M«А») в
M«А», параметр стоит в полях целиком, блок без `возврат` не собирается.
ПРОВЕРЯЕТСЯ на конечной сетке из примеров автора: левая единица, правая
единица, ассоциативность связывания — с контрпримером в сообщении, как у
моноида.

Три измерения про законы, ни одно не было ожидаемым:

  1. у «Возможно» ассоциативность отдельно сломать НЕЛЬЗЯ — единицы задают
     `соединение` на всех трёх входах целиком, свободы не остаётся;
  2. перепутанный порядок склейки у монады-писателя — НЕ ошибка: противоположный
     моноид тоже моноид, законы правы, а ловится это примером. Записано тестом,
     чтобы никто не «починил» проверку под ожидание;
  3. значит ассоциативность ловит то, чего не ловят единицы, только на операции
     с нейтралью, но без ассоциативности. В тесте это `а плюс б плюс а·б·(а−б)`:
     ноль нейтрален точно, а перестановка скобок даёт 37 против 5.

Второй дефект нашёл ЗАПУСК, а не проверка. Отображение пересобирает вариант
целиком, значит соседние поля надо связать и подставить обратно; связывались они
под своими же именами — и молча крали имена у автора. Функция с параметром
`метка` над монадой с полем `метка` получала в теле блока метку из-под варианта:
«ш7» вместо «снаружи7». Типы совпадали, поэтому проверка молчала; законы говорят
о значениях, а не об именах, и тоже молчали бы. Отвергать такую программу было
бы произволом — как называются поля ВНУТРИ монады, автор знать не обязан, — и
переименовывается копия, а не программа: `метка`, `метка 2`, `метка 3`. Улика —
два теста, столкнутые с обеих сторон.

Первый дефект нашёлся раньше, и не в монаде. Программа-пример написана на
ДВУХ монадах, вторая — на типе с двумя параметрами, по правилу из POLY.md
(«новая форма не проверена, пока на ней не написана настоящая программа»).
Блок над ней не собирался: у конструктора «Успех» параметр «Значение» решается
полем, а «Беда» — ничем, и ожидание, которое её знает, не доезжало — `callType`,
`constructType` и `recordType` гасили его в null, как только тип аргумента или
поля оказывался параметрическим. Починено тремя местами: ожидание участвует и ДО
аргументов, но только как ПОДСКАЗКА вложенному выводу, в `matchAgainst` и
`sameType` оно по-прежнему не входит. Отсюда свойство правки: принять она может
больше прежнего, отвергнуть — ровно столько же.

Мерено, а не оценено:

  AST всех 133 исходников репозитория напечатан до и после — расхождений 0;
  все 133 размечены новым лексером — новых ключевых слов сработало 0;
  self-types.test.mjs (46 тестов, включая порченые файлы и фаззинг) — зелёный,
    то есть правка вывода типов с `self/types.flang` не разошлась;
  flang/examples/monad/order-total.flang: 12 функций, ВСЕ доказаны тотальными,
    27 примеров сходятся, обе монады проходят все три закона;
  печать во все восемь целей; C собран `cc -std=c99 -Wall -Wextra -Werror
    -pedantic` без предупреждений;
  сверка с интерпретатором: 48 точек на напечатанном C, 42 на напечатанном JS —
    расхождений 0;
  форма и написанный руками вложенный разбор дают одно и то же на 7 входах.

Чего форма не может, и это записано уликой в claims.test.mjs: монадой не
объявить список и всё рекурсивное, включая ввод-вывод. Монада ввода-вывода —
`«Дело» от «А»` с продолжением полем `функция из «Отклик» в («Дело» от «А»)`, а
отображение внутрь функции на месте не печатается. Значит машина продолжений из
io.mjs на форму сегодня НЕ переезжает, вопреки тому, что обещал раздел «Чем это
не монада»; обещание не отменяется, а получает верный срок — частичное
применение, фаза 4 в HOF.md, а не полиморфизм, которого уже хватило.

Author: Marat Zimnurov

README.md

@@ -666,8 +666,10 @@ would be nothing to check — equality of two computations is undecidable.
 
 Where the surface stops is stated as plainly: category names (`из «Продажи» в «Биллинг»`) remain
 a note for the reader, because a category is not declared as an entity and there is nothing to
-check membership against. Natural transformations, monads, monoids and bifunctors are described
-in [`flang/cat/SPEC.md`](flang/cat/SPEC.md) and are not implemented.
+check membership against. Natural transformations are described in
+[`flang/cat/SPEC.md`](flang/cat/SPEC.md) and are not implemented; monoids, groups, isomorphisms,
+bifunctors and monads are — and a monad also comes with the binding form `в монаде`
+([`flang/cat/MONAD.md`](flang/cat/MONAD.md)).
 
 ---
 
@@ -1113,10 +1115,13 @@ attaching a solver to the verification conditions is an open task, not a feature
   diagnostic blames the pattern instead of naming the real cause. Workaround: rename it, or use
   the explicit `случай вариант «Имя»` form the stdlib uses.
 
-**The category surface.** Morphisms, composition, chains, identities and functors are
-implemented. Natural transformations, monads, monoids, groups and bifunctors are specified in
-[`flang/cat/SPEC.md`](flang/cat/SPEC.md) and are not. Category names in a functor declaration are
-a note for the reader, not a checked claim.
+**The category surface.** Morphisms, composition, chains, identities, functors, bifunctors,
+isomorphisms, monoids, groups and monads are implemented; a monad also comes with the binding form
+`в монаде`. Natural transformations are specified in [`flang/cat/SPEC.md`](flang/cat/SPEC.md) and
+are not implemented. Category names in a functor declaration are a note for the reader, not a
+checked claim. A list — and anything recursive, I/O included — cannot be declared a monad today:
+the endofunctor map is printed in place, so the parameter must occupy a whole field
+([`flang/cat/MONAD.md`](flang/cat/MONAD.md)).
 
 **Concurrency.** Six steps of seven. The missing one is the sixth — a scheduler in the C runtime:
 processes are printed only to Elixir, and the other seven targets turn a program with `процесс`

README.ru.md

@@ -677,8 +677,10 @@ FLANG_COMPOSE_MISMATCH: композиция «оформить» не стык
 
 Где поверхность кончается, сказано так же прямо: имена категорий (`из «Продажи» в «Биллинг»`)
 остаются пометкой для читателя, потому что категория отдельной сущностью не объявляется и
-проверять принадлежность не на чем. Естественные преобразования, монады, моноиды и бифункторы
-описаны в [`flang/cat/SPEC.md`](flang/cat/SPEC.md) и не реализованы.
+проверять принадлежность не на чем. Естественные преобразования описаны в
+[`flang/cat/SPEC.md`](flang/cat/SPEC.md) и не реализованы; моноиды, группы, изоморфизмы,
+бифункторы и монады — реализованы, и у монады заодно есть форма связывания `в монаде`
+([`flang/cat/MONAD.md`](flang/cat/MONAD.md)).
 
 ---
 
@@ -1121,10 +1123,13 @@ node --test flang/test/core-json.test.mjs
   диагностика винит образец вместо настоящей причины. Обходится переименованием либо явной формой
   `случай вариант «Имя»`, которой пользуется стандартная библиотека.
 
-**Категорная поверхность.** Морфизмы, композиция, цепочки, единицы и функторы реализованы.
-Естественные преобразования, монады, моноиды, группы и бифункторы описаны в
-[`flang/cat/SPEC.md`](flang/cat/SPEC.md) и не реализованы. Имена категорий в объявлении функтора —
-пометка для читателя, а не проверяемое утверждение.
+**Категорная поверхность.** Морфизмы, композиция, цепочки, единицы, функторы, бифункторы,
+изоморфизмы, моноиды, группы и монады реализованы; у монады есть форма связывания `в монаде`.
+Не реализованы естественные преобразования — они описаны в
+[`flang/cat/SPEC.md`](flang/cat/SPEC.md). Имена категорий в объявлении функтора —
+пометка для читателя, а не проверяемое утверждение. Монадой сегодня не объявить список и всё
+рекурсивное, включая ввод-вывод: отображение эндофунктора печатается на месте, поэтому параметр
+обязан стоять в поле целиком ([`flang/cat/MONAD.md`](flang/cat/MONAD.md)).
 
 **Конкурентность.** Сделаны шесть шагов из семи. Не сделан шестой — планировщик в рантайме C:
 процессы печатаются только в Elixir, а остальные семь целей дают из программы с `процесс`

docs/overview.ru.md

@@ -119,11 +119,27 @@ FLANG_COMPOSE_MISMATCH: «выставить» приводит в «Счёт»,
 тела, вычислять нечего. Это допущение автора, и компилятор отвечает лишь на то,
 осмысленно ли оно сформулировано.
 
-Естественные преобразования и монады описаны в контракте `flang/cat/SPEC.md` и
-не реализованы. Причина сместилась: раньше мешал сам параметрический
-полиморфизм, теперь он есть — и в языке, и в самоприменении, и в стандартной
-библиотеке. Мешает то, что `checkMorphisms` и `checkFunctors` знают имя типа, а
-не применение: домен морфизма ищется как `ctx.records.has(имя)`, а «из функтора
+Монада объявляется на параметрическом типе и называет две функции — `возврат`
+(η) и `соединение` (μ). Граница «доказано / проверено» проходит здесь так же,
+как у моноида: доказывается устройство — тип параметричен, `возврат` ведёт из
+«А» в M«А», `соединение` из M(M«А») в M«А», — а левая единица, правая единица и
+ассоциативность связывания проверяются на конечной сетке из примеров автора, с
+контрпримером в сообщении.
+
+Отображение эндофунктора при этом не объявляется вовсе: у полиномиального
+функтора оно ровно одно, и компилятор выводит его из устройства типа. На том же
+стоит форма `в монаде` — do-нотация словами, где каждое `пусть` есть
+связывание, а последняя строка `возврат` есть η. Форма разворачивается
+компилятором ВНУТРИ разбора, в обычные вызовы поверх обычного `разбор`, поэтому
+печать во все восемь целей и оба слоя самоприменения получают её даром, а
+функций первого класса ей не требуется: тело продолжения известно
+синтаксически. Подробности и границы — `flang/cat/MONAD.md`.
+
+Естественные преобразования описаны в контракте `flang/cat/SPEC.md` и не
+реализованы. Причина сместилась: раньше мешал сам параметрический полиморфизм,
+теперь он есть — и в языке, и в самоприменении, и в стандартной библиотеке.
+Мешает то, что `checkMorphisms` и `checkFunctors` знают имя типа, а не
+применение: домен морфизма ищется как `ctx.records.has(имя)`, а «из функтора
 «Список» в функтор «Возможно»» — утверждение про применения. Это фаза 3 в
 `flang/cat/POLY.md`.
 

flang/PLAN.md

@@ -86,10 +86,25 @@
 зависимость такой, какой она вышла:
 
 ```
-1. Параметрический полиморфизм ──→ 3. Монада ──→ 4. форма «в монаде» поверх готовой машины
+1. Параметрический полиморфизм ✅ ──→ 3. Монада и форма «в монаде» ✅
 4. Ввод-вывод (машина продолжений) ✅ ──→ 6. Отказоустойчивость
 ```
 
+Стрелка «3 → 4» не пригодилась и во второй раз: форма `в монаде` сделана, а
+машина продолжений ввода-вывода на неё НЕ переехала. Причина измерена, а не
+предположена: монада ввода-вывода — это `«Дело» от «А»`, где продолжение стоит
+полем типа `функция из «Отклик» в («Дело» от «А»)`, а форма разворачивает только
+те типы, у которых параметр стоит в поле ЦЕЛИКОМ. Проверено программой:
+
+```
+FLANG_MONAD  монада «Дело»: в варианте «Дальше» параметр «А» стоит внутри поля
+             «потом», а не целиком; отображение внутрь применения на месте
+             не разворачивается
+```
+
+Переезд ждёт частичного применения — фазы 4 в `HOF.md`, — и до тех пор
+написанное сегодня продолжает работать, как и обещал пункт 4.
+
 **1. Параметрический полиморфизм. ✅ СДЕЛАН, включая самоприменение.** Пока его
 не было, `Возможно` для чисел и для строк были двумя типами с разными именами
 конструкторов, `M(M)` — третьим, написанным руками, монада не выражалась вовсе, а
@@ -183,12 +198,41 @@ gcc и clang, Java, Elixir, Rust, Python; Go и .NET на машине нет 
 Осталось: прослеживание тегов по параметрам и частичное применение.
 Подробности и порядок — `flang/cat/HOF.md`.
 
-**3. Монада и `в монаде`. 🟢 Разблокирована пунктом (1), форма ещё не сделана.**
-Требовала (1): монада — эндофунктор плюс два преобразования, а эндофунктор без
-параметра типа не выражался. Теперь выражается — тип, «Обернуть» и «Связать»
-проходят все три проверки. Осталась синтаксическая форма `в монаде`. Форма `в монаде`
-разворачивается компилятором в вызовы `возврат` и `соединение`; функций первого
-класса ей не нужно, потому что тело известно синтаксически.
+**3. Монада и `в монаде`. ✅ СДЕЛАНЫ.** Требовала (1): монада — эндофунктор плюс
+два преобразования, а эндофунктор без параметра типа не выражался. Теперь
+выражается, и на нём сделана форма.
+
+Обещание «разворачивается компилятором в вызовы `возврат` и `соединение`;
+функций первого класса ей не нужно, потому что тело известно синтаксически»
+выполнено буквально — и оказалось не самоочевидным. Связывание требует, чтобы
+продолжение было ЗНАЧЕНИЕМ, а у продолжения есть свободные имена, которые тег
+захватить не умеет (частичного применения нет, `HOF.md`, фаза 4). Выход в том,
+что продолжение не строится вовсе: отображение эндофунктора печатается НА МЕСТЕ,
+`разбор`ом по вариантам типа, и тело стоит прямо в ветви. Свободные имена
+работают, потому что это выражение, а не функция.
+
+Отображение при этом никто не объявляет — компилятор выводит его из устройства
+типа: у полиномиального функтора законное отображение ровно одно. Поэтому
+функториальность ДОКАЗАНА построением, а строки `эндофунктор` в объявлении нет.
+
+Разворачивание сделано внутри разбора, поэтому наружу парсера форма не выходит:
+печать во все восемь целей, анализ завершаемости и обе реализации
+самоприменения получили её даром — `self/parser.flang` и `self/types.flang` не
+потребовали НИ ОДНОЙ правки, в `self/lexer.flang` дописаны только четыре
+поверхности в таблицу слов, потому что таблица сверяется тестом.
+
+Новых ключевых слов четыре: `монада`, `возврат`, `соединение`, `в монаде`; голых
+вхождений в 133 исходниках — ноль, проверено разметкой новым лексером, а не
+только `grep`-ом. Слово `вернуть` отвергнуто измерением: оно стоит голым именем
+в `examples/rosetta/towers-of-hanoi.flang`.
+
+Устройство доказывается сличением объявлений, три закона связывания
+проверяются на сетке из примеров автора с контрпримером в сообщении. По дороге
+нашёлся настоящий дефект — не в монаде, а в выводе типов: ожидание не доезжало
+внутрь аргумента вызова и внутрь поля конструктора, из-за чего блок над
+ДВУХпараметрической монадой не собирался. Починено тремя местами; сверка с
+`self/types.flang` на всём репозитории и на сломанных программах — расхождений
+ноль. Подробности, границы и три измерения про законы — `flang/cat/MONAD.md`.
 
 **4. Ввод-вывод. 🟡 Сделан — но НЕ монадой.** Язык остался чистым: описание
 действия — обычное значение (`«Поручение»`, пять вариантов, набор закрыт), а

flang/SPEC.md

@@ -176,6 +176,37 @@ flang, целиком лежащая в тотальном классе.** Об
 **стирается**: все восемь бэкендов уже печатают одно представление значения,
 и `«Возможно» от числа` со `«Возможно» от строки` дают одну фабрику варианта.
 
+### Монада и форма `в монаде`
+
+Монада объявляется НА параметрическом типе и называет две функции — η и μ.
+Отображение эндофунктора не объявляется: у полиномиального функтора оно ровно
+одно, и компилятор выводит его из устройства типа.
+
+```flang
+монада «Возможно» от «А»
+  возврат «Обернуть»
+  соединение «Сплющить»
+
+тотальная функция «Итог со скидкой»
+  принимает номер: число
+  возвращает «Возможно» от числа
+  в монаде «Возможно»
+    пусть цена равно «Цена позиции» от номер
+    пусть скидка равно «Скидка по цене» от цена
+    возврат цена минус скидка
+```
+
+Каждое `пусть` — связывание, `возврат` — последняя строка блока. Форма
+**разворачивается компилятором внутри разбора** в вызовы объявленных `возврат`
+и `соединение` поверх `разбор` по вариантам типа, поэтому в AST её нет и все
+последующие слои — типы, завершаемость, восемь бэкендов, самоприменение — о ней
+не знают. Функций первого класса форме не нужно: тело продолжения известно
+синтаксически и печатается на месте, а не заворачивается в значение.
+
+Устройство монады доказывается сличением объявлений, три закона связывания
+проверяются на конечной сетке. Подробности, счёт занятых слов и границы —
+`flang/cat/MONAD.md`.
+
 ## 4. Синтаксис
 
 Отступный, без скобок — как в FTS. Русская и английская поверхности
@@ -398,6 +429,17 @@ Pattern := { "kind": "empty" }                                  пустой с
             "initial": "Начать", "handler": "Дальше" }]
 ```
 
+### Монада
+
+Объявление добавляет ещё один необязательный список верхнего уровня; форма
+`в монаде` в AST не появляется вовсе — к концу разбора она уже развёрнута в
+`call` и `match` (`flang/cat/MONAD.md`).
+
+```jsonc
+"monads": [{ "kind": "monad", "name": "Возможно", "param": "А",
+             "unit": "Обернуть", "join": "Сплющить" }]
+```
+
 Программе, где встретилось имя из словаря ввода-вывода (или объявлен `план`),
 парсер приписывает три суммы — `«Поручение»`, `«Отклик»`, `«Продолжение»`
 (`flang/src/io.mjs`), по тому же правилу и по той же причине, что сумму