Теоркат-поверхность flang — контракт

Черновик на согласование. Что из него сделано и чем сделанное разошлось с задуманным, отмечено в разделе «Порядок работ» в конце и подробно — в главах «Моноид, группа, монада» и «Эффекты и HTTP».

Зачем

Дословно то, что заказано:

крутой язык, который позволяет писать формально-доказуемый код как в compile, так и в runtime; причём тьюринг-полный и с понятным синтаксисом словами, если освоить теоркат; мочь писать монады и моноиды, цепочку и бифунктор; и при этом чтобы я мог и http на нём писать, и для typescript на fts-like вставки утилит делать; рекурсии и прочее; иммутабельные структуры данных вести и иметь их в std, если нужно

Отсюда семь требований, и каждое ниже разобрано отдельно: полнота, поверхность теорката, монады и моноиды, эффекты (HTTP), встраиваемость, неизменяемые структуры, проверяемость в двух местах — при компиляции и при выполнении.

Что уже есть и как ложится

Разрыв, который надо закрыть, выглядит так: семантика уже категорная, а поверхность об этом молчит.

Последняя строка изменилась 2026-08-07: функции стали значениями первого класса через дефункционализацию (flang/cat/HOF.md), и объект «Б»^«А» в языке появился — его пишут функция из «А» в «Б», а вычисление eval : «Б»^«А» × «А» → «Б» пишут ф от х.

Декартово замкнутой категорией flang от этого ещё не стал, и утверждать обратное нельзя. Не хватает второй половины сопряжения — каррирования: нет ни частичного применения (функция «Сложить» от 1), ни способа превратить функцию двух аргументов в функцию одного, возвращающую функцию. Арность в flang — свойство функции, а не сахар над цепочкой одноместных, и это решение (HOF.md, «Чего решено не делать никогда»). Частичное применение стоит в плане фазой 4; до неё экспоненциал есть как объект, но не как сопряжение.

В FTS теоркат-поверхность уже есть и работает: 37 категорий, 53 объекта, 24 морфизма, 5 теорем, 4 функтора. Записана словами, без символов:

функтор «Запрос страницы в условие выборки» из «Запрос списка» в «Хранилище»
  объект «Запрос страницы» отображается в «Условие выборки»
    поле «номер страницы» отображается в поле «номер страницы»

Задача — не изобрести вторую поверхность, а распространить эту на flang.

Принятые решения

Пять вопросов, которые оставались открытыми, решены так.

1. Естественные преобразования — делаем, объявлением с проверкой. Сделано 2026-08-15. Экспоненциалы при этом не введены — преобразование объявляется, а не вычисляется как значение, и коммутативность квадрата проверяется на сетке. Прямая печать в C сохраняется: узел преобразования не доходит ни до одного бэкенда, потому что печатать в нём нечего.

Довод «без них нельзя монаду» оказался неверным, и это стоит записать: монада сделана раньше и БЕЗ них — η и μ названы обычными функциями, как операция у моноида (flang/cat/MONAD.md). Предусловием преобразования оказалось не то, что здесь предполагалось, а равенство морфизмов: квадрат коммутирует — это равенство двух композиций.

2. Категории как значения времени выполнения — нет. Категория, функтор, преобразование — объявления времени компиляции. Категория, вычисляемая в рантайме, — другой язык, и он не печатается в C без интерпретатора внутри.

**3. функция остаётся; морфизм — надстройка. Объявить функцию частным случаем морфизма красивее, но это переписывает 1711 объявлений в репозитории и ломает всё, что уже доказано побайтовой сверкой. Вместо этого: морфизм — отдельное объявление, которое может** быть реализовано функцией.

4. Законы проверяются и при компиляции, и при выполнении. Это прямое требование «как в compile, так и в runtime». Разделение такое: при компиляции закон проверяется на объявленных примерах и на выведенной сетке входов; в напечатанном коде остаётся проверка — по умолчанию включённая, отключаемая ключом печати --без-законов для горячего пути. Отключение обязано быть видимым решением, а не молчаливым умолчанием.

Первая половина сделана (flang test, flang/src/compat.mjs); вторая — объявлено, не сделано: ни проверки закона в напечатанном коде, ни ключа --без-законов нет ни в одной из восьми целей. Это шаг 5 «Порядка работ», и он не начат.

**5. Законы у нетотальных морфизмов — разрешены, с лимитом шагов. Сделано в flang test.** Запрещать неправильно: HTTP-обработчик редко тотален, а закон при нём нужен именно там. Проверка идёт под НАЗВАННЫМ пределом шагов (LAW_MAX_STEPS, flang/src/compat.mjs), и упор в предел — отдельная диагностика FLANG_LAW_LIMIT, а не молчаливый успех: passed остаётся ложью и flang test кончается кодом 1.

Отдельный код заведён не ради полноты таблицы. Исходов у проверки закона три, а не два: сошлось, не сошлось — и не досчиталось. Третий не значит «закон нарушен»: про закон в этом случае не известно ничего, и назвать его нарушенным значило бы утверждать больше, чем видели.

Здесь стояло то же самое в настоящем времени, и это было неправдой. Кода FLANG_LAW_LIMIT не существовало нигде, кроме этой строки: упор в предел уезжал в отчёт общим FLANG_RECURSION_LIMIT — тем же, каким падает зациклившийся пример обычной функции, — и по отчёту нельзя было отличить опровергнутый закон от непроверенного. Улика и обе половины проверки (краснеет на нетотальной реализации без конца; НЕ краснеет на нетотальной, которая досчиталась) — flang/test/cat-morphism.test.mjs, раздел «закон у нетотальной стрелки».

Объявлено, не сделано и здесь: тот же код в НАПЕЧАТАННОМ коде — вместе с шагом 5 «Порядка работ»; предел один на все законы и доводом не меняется.

Видом отказа процесса FLANG_LAW_LIMIT при этом НЕ становится, и это не упущение. Замкнутое множество видов (flang/conc/SPEC.md, src/failures.mjs, сегодня их семь) — про то, чем падает процесс НА ПРОГОНЕ; этот же код рождается в инструменте, когда тот считает примеры автора, и никакого процесса рядом нет. Вопрос откроется заново вместе с шагом 5: закон, проверяемый внутри обработчика в напечатанном коде, будет отказывать уже процессом — и тогда виду быть.

Поверхность

Только слова. Никаких →, ≅, ∘, ∀, >>= — всё, что нельзя набрать на обычной клавиатуре, запрещено. Правило уже действует в FTS и остаётся.

Категория и морфизм

Сделано. Форма вышла короче задуманной на одну строку и на одно понятие.

объект «Заказ»
  сумма является числом

объект «Отгрузка»
  номер является числом

тотальная функция «Отгрузить заказ»
  принимает заказ: «Заказ»
  возвращает «Отгрузка»
  запись «Отгрузка» с номер равным заказ.сумма

морфизм «отгрузить» из «Заказ» в «Отгрузка»
  даёт «Отгрузить заказ»
  закон «номер берётся из суммы»
    пример «обычный»
      дано заказ равно запись «Заказ» с сумма равным 5
      ожидается запись «Отгрузка» с номер равным 5

даёт — вычисление, закон — проверяемое обещание. Блок необязателен: морфизм без даёт остаётся чистым утверждением, как в FTS сегодня, и обратная совместимость сохраняется. Поля gives и laws появляются в узле AST только когда написаны — иначе AST каждой существующей стрелки поменялся бы на два поля, а его сверяет побайтово неподвижная точка самоприменения.

**даёт называет функцию, а не несёт выражение**, и это расхождение с черновиком выше (даёт запись «Отгрузка» с номер равным …). Тело прямо в стрелке — это второй разбор выражений, второй вывод типов, второй анализ завершаемости и восьмая печать в восьми целях; названная функция не стоит ничего из этого и говорит ровно то же. Так уже сделано у моноида (операция «Соединить») и у монады (возврат «Обернуть»), и решение 3 выше — «морфизм может быть реализован функцией» — это же и говорит.

**требует не заведено.** Предусловие — отдельное понятие, у него своя цена (проверка при выполнении во всех восьми целях) и свой смысл; на закон оно не влияет, а поверхность занимает. Оно остаётся в этом контракте как задуманное, не как сделанное.

Граница здесь проходит внутри одной конструкции. Доказывается сличением объявлений: функция объявлена; она принимает ровно один вход (стрелка ведёт из одного объекта в один, а произведение объектов пишется записью-доменом); тип входа — домен, тип результата — кодомен. Несовпадение даёт свой код FLANG_MORPHISM_SHAPE, а не общий FLANG_TYPE.

Проверяется на примерах сам закон, и проверяет его flang test, а не flang check: закон говорит о равенстве вычислений, а примеры функции проверяет ровно эта команда. Класть закон в check значило бы, что часть примеров языка проверяет одна команда, а часть — другая, и автор обязан помнить, какая именно. Нарушенный закон называет себя целиком — морфизм «отгрузить», закон «номер берётся из суммы», — потому что по одной строке отчёта обязано быть видно, чьё обещание не выполнилось.

Закон без даёт и закон без единого примера отвергаются разбором. Первый проверять не на чем; второй обещает и не проверяет ничего, а такое объявление хуже отсутствующего — оно читается как гарантия.

Категория называет свои стрелки

Сделано 2026-08-14. До этого дня категория в языке НЕ ОБЪЯВЛЯЛАСЬ вовсе: категория «Х» была заголовком документа FTS, именем и ничем больше. Имена на концах функтора (из «Продажи» в «Биллинг») оставались пометкой для читателя, и утверждать, что стрелка принадлежит именно этой категории, было не на чем.

Дороже стоила вторая половина той же дыры. Раздел «Граница честности» ниже обещал «полноту отображений функтора — каждому объекту и морфизму ДОМЕНА сопоставлено что-то в кодомене», а проверить это было нечем: функтор, отобразивший две стрелки из пяти, проходил flang check молча, потому что «пять» было неизвестным числом.

категория «Продажи»
  морфизм «отгрузить»
  морфизм «выставить»
  морфизм «оформить»

Ни одного нового слова. Таблицу лексера сверяет побайтово self/lexer.flang, и новое слово стоило бы правки в обоих; морфизм «имя» без из и без блока разбор прежде ОТВЕРГАЛ («требует строки 'если' и 'то'»), значит эта запись занимает то, что было ошибкой, и не отнимает ничего у написанного. Членство отличается от объявления тем, что за именем НЕТ ничего, включая отступной блок, — заголовок документа FTS читается ровно как читался, и ключа categories у него не появляется.

Единицы в списке не пишутся: единица «Заказ» входит в категорию тогда и только тогда, когда «Заказ» — объект одной из её стрелок. Иначе автор писал бы её дважды — объявлением и членством, — и второе место могло бы разойтись с первым молча.

Доказываются сличением объявлений, без единого вычисления, две аксиомы категории: замкнутость под композицией (FLANG_CATEGORY_NOT_CLOSED — композиция в категории обязана быть собрана из стрелок этой же категории) и наличие единицы у каждого объекта (FLANG_CATEGORY_NO_IDENTITY). Сюда же членство: FLANG_CATEGORY_UNKNOWN_ARROW и FLANG_CATEGORY_ARROW_TWICE. Повтор не безобиден — полнота функтора считается по числу членов, и дважды посчитанная стрелка сделала бы «пять из пяти» неправдой.

Здесь стояло «не проверяется ассоциативность композиции», и довод был верный: «в» после («б» после «а») и («в» после «б») после «а» — в языке ДВА РАЗНЫХ ИМЕНИ, а равенства морфизмов в языке не было вовсе, и проверка, сравнивающая имена, продавала бы сличение строк за аксиому. Равенство появилось 2026-08-15 — следующим разделом, — и ассоциативность вместе с ним стала выразимой и проверяемой на сетке (FLANG_CATEGORY_NOT_ASSOC). Про силу этой проверки там же сказано прямо: она подтверждает, а не устанавливает.

Категория, о которой не сказано ничего, остаётся допущением автора. Полнота функтора проверяется там и только там, где написано, из чего категория состоит: FLANG_FUNCTOR_NOT_TOTAL — стрелка домена без образа, FLANG_FUNCTOR_IMAGE_OUTSIDE — образ, уехавший мимо категории кодомена. Это та же граница, по которой изоморфизм без даёт уходит в assumed, а не в диагностику: объявлять то, чего ещё нет, законно и полезно.

Равенство морфизмов: категория объявляет своё равенство

Сделано 2026-08-15. Без него не проверялась ассоциативность композиции и не были выразимы естественные преобразования: коммутирующий квадрат — это равенство двух композиций.

категория «Отгрузки»
  морфизм «отгрузить»
  морфизм «выписать»
  объект «Заказ» даёт «Заказы равны»
  объект «Отгрузка» даёт «Отгрузки равны»

Категория обогащена сетоидами: она объявляет СВОЁ отношение равенства на значениях каждого своего объекта — функцией из двух значений в признак, — а равенство СТРЕЛОК выводится из него поточечно: ф и ф' из «А» в «Б» равны, когда на каждом значении «А» их образы равны по равенству «Б». Это стандартный ответ теории категорий, записанной в языке с типами: так устроены agda-categories и категорные библиотеки Coq вне UniMath.

Два других пути отвергнуты, и оба по существу. Равенство через типы тождества требует зависимых типов, которых у flang нет и не будет (см. «Чего нет и не будет без отдельной большой работы»). Равенство по нормализации работает только для очень конкретных категорий и про остальные молчаливо лжёт.

Ни одного нового слова. объект и даёт ключевые с первого дня, значит таблица лексера, четыре её поверхности и парсер на flang новых продукций не получили — форма разобралась готовыми. объект «Х» с ключевым словом в той же строке разбор ПРЕЖДЕ отвергал (за именем записи идёт блок полей), значит запись занимает то, что было ошибкой, и не отнимает ничего у написанного. Довод тот же, каким членство категории заняло морфизм «имя» без из. даёт здесь означает ровно то же, что у стрелки и у моноида: вот функция, которая это считает.

Доказывается сличением объявлений, без единого вычисления: объект стоит на конце хотя бы одной стрелки ЭТОЙ категории (FLANG_CATEGORY_EQUALITY_OUTSIDE); равенство у объекта одно (FLANG_CATEGORY_EQUALITY_TWICE); названная функция объявлена, принимает ровно два входа этого объекта и возвращает признак (FLANG_CATEGORY_EQUALITY_SHAPE). Отношение — это функция в «да/нет»; функция, возвращающая число, отношением не является ни при каком прочтении.

Проверяется на сетке — три закона, и все три говорят о равенстве вычислений на всех значениях объекта, то есть неразрешимы:

1. объявленное равенство есть ЭКВИВАЛЕНТНОСТЬ — рефлексивно, симметрично, транзитивно (FLANG_EQUALITY_NOT_REFLEXIVE, FLANG_EQUALITY_NOT_SYMMETRIC, FLANG_EQUALITY_NOT_TRANSITIVE). Не проверив этого, «доказать» можно что угодно: «не больше» рефлексивно и транзитивно, а равными на нём вышли бы стрелки, из которых одна меньше другой;
2. композиция его УВАЖАЕТ — «если ф равно ф', то г после ф равно г после ф'». При поточечном равенстве стрелок это ровно требование к каждой стрелке категории: равные значения обязаны переходить в равные (FLANG_EQUALITY_NOT_CONGRUENT). Проверяется и корень — каждая стрелка, — и само утверждение о композиции на тех парах стрелок, которые на сетке вышли равными;
3. композиция АССОЦИАТИВНА (FLANG_CATEGORY_NOT_ASSOC): обе скобки собираются порознь, как два разных морфизма, и сравниваются ОБЪЯВЛЕННЫМ равенством кодомена.

Сломанное равенство останавливает остальные два закона, а не считается заодно: их вердикт был бы утверждением о том, что равенством не является. Отчёт говорит об этом словами (aborted), а не выдаёт непосчитанное за чистую сетку.

Сила третьей проверки названа честно, и это важнее самой проверки. Композиция в flang не пишется автором: после разворачивается в применение, а применение ассоциативно по построению вычислителя. Значит у категории, где все три стрелки реализованы, обе скобки дают ОДНО значение, и вся проверка сводится к вопросу «рефлексивно ли объявленное равенство в той точке, куда композиция пришла». Вопрос не пустой — точка эта в сетку кодомена, вообще говоря, не входит, и рефлексивность там никем не считана (на этом и построен тест «ассоциативность умеет краснеть»), — но выдавать его за проверку аксиомы нельзя. Что изменилось по существу: раньше две скобки были ДВУМЯ ИМЕНАМИ и сравнить их было нечем; теперь сравниваются ВЫЧИСЛЕНИЯ через объявленное автором равенство.

**Чтобы ассоциативность могла краснеть и на честной программе, композиции нужен собственный даёт** — тогда две скобки пойдут через две написанные руками функции и разойдутся, если хоть одна из них неверна. Слова для этого есть все, работа отдельная, и здесь она записана как задуманная, а не как сделанная.

Категория без объявленного равенства остаётся допущением автора: сравнивать нечем, диагностики нет, а в ведомости стоит строка «на веру» с причиной. Это та же граница, по которой туда уходит изоморфизм без даёт, и тот же довод: объявление, о котором отчёт молчит, читается как проверенное.

Реализация — flang/src/setoid.mjs (сетка), checkCategories в flang/src/types.mjs (устройство); проверки — flang/test/cat-equality.test.mjs, настоящая программа — flang/examples/cat/order-shipment.flang.

Композиция, единица, цепочка

морфизм «выставить счёт по отгрузке» это «выставить счёт» после «отгрузить»
единица «Заказ»

цепочка «оформить заказ»
  сначала «проверить остаток»
  затем «отгрузить»
  затем «выставить счёт»

после — композиция в математическом порядке (правая применяется первой). цепочка — та же композиция в порядке чтения, для длинных конвейеров: без неё «в» после («б» после «а») читается наизнанку. Компилятор проверяет стыковку доменов и кодоменов в обоих случаях.

Функтор и бифунктор

Сделано. Поверхность вышла короче задуманной: строк сохраняет композицию и сохраняет единицы нет. Отображение, не сохраняющее композицию, функтором не является, и разрешение на проверку закона продавало бы имя вместо содержания. Образ морфизма пишется через отображается в морфизм, чтобы отличаться от образа объекта.

функтор «Заказ в счёт» из «Продажи» в «Биллинг»
  объект «Заказ» отображается в «Счёт»
  морфизм «отгрузить» отображается в морфизм «выставить»

бифунктор «Пара» из «Продажи» и «Продажи» в «Пары»
  объекты «Заказ» и «Заказ» отображаются в «Пара заказов»
  объекты «Отгрузка» и «Отгрузка» отображаются в «Пара отгрузок»
  морфизмы «отгрузить» и «отгрузить» отображаются в морфизм «отгрузить обе»

Бифунктор лёг на устройство функтора целиком: вся проверка построена на сличении объявленных имён, а ключ отображения — деталь, там имя объекта, здесь пара имён. Все законы переписались заменой ключа и ничем больше.

Не лёг общий вид из этого контракта — из «Значения» и «Значения» в «Значения» с образом «Пара А Б». Здесь «А» и «Б» переменные типа. Раньше причина была в языке — параметрических типов не было вовсе; теперь они есть (объект «Пара» от «Первый» и «Второй» разбирается и проверяется, а flang/stdlib/optional.flang на них написан), и причина сместилась в проверку: checkFunctors ищет объект по ИМЕНИ (ctx.records.has(имя)) и применения не знает. Поэтому пары объектов и морфизмов конкретные — ровно так же, как конкретны объекты у функтора, где «Заказ отображается в Счёт» пишется для двух записей, а не для семейства. Ограничение общее для обеих конструкций, снимется фазой 3 в flang/cat/POLY.md и законов не касается.

Множественное число (объекты, морфизмы, отображаются в) заведено отдельными поверхностями — как равен, равна и равное дают один cmpEq. Множественное «объекты» не приписано к объект намеренно: иначе объекты «Х» наверху файла разбиралось бы как объявление записи.

Изоморфизм

Сделано. Пара стрелок туда и обратно; концы называются теми же из … в …, какими их называют морфизм и функтор.

изоморфизм «Заказ и накладная» из «Заказ» в «Накладная»
  прямой морфизм «выписать»
  обратный морфизм «по накладной»

прямой морфизм и обратный морфизм — фразы из двух слов, а не «туда» и «обратно». Оба наречия сегодня свободны, но свободны случайно: это обычные слова, и завтра кто-нибудь напишет пусть обратно равно …. Фраза из двух слов именем быть не может никогда — тот же довод, по которому в языке стоят обратный элемент и разложить … на символы.

Граница здесь проходит внутри одной конструкции, и она не та, что была намечена ниже в разделе о честности. Доказывается сличением объявлений: объекты объявлены; обе стрелки объявлены; концы сходятся крест-накрест — прямая из «А» в «Б», обратная из «Б» в «А», отчего обе композиции и замыкаются на себя; единицы обоих объектов объявлены, потому что закон говорит именно о них.

Проверяется на сетке — само равенство «обратный после прямого = единица», и ровно там, где обе стрелки реализованы (даёт «Ф»). Здесь стояло «не проверяется вовсе», и причина была честная: у стрелки не было тела, вычислять на сетке было нечего. Там же было названо условие, при котором это меняется, — «сетка появится здесь тогда же, когда у морфизма появится даёт». даёт появился, и сетка появилась (flang/src/iso.mjs, код FLANG_ISO_NOT_INVERSE). Значения берутся оттуда же, откуда у моноида, — из написанных автором: входы примеров прямой стрелки суть значения первого объекта, ожидаемые значения примеров обратной — тоже; для второго объекта наоборот. Сообщение предъявляет контрпример: без значения «не обратимо» заставляет искать его руками, а именно значение и есть вся находка.

Остаётся допущением автора — пара, где хотя бы одна стрелка без даёт. Проверять нечем, и проверка молчит: объявление стрелки без реализации законно и полезно (так написаны все 24 морфизма наследия FTS), а требовать реализацию ради проверки значило бы запретить объявлять то, чего ещё нет. Изоморфизм с пустой сеткой в список проверенных не попадает вовсе — сказать «проверено» о нуле значений значило бы подменить «доказано» на «посмотрели».

Из допущения компилятор не выводит следствий, и это тоже решение, а не недоделка. Зная «обратный после прямого = единица А», можно было бы считать единицей объявленную композицию с такими сомножителями — и тогда у функтора столкнулись бы два его собственных закона: сохранение композиции требует, чтобы образом была «композиция образов», сохранение единиц — чтобы образом была «единица …», а выполнить оба сразу нельзя ни при каком объявлении.

Здесь стояло «языку с равенствами морфизмов нужна отдельная работа». Работа сделана — «Равенство морфизмов» выше, — но вывод следствий из допущения она НЕ открывает и открыть не может: равенство там поточечное, то есть проверяемое на сетке, а следствие компилятор выводил бы обо всех входах. Столкновение двух законов функтора от появления равенства никуда не делось.

Связь модулей: интерфейс объектом, связь морфизмом

Сделано 2026-08-16. Ни одного нового слова.

Разговор начался с мысли, которая верна: программа на flang — это и есть спецификация, а значит категорную запись можно использовать, чтобы сверять деловые требования с уже построенной цепочкой модулей. Модуль заказов, модуль платежей, модуль отгрузки — у каждого своё представление о заказе; перевод между ними обязан сохранять устройство; если новое требование его ломает, модули рассогласованы, и ни одна система типов этого не поймает.

Интерфейс модуля — это его категория. Читать её проще всего как рисунок из коробочек и стрелок: коробочка — вид вещи (объект «Заказ»), стрелка обязана быть функцией, то есть на каждую вещь давать ровно один ответ (морфизм «отменить заказ»), а строка категория «Заказы» со списком стрелок и есть объявление «вот что я умею». Ничего нового здесь нет — так категория пишется с 14 августа.

Связь между модулями — это функтор между такими категориями. В категории категорий функтор и есть морфизм, поэтому «связь морфизмом» — не метафора, а то, чем эта запись является. Нового и здесь нет: функтор «Ф» из «А» в «Б» пришёл ещё из FTS.

Новое одно — перевод данных:

функтор «Заказ в платёж» из «Заказы» в «Платежи»
  объект «Заказ» отображается в «Платёж» даёт «Платёж по заказу»
  морфизм «отменить заказ» отображается в морфизм «вернуть платёж»

даёт «Ф» называет функцию, которая переводит значения одного объекта в значения другого. Без неё связь была сличением имён: сказать «заказу соответствует платёж» можно было, а сказать, ЧЕМ именно, — нечем, и проверять было нечего.

Ни одного нового слова, и это не экономия. Слово в таблице лексера — это ещё и четыре поверхности (ru/en/eo/zh), и правка self/lexer.flang, которую сверяет побайтово тест самораскрутки. даёт уже ключевое и значит здесь ровно то же, что у стрелки, у моноида и у вложения. Сама запись занимает то, что было ошибкой: объект «А» отображается в «Б» даёт «Ф» разбор прежде отвергал («не разобрана конструкция: непонятная строка функтора»), потому что за именем образа шёл либо конец строки, либо отступной блок полей. Тот же приём, каким категория получила список своих стрелок. Занятость слов, которые понадобились бы иначе, измерена по 188 файлам: связь — 19 голых вхождений (сломалось бы 19 мест), через — 7; интерфейс, перевод, согласование, сохраняет свободны, но даром ни одно из них не досталось бы.

Ключ gives встаёт в AST после fields и появляется только там, где написан: AST сорока моделей .fts репозитория не меняется ни на байт.

Замкнутый контур — это проверяемое утверждение

     ┌─────────┐  отменить заказ   ┌─────────┐
     │  Заказ  │ ────────────────▶ │  Заказ  │
     └────┬────┘                   └────┬────┘
          │ Платёж по заказу            │ Платёж по заказу
          ▼                             ▼
     ┌─────────┐  вернуть платёж   ┌─────────┐
     │ Платёж  │ ────────────────▶ │ Платёж  │
     └─────────┘                   └─────────┘

Два пути из левого верхнего угла в правый нижний обязаны давать одно и то же:

перевести и сделать = сделать и перевести

По-деловому это значит «отменённый заказ отменён везде». Формально t есть естественное преобразование из вложения категории домена в композицию «функтор, потом вложение категории кодомена»; обе категории вложены в одну большую категорию типов и тотальных функций flang, поэтому вертикальные стрелки квадрата законны, хотя ни одной из двух категорий не принадлежат.

Доказывается сличением объявлений, без единого вычисления: перевод объявлен, принимает ровно один вход, вход этот — объект-источник, результат — его образ. Не сошлось — свой код FLANG_FUNCTOR_TRANSLATION, а не общий FLANG_TYPE.

Проверяется на сетке сам квадрат — flang/src/functor.mjs, код FLANG_FUNCTOR_SQUARE. Значения берутся оттуда же, откуда у изоморфизма: из примеров, написанных автором. Сообщение предъявляет контрпример — значение и оба исхода, — потому что именно значение и есть вся находка:

FLANG_FUNCTOR_SQUARE  функтор «Заказ в платёж»: квадрат не сходится на стрелке
                      «отменить заказ»: на {"сумма":500,"отменён":0} путь «Платёж
                      по заказу» после «отменить заказ» дал {"копейки":50000,
                      "возвращён":0}, а «вернуть платёж» после «Платёж по заказу»
                      — {"копейки":50000,"возвращён":1}

Замыкание по композиции достаётся даром, и это не случайность: вычисление и есть композиция. Если квадраты образующих стрелок сошлись на сетке, квадрат любой их композиции на той же сетке сходится сам. Проверка тем не менее умеет взять и композицию — иначе категория, собранная из стрелок, была бы наполовину непроверяемой.

Связь без переводов остаётся допущением автора. Диагностики ей не нужно — объявление без реализации законно и полезно, так написаны все четыре функтора наследия FTS, — но и в checked ей не место: сказать «проверено» о нуле сравнений значило бы подменить «доказано» на «посмотрели». Такие связи уезжают в assumed и стоят в ведомости строкой «на веру».

Связывание переносит категории — иначе всё это мертво

Отдельная правка, без которой у главы не было бы смысла. linkProgram не переносил categories в слитую программу, и полнота связи между модулями не проверялась вовсе. Улика снималась тремя файлами: модуль с категорией из одной стрелки, второй со своей, третий с функтором, который эту стрелку не отображает. Одним файлом — FLANG_FUNCTOR_NOT_TOTAL; теми же строками, разложенными по трём модулям, — valid: true и ноль диагностик. Заодно молчали и две аксиомы самой категории: замкнутость и наличие единиц переставали проверяться, стоило файлу обзавестись хоть одной строкой использует.

Что этот слой НЕ проверяет — и не будет

Раздел обязательный, потому что соблазн продать больше велик.

• Он не говорит, что требование хорошее. Он говорит, что новое требование противоречит существующему переводу. Деловая правильность самих требований вне его досягаемости целиком и навсегда.
• Сетка конечна. Квадрат, сошедшийся на значениях автора, не доказан ни для каких других. Ведомость печатает про него строку, оканчивающуюся словами «Это не доказательство», и это не скромность: на сетке ловится опровержение, а подтверждения там нет.
• Вырожденная сетка проверяет саму себя. Если оба пути на всех значениях сетки дают одно и то же значение, квадрат сходится при любой реализации. Запретить это нечем, поэтому оно называется числом: checked несёт distinct — сколько РАЗЛИЧНЫХ исходов дала сетка, — и ведомость его печатает.
• Полей перевода компилятор не видит. Строки поле … отображается в поле … внутри объекта функтора — пометка наследия FTS; согласованность перевода с ними не проверяется ничем. Проверяется только то, что перевод вычисляет.
• Двух переводов одного объекта не бывает. Отображение объектов однозначно (FLANG_FUNCTOR_OBJECT_TWICE), значит и перевод у объекта один. Связь, где один заказ переводится в платёж двумя способами и способы обязаны совпасть, в этой записи не выражается.
• Обратной связи не выводится. Из того, что квадрат сошёлся, компилятор не заключает ничего о существовании перевода назад: это утверждение об обратимости, и для него есть своё слово — изоморфизм.
• Ничего не проверяется у связи, ведущей в модуль, которого нет в сборке. Слой видит ровно те объявления, которые приехали через использует; связь с модулем, лежащим за границей программы, объявить нельзя.

Вложение и общая часть

Сделано. Два слова, и каждое отвечает на вопрос, на который стрелка сама по себе не отвечает. Подробный контракт — flang/cat/SETS.md; здесь только место в этой картине.

вложение «Срочные среди заказов» из «Срочный» в «Заказ» даёт «Срочный заказ»
пересечение «Срочные оплаченные» из «Срочный» и «Оплаченный» в «Заказ»

вложение — подобъект: мономорфизм, обещающий, что «Срочный» есть ЧАСТЬ «Заказа», а не его фактор. Обычный морфизм этого не обещает: у него сказано только, что стрелка есть. Разница проверяема — склеивающая стрелка ловится контрпримером (FLANG_EMBED_NOT_INJECTIVE), и в этом весь смысл отдельного слова: печатать вложение обычной стрелкой значило бы записать «стрелку» там, где автор сказал «подмножество».

пересечение — предел: расслоенное произведение над объемлющим объектом. Объемлющее обязательно, и это не украшение записи: без него квадрата, который общая часть замыкает, попросту нет, а в языке — нечем сличать общий элемент, потому что значения разных типов несравнимы.

Объединения среди слов нет намеренно: ко-произведение в языке уже есть и называется тип … вариант … вместе с исчерпывающим разбором. Довод и два других, почему третьего слова не завелось, — в flang/cat/SETS.md.

Форма в AST

Обе конструкции добавляют по необязательному списку верхнего уровня — появляются они только там, где объявления есть, как morphisms и monoids:

"isomorphisms": [{ "kind": "isomorphism", "name": "Заказ и накладная",
                   "from": "Заказ", "to": "Накладная",
                   "forward": "выписать", "backward": "по накладной" }],
"bifunctors":   [{ "kind": "bifunctor", "name": "Пара",
                   "from": ["Продажи", "Продажи"], "to": "Пары",
                   "objects":   [{ "from": ["Заказ", "Заказ"], "to": "Пара заказов" }],
                   "morphisms": [{ "from": ["отгрузить", "отгрузить"],
                                   "to": "отгрузить обе" }] }]

Функтор, в отличие от них, до сих пор живёт в legacy узлом functorFile — он пришёл из FTS и разбирается тем же кодом. Переносить его сюда сейчас значило бы менять форму, которую читает compat.mjs, ради одной только стройности.

Стрелка с реализацией добавляет к своему узлу два необязательных ключа — и только когда они написаны:

"morphisms": [{ "kind": "morphism", "name": "отгрузить",
                "domain": "Заказ", "codomain": "Отгрузка",
                "gives": "Отгрузить заказ",
                "laws": [{ "name": "номер берётся из суммы",
                           "examples": [{ "name": "обычный",
                                          "args": { "заказ": { "сумма": 5 } },
                                          "expected": { "номер": 5 } }] }] }]

Пример закона — той же формы, что пример функции, и разбирается тем же кодом: второй разбор примеров означал бы второе понимание слов «дано» и «ожидается».

Категория со списком стрелок добавляет свой список — и тоже только там, где членство написано; ключ стоит последним, поэтому AST моделей .fts, где категория «Х» служит заголовком документа, не меняется ни на байт:

"categories": [{ "kind": "category", "name": "Продажи",
                 "morphisms": ["отгрузить", "выставить", "оформить"] }]

Своё равенство добавляет к этому узлу ещё один необязательный ключ — и тоже только когда написано; стоит он между morphisms и span, потому что порядок ключей есть часть побайтовой сверки:

"categories": [{ "kind": "category", "name": "Отгрузки",
                 "morphisms": ["отгрузить", "выписать"],
                 "equalities": [{ "object": "Заказ", "gives": "Заказы равны" }] }]

Естественное преобразование добавляет свой список верхнего уровня — последним, после categories, и по тому же правилу «только когда написано»:

"transformations": [{ "kind": "transformation", "name": "в копейки",
                      "from": "В рублях", "to": "В копейках",
                      "components": [{ "object": "Заявка",
                                       "morphism": "заявку в копейки" }] }]

Свои коды диагностик: FLANG_CATEGORY_UNKNOWN_ARROW, FLANG_CATEGORY_ARROW_TWICE, FLANG_CATEGORY_NOT_CLOSED, FLANG_CATEGORY_NO_IDENTITY, FLANG_CATEGORY_EQUALITY_SHAPE, FLANG_CATEGORY_EQUALITY_TWICE, FLANG_CATEGORY_EQUALITY_OUTSIDE, FLANG_CATEGORY_NOT_ASSOC, FLANG_EQUALITY_NOT_REFLEXIVE, FLANG_EQUALITY_NOT_SYMMETRIC, FLANG_EQUALITY_NOT_TRANSITIVE, FLANG_EQUALITY_NOT_CONGRUENT, FLANG_TRANSFORM_SHAPE, FLANG_TRANSFORM_COMPONENT, FLANG_TRANSFORM_NOT_TOTAL, FLANG_TRANSFORM_NOT_NATURAL, FLANG_FUNCTOR_NOT_TOTAL, FLANG_FUNCTOR_IMAGE_OUTSIDE, FLANG_MORPHISM_SHAPE, FLANG_ISO_MISMATCH, FLANG_ISO_IDENTITY_MISSING, FLANG_ISO_NOT_INVERSE, FLANG_BIFUNCTOR_OBJECT_TWICE, FLANG_BIFUNCTOR_OBJECT_MISSING, FLANG_BIFUNCTOR_ARROW_MISMATCH, FLANG_BIFUNCTOR_COMPOSITION, FLANG_BIFUNCTOR_IDENTITY, FLANG_FUNCTOR_TRANSLATION, FLANG_FUNCTOR_SQUARE. Общего FLANG_TYPE здесь нет намеренно: по коду машина понимает, что чинить, и это записано ниже отдельным требованием.

Естественное преобразование

Сделано 2026-08-15. Поверхность вышла не той, что была задумана здесь, и правка вынужденная — зато вынужденная в дешёвую сторону.

морфизм «в копейки» из функтора «В рублях» в функтор «В копейках»
  объект «Заявка» отображается в морфизм «заявку в копейки»
  объект «Счёт» отображается в морфизм «счёт в копейки»

Задуманного здесь преобразование … на объекте … действует морфизмом … квадрат коммутирует нет, и слов этих в языке не заведено. Занятость всех четырёх измерена flang/scripts/word-occupancy.mjs на 179 файлах корпуса — голым именем у каждого ноль, — то есть дело не в том, что слова заняты. Дело в цене: свободное слово стоит правки в ДВУХ таблицах лексера (src/lexer.mjs и self/lexer.flang, они сверяются побайтово), в ЧЕТЫРЁХ поверхностях и продукции в ДВУХ парсерах. За то же самое.

Естественное преобразование ЕСТЬ морфизм в категории функторов, и других прочтений у записи нет: из функтора «Ф» в функтор «Г» называет концы тем же из … в …, каким их называют стрелка, функтор и изоморфизм. Слово морфизм открывает теперь четыре конструкции, и решает не оно, а следующий токен: из «А» в «Б» — стрелка, из функтора «Ф» в функтор «Г» — преобразование, это «б» после «а» — композиция, всё остальное — утверждение наследия FTS. Ключевым словом имя быть не может никогда, значит взгляда на один токен хватает.

Из таблицы лексера прибавилась ровно ОДНА форма — родительный падеж функтора рядом с функтор, как поля рядом с поле и числа рядом с число. Это не новое слово, а второй падеж того же, и нужен он одной этой фразе: без него она была бы не по-русски. Трём другим поверхностям падеж не нужен — from functor … to functor …, de funktoro … al funktoro … и 从函子…到函子… стоят в исходной форме. отображается в морфизм взято у функтора вместе с его смыслом: там объект переходит в объект (отображается в), здесь объекту сопоставлена СТРЕЛКА.

Доказывается сличением объявлений: оба функтора объявлены; они параллельны — ведут из одной категории в одну (FLANG_TRANSFORM_SHAPE); у объекта не больше одной компоненты и концы компоненты — ровно Ф(Х) и Г(Х) (FLANG_TRANSFORM_COMPONENT); компонента есть у каждого отображённого объекта (FLANG_TRANSFORM_NOT_TOTAL). Преобразование без единой компоненты отвергается разбором — тем же доводом, каким отвергается закон без примеров.

Проверяется на сетке закон естественности (FLANG_TRANSFORM_NOT_NATURAL): для каждой стрелки ф: Х → У категории домена пути Г(ф) после альфа_Х и альфа_У после Ф(ф) дают значения, равные по объявленному равенству категории кодомена. Категория кодомена без своего равенства и нереализованная стрелка квадрата уводят преобразование в «на веру», а не в отказ.

И вот чем этот закон отличается от ассоциативности — это главное. Ассоциативность на реализованных стрелках сходится всегда: обе скобки — одна и та же цепочка применений. Квадрат же собран из ЧЕТЫРЁХ написанных автором функций, и равенство путей есть настоящее утверждение о его коде. В flang/examples/cat/natural-square.flang это видно на настоящей задаче: два функтора — «то же самое в рублях» и «то же самое в копейках», преобразование — перевод единиц, и закон говорит, что перевести и посчитать наценку есть то же, что посчитать наценку и перевести. Поставьте в наценку копейками 100 вместо 1000 — забудьте про единицы ровно один раз — и файл не соберётся, назвав значение, на котором пути разошлись. Ни один другой закон дерева этой правки не видит: функция остаётся тотальной, типы сходятся, свой пример подгоняется.

Чего здесь по-прежнему НЕТ: задуманного из функтора «Список» в функтор «Возможно» — преобразования между функторами над ПРИМЕНЕНИЯМИ параметрических типов. checkFunctors знает имя типа, но не применение; это фаза 3 в flang/cat/POLY.md, и она не сделана. Сделанное работает над функторами, объявленными по именам, — то есть над теми, какие в языке есть.

Моноид, группа, монада

Сделано. Поверхность вышла не той, что была задумана здесь, и обе правки вынужденные.

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

Это оказалось не потерей, а находкой: группа и есть моноид с обращением. Второе слово развело бы две проверки, обязанные совпадать во всём, кроме одного закона.

моноид «Склейка строк»
  носитель строка
  операция «Склеить»
  единица ""

моноид «Сложение чисел»
  носитель число
  операция «Сложить»
  единица 0
  обратный элемент «Противоположное»

Что здесь доказано, а что проверено, — граница проходит внутри одной конструкции, и это стоит запомнить.

Доказывается устройство: операция обязана быть функцией двух аргументов носителя, возвращающей носитель; единица — значением носителя; обращение — функцией носителя в носитель. Утверждения обо всех входах, берутся из объявлений, живут в checkTypes рядом с законами функтора.

Проверяются на конечной сетке сами законы — ассоциативность, нейтральность, обратимость. Это равенства вычислений на всех значениях носителя, и решить их нельзя: можно только предъявить контрпример. Сетка берётся из примеров самой операции плюс единица — оттуда, где автор уже написал краевые случаи, — и её размер печатается в отчёте. Сообщение называет значения, а не выносит вердикт:

FLANG_MONOID_ASSOC  моноид «Вычитание»: операция не ассоциативна:
                    на 0, 0, 5 слева вышло -5, справа 5

Монада — сделана. Поверхность вышла короче задуманной на две строки, и обе правки вынужденные; подробности, счёт занятых слов и границы — в flang/cat/MONAD.md.

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

Строки эндофунктор «Возможно» нет: она повторяла бы имя, стоящее строкой выше, и не проверяла ничего — монада объявляется НА типе, как моноид на носителе. Слова преобразованием нет тоже: естественных преобразований в языке ещё нет, а возврат «Обернуть» называет обычную функцию — ровно как операция «Склеить» у моноида. Зато появилось от «А», и оно обязательно: «Результат» от «Значение» и «Беда» — монада по первому параметру, а соглашение «по последнему» было бы неверным ровно в половине случаев.

Законы объявлены самим видом конструкции — писать их отдельно не нужно, компилятор знает, что проверять: ассоциативность и нейтральность у моноида, обратимость у группы, левую и правую единицу и ассоциативность связывания у монады.

Свойства, объявляемые отдельно от конструкции

Сделано 2026-08-16. У моноида коммутативности не было, и в таблице персистентных структур выше это стояло записанным честно: множество названо «моноидом, коммутативным», а сказать этого языком было нечем. Строкой в моноид такое не ложится — моноид объявляет ТРИ вещи разом и получает три закона, а коммутативность есть свойство ОДНОЙ операции, и объявлять её надо там же, где объявляют саму операцию.

Отсюда пятое объявление — свойство, — и пять законов при нём: дистрибутивность, идемпотентность, частичный порядок, монотонность, коммутативность. Каждое заводится ради своего разрешения, а не ради полноты списка: повторить, разложить свёртку, переписать выражение, сравнить состояния, кешировать. Поверхность, границы честности, недостачи и настоящие примеры — в flang/cat/ZAKONY.md.

свойство «коммутативность»
  носитель «Частичный итог»
  операция «Слить итоги»

Ноль новых слов: свойство было ключевым и раньше (предел утилиты внутри утилита), а верхнеуровневого свойство в дереве не было ни одного — эта запись занимает то, что было ошибкой разбора.

Для монады добавляется форма связывания, потому что без неё она бесполезна:

в монаде «Возможно»
  пусть заказ равно «Найти заказ» от номер
  пусть остаток равно «Проверить остаток» от заказ
  возврат «Отгрузить» от заказ и остаток

Это do-нотация словами: каждое пусть — связывание, возврат — возврат монады. Слово здесь то же, что и в объявлении, и это не экономия: возврат «Обернуть» называет η, возврат выражение её применяет. Задуманное вернуть отвергнуто измерением — оно стоит голым именем переменной в flang/examples/rosetta/towers-of-hanoi.flang, и ключевое слово сломало бы этот файл; тот же счёт, по которому уже потеряны «символы», «группа», «обратный», «на», «начальное» и «порог».

Разворачивается компилятором в вызовы объявленных возврат и соединение, внутри разбора; никаких функций первого класса не требуется, потому что тело известно синтаксически и печатается прямо в ветвь разбор. Обещание проверено: узла формы в AST нет, печать во все восемь целей получает её даром, а self/parser.flang и self/types.flang не потребовали ни одной правки.

Отображение эндофунктора не объявляется и не проверяется: у полиномиального функтора оно ровно одно, и компилятор выводит его из устройства типа. Цена — параметр обязан стоять в поле целиком, поэтому список и всё рекурсивное монадой сегодня не объявить.

Эффекты и HTTP

Требование «мочь http на нём писать» — самое дорогое, и решается оно одним словом: язык остаётся чистым.

вариант «Прочитать файл» с путь равным "адрес.txt" не читает файл. Оно строит описание действия — обычное значение обычной суммы типов. Читает файл хозяин: среда, в которую напечатан модуль.

Сделано. Поверхность вышла не той, что задумывалась здесь, и расхождение одно, зато крупное: это не монада. Почему — ниже, в отдельном разделе, и это самая важная часть главы. Реализация: flang/src/io.mjs (словарь и исполнитель), flang/src/host/node.mjs (хозяин для Node), flang/examples/io/link-report.flang (программа, которая читает файл, ходит в сеть и пишет отчёт).

Словарь поручений — пять действий, и набор закрыт

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

тип «Поручение»            // что программа просит сделать
  вариант «Прочитать файл» содержит путь: строка
  вариант «Записать файл» содержит путь: строка, содержимое: строка
  вариант «Запросить» содержит способ: строка, адрес: строка, тело: строка
  вариант «Текущее время»
  вариант «Случайное число»

тип «Отклик»               // что хозяин принёс обратно
  вариант «Пока ничего»                                    // первый шаг
  вариант «Прочитано» содержит содержимое: строка
  вариант «Записано» содержит сколько: число
  вариант «Ответ сети» содержит код: число, тело: строка
  вариант «Отметка времени» содержит миллисекунды: число
  вариант «Выпало» содержит значение: число
  вариант «Сбой» содержит код: строка, сообщение: строка

тип «Продолжение»          // что программа решила делать дальше
  вариант «Сделать» содержит поручение: «Поручение», потом: любое
  вариант «Конец работы» содержит значение: любое
  вариант «Провал» содержит код: строка, сообщение: строка

Пять поручений, и набор закрыт — это утверждение, а не текущее состояние. Полнота здесь дороже, чем кажется: каждое поручение обязан уметь исполнить КАЖДЫЙ хозяин, включая напечатанного в C. Пять — это то, что честно поддерживается везде; шестое пришлось бы либо писать восемь раз, либо объявлять «в некоторых целях не работает», а это уже не контракт.

«Сбой» — не исключение, а обычный вариант: «файла нет», «сеть не ответила» и «хозяин запретил» приходят программе одним и тем же путём, и она обязана уметь его встретить. Один путь на все неудачи — один и проверенный.

План: три строки и ни одного нового слова, кроме план

план «Сходить по ссылке»
  состояние «Ход»
  начинает с «Начать»
  обрабатывает «Дальше»

состояние, начинает с и обрабатывает уже ключевые — теми же тремя словами объявляется процесс, и это не экономия, а утверждение: план и процесс устроены одинаково. И там и здесь чистая функция получает «где мы были» и «что случилось», а возвращает «что делать»:

Одно новое слово план (plan). Проверено grep-ом по всем .flang и .fts репозитория на голое, не закавыченное вхождение: план — 0, plan — 0. Слово шаг отвергнуто: оно встречается голым семь раз (поле записи и переменная в flang/core/lexer.flang, накопитель свёртки в flang/examples/rosetta/fibonacci.flang) — ключевое слово запретило бы их и сломало бы два файла, к вводу-выводу отношения не имеющих. Это тот же счёт, по которому уже потеряны «символы», «группа», «обратный», «на», «начальное» и «порог».

Имена вариантов ключевыми словами не становятся вовсе — они пишутся в ёлочках, — но занятость проверялась и у них: «Готово» занято в flang/core/evaluate.flang, «Начало» — в flang/self/lexer.flang, поэтому в словаре стоят «Конец работы» и «Пока ничего».

Чем это не монада — и что изменится, когда появится полиморфизм

Монада ввода-вывода требует типа Действие А, параметрического по результату: без параметра не выразить соединение, которому нужен Действие (Действие А). Параметрических типов в языке пока нет (flang/PLAN.md, пункт 1), а ждать их здесь было нельзя: без ввода-вывода язык не читает файл СЕГОДНЯ.

Поэтому здесь машина продолжений, и разница называется прямо:

монада прячет продолжение в замыкании — «что делать с ответом»; здесь продолжение — ЗНАЧЕНИЕ объявленного автором типа.

Это дефункционализация монады, сделанная руками: ровно тот приём, которым PLAN.md собирается печатать функции первого класса. Что из-за этого потеряно — четыре пункта, и все четыре видны в коде:

1. Связывание не является выражением. пусть ответ равно «запросить» от адрес внутри тела функции написать нельзя. Каждая точка ожидания — это отдельный вариант состояния, объявленный автором. В примере link-report.flang их четыре, и они видны глазами.
2. Тип результата поручения не отслеживается. «Отклик» — одна закрытая сумма на все пять поручений, поэтому шаг обязан разбирать и заведомо невозможные случаи («Записано» после чтения). Монада сделала бы их невыразимыми; здесь их приходится отвергать явным случай любое.
3. Продолжение хранится в джокере. Поле потом имеет тип любое — тот же компромисс, что у поля что в действии отправить. Тип состояния известен (он назван строкой состояние «Ход»), но выразить «здесь лежит значение именно этого типа» нечем. Проверка ловит расхождение в двух местах: в исходнике — сверяя ВЫРАЖЕНИЕ в поле потом с объявленным состоянием, и на витке цикла — сверяя ЗНАЧЕНИЕ, пришедшее на вход шага, тем же checkArguments, каким проверяются --args, факты и значения примеров. Вторая сверка нужна и второму входу шага — отклику: его приносит ХОЗЯИН, которого компилятор не видел. До неё хозяину верили на слово наполовину («это вообще «Отклик»?» — и точка на имени варианта), и хозяин, вернувший «Отметка времени» с миллисекунды равным "вчера", доводил план до конца с результатом "мс: вчера". Правильно устроенный, но не тот вариант отклика границей не задет: его обязана встретить ветка случай любое программы.
4. Законов монады нет, потому что нет монады. Левая единица, правая единица и ассоциативность не проверяются: проверять нечего, соединение не объявлено. Проверять их ЕСТЬ чем — flang/src/monad.mjs сделан, — но здесь объявлять нечего до частичного применения (см. ниже).

Что изменится — и чего для этого не хватает, теперь измерено. Пункт 4 здесь говорил, что всё упирается в параметрический полиморфизм. Он появился, форма в монаде сделана (flang/cat/MONAD.md) — а машина продолжений на неё не переехала, и причина другая.

Монада ввода-вывода — это «Дело» от «А», где продолжение стоит полем типа функция из «Отклик» в («Дело» от «А»). Форма разворачивает отображение эндофунктора НА МЕСТЕ, разбором, поэтому требует, чтобы параметр стоял в поле целиком, и такой тип отвергает поимённо:

FLANG_MONAD  монада «Дело»: в варианте «Дальше» параметр «А» стоит внутри поля
             «потом», а не целиком; отображение внутрь применения на месте
             не разворачивается

Значит недостающее — не полиморфизм, а частичное применение (фаза 4 в flang/cat/HOF.md): без захвата продолжение не становится значением, а без значения отображение внутрь функции не написать. Обещание не отменяется, а получает верный срок. Машина останется — сменится тот, кто её пишет. Программы, написанные сегодня, продолжат работать: они пишут то, во что компилятор станет разворачивать в монаде.

Проверяемость без единого эффекта — главное свойство

Описание действия сравнивается с ожидаемым описанием, значит функция с вводом-выводом проверяется обычным примером:

тотальная функция «После чтения»
  принимает отклик: «Отклик»
  возвращает «Продолжение»
  пример «Содержимое файла становится адресом запроса»
    дано отклик равно вариант «Прочитано» с содержимое равным "http://пример\n"
    ожидается вариант «Сделать» с поручение равным (вариант «Запросить» с способ равным "GET" и адрес равным "http://пример" и тело равным "") и потом равным (вариант «Пишем отчёт»)
  пример «Отказ хозяина становится отказом плана, а не молчанием»
    дано отклик равно вариант «Сбой» с код равным "FLANG_IO_READ" и сообщение равным "нет такого файла"
    ожидается вариант «Провал» с код равным "FLANG_IO_READ" и сообщение равным "нет такого файла"

Ни файла, ни сокета при этом нет. Отсюда два свойства, которые обычно теряются вместе с чистотой:

• программа, ходящая в сеть, остаётся ТОТАЛЬНОЙ. Все семь функций link-report.flang доказаны тотальными: завершается описание, а ждёт ответа хозяин. Сеть не входит в язык, поэтому доказательство не портится;
• путь отказа проверяется тем же примером, что и путь успеха — «что делать, если файла нет» пишется и проверяется рядом с «что делать, если файл есть».

Целый план тоже прогоняется без эффектов: runPlan принимает функцию «выполнить поручение», и подставленный список заготовленных откликов даёт журнал выданных поручений — сверять есть что, выполнять нечего.

Полномочия принадлежат хозяину

flang io <файл> исполняет план, и ключи --no-read, --no-write, --no-net, --no-clock, --no-random, --in-dir сужают полномочия хозяина. Запрещённое поручение возвращается откликом «Сбой» с кодом FLANG_IO_DENIED.

Это не украшение, а то, ради чего чистота и нужна: описание действия можно прочитать ДО того, как оно случилось, и решить, случится ли оно вообще. Программа, пропущенная через факт-чекинг, не могла тайком сходить в сеть — в сеть ходит только хозяин.

Случайность приходит семенем (--seed N, генератор тот же mulberry32, что у планировщика конкурентности): прогон, который нельзя повторить, нельзя и проверить.

Граница честности

Сам HTTP пишется не на flang. На flang пишется то, что запрос описывает и что с ответом делать, — то есть логика, которую и надо проверять. Обещать, что на языке без эффектов появится сокет, было бы обманом.

Слой исполнения по целям: сделан один из восьми

Печать программы с планом уже работает во всех восьми целях — и это не обещание, а проверенный факт: flang emit --target c на link-report.flang даёт код, который собирается cc -std=c99 -Wall -Wextra -Werror -pedantic и на вход {"fn":"Дальше","args":[{"v":"Читаем адрес","f":[]},{"v":"Пока ничего","f":[]}]} отвечает тем же описанием поручения, что интерпретатор. Причина проста: план — это две обычные функции и три обычные суммы, а бэкенды печатают их как всё остальное.

Чего в семи целях нет — цикла хозяина (сорок строк: позвать начальное состояние, звать шаг, разбирать «Продолжение») и пяти исполнителей поручений. Что для этого нужно каждой цели:

Отсюда решение для двух последних, и оно то же, что было записано в первой редакции этой главы: в C хозяин передаётся снаружи — указателем на функцию fl_io_perform(поручение) → отклик, а по умолчанию все поручения отвергаются кодом FLANG_IO_DENIED. Это не полумера, а признание устройства: библиотека на C, которая сама лезет в сеть, — не библиотека. То же годится и для Rust, если зависимость от крейта нежелательна.

Собственная mulberry32 в каждой цели — не прихоть: rand(), math/rand и Random дают разные последовательности, и обещание «одно семя — один прогон» перестало бы выполняться при переносе. Генератор укладывается в шесть строк целочисленной арифметики ровно поэтому (см. conc.mjs, makeRandom).

Чего нет и в сделанной цели: дифференциальной сверки самого хозяина. Шаг плана — чистая функция, и он сверяется наравне со всем остальным; а вот «прочитать файл в Go и прочитать файл в Node дают один и тот же «Отклик»» сегодня не проверяется ничем, кроме этой таблицы. Это долг, и он записан здесь, а не забыт.

Неизменяемые структуры данных

Значения flang неизменяемы уже сейчас — это свойство языка, а не библиотеки. Не хватает эффективных структур: добавить копирует список целиком у целей печати, и на длинных списках это квадратично по времени (в C было ещё и по памяти — уже исправлено продлением последней выдачи в арене; у эталонного вычислителя цена стала постоянной 15 августа 2026 — flang/src/builtins.mjs, «Список с запасом»).

В стандартную библиотеку добавляются персистентные структуры, у каждой — объявленный моноид или группа там, где он есть:

Все они — обычные модули на flang, а не встроенные типы: значит печатаются во все восемь языков и проверяются той же сверкой.

Граница честности: доказано против проверено

Это главный раздел. Смешивать эти две вещи нельзя, а соблазн велик, потому что слово «доказуемый» звучит одинаково в обоих случаях.

Доказывается компилятором — утверждение обо всех входах:

• завершение — анализ убывания: по части значения или по числовой мере; функция, помеченная тотальная, завершается на любом входе. Это настоящее доказательство;
• типы — совпадение доменов и кодоменов, исчерпывающность разбора, корректность композиции: «Б» после «А» не соберётся, если кодомен «А» не равен домену «Б»; цепочка не соберётся, если рвётся в середине;
• согласованность отображений функтора и бифунктора — у каждого написанного образа (у бифунктора — у каждой пары) типы сходятся, композиции и единицы сохраняются;
• две аксиомы категории — замкнутость под композицией и наличие единицы у каждого объекта, там, где категория назвала свои стрелки;
• устройство своего равенства категории — объект стоит на конце её стрелки, равенство у него одно, названная функция берёт два входа этого объекта и возвращает признак. Не сошлось — FLANG_CATEGORY_EQUALITY_SHAPE, FLANG_CATEGORY_EQUALITY_TWICE, FLANG_CATEGORY_EQUALITY_OUTSIDE;
• устройство естественного преобразования — оба функтора объявлены и параллельны, у каждого отображённого объекта ровно одна компонента, и её концы — образы этого объекта у первого и второго функтора. Не сошлось — FLANG_TRANSFORM_SHAPE, FLANG_TRANSFORM_COMPONENT, FLANG_TRANSFORM_NOT_TOTAL;
• полнота отображений функтора — каждой стрелке категории домена сопоставлен образ, и образ лежит в категории кодомена. Строка эта долго стояла здесь ОБЕЩАНИЕМ БЕЗ СОДЕРЖАНИЯ: пока категория не объявлялась, «каждой» было словом без числа, и функтор, отобразивший две стрелки из пяти, проходил проверку молча. Считается там и только там, где домен объявлен категорией; не объявлен — остаётся допущением автора;
• устройство изоморфизма — концы обеих стрелок сходятся крест-накрест, а единицы обоих объектов объявлены;
• устройство отношений множеств (flang/cat/SETS.md) — у вложения оба множества объявлены, а написанное даёт «Ф» принимает ровно один вход нужного вида; у общей части объемлющее множество объявлено, обе стороны в него вложены объявленным вложение, имя свободно, стороны различны, и общая часть у пары одна. Не сошлось — свои коды FLANG_EMBED_SHAPE, FLANG_MEET_NO_UNIVERSE, FLANG_MEET_NAME_TAKEN, FLANG_MEET_SAME_SIDE, FLANG_MEET_TWICE;
• устройство реализации стрелки — даёт «Ф» принимается тогда и только тогда, когда «Ф» объявлена, принимает ровно один вход, и вход этот — домен, а результат — кодомен. Не сошлось — FLANG_MORPHISM_SHAPE;
• устройство перевода данных у связи модулей — то же самое и по тем же доводам, только концы другие: вход перевода — объект-источник, результат — его образ у функтора. Не сошлось — FLANG_FUNCTOR_TRANSLATION;
• исчерпанность монадического блока — в монаде без возврат не соберётся; устройство монады — тип параметричен, возврат ведёт из «А» в M«А», соединение из M(M«А») в M«А», а параметр стоит в полях целиком, значит отображение эндофунктора выводится однозначно и функториально;
• форма плана ввода-вывода — начинает с называет функцию без аргументов, возвращающую объявленное состояние; обрабатывает — функцию (состояние, «Отклик») → «Продолжение». Не сошлось — FLANG_PLAN, а не общий FLANG_TYPE: по коду машина понимает, что чинить.

Проверяется на примерах и сетке входов — утверждение о конечном множестве:

• естественность преобразования (коммутативность квадрата) — сделано (flang/src/setoid.mjs, FLANG_TRANSFORM_NOT_NATURAL) там, где категория кодомена объявила своё равенство, а все четыре стрелки квадрата реализованы; иначе преобразование уходит в assumed;
• пять объявляемых свойств — дистрибутивность, идемпотентность, частичный порядок, монотонность, коммутативность — сделано (flang/cat/ZAKONY.md). Устройство каждого доказано сличением объявлений (FLANG_PROPERTY_SHAPE, FLANG_PROPERTY_UNKNOWN, FLANG_PROPERTY_TWICE), сам закон посчитан на сетке значений автора, а из посчитанного выдано ИМЕНОВАННОЕ разрешение — отдельным разделом ведомости. Нарушение разрешения не даёт, и строка закона говорит «НАРУШЕНО», а не «нарушений не найдено». Сломанный частичный порядок ОСТАНАВЛИВАЕТ монотонность: она уходит «на веру», а не краснеет;
• законы монады: левая единица, правая единица, ассоциативность связывания — сделано, сетка берётся из примеров автора, а сообщение называет контрпример (flang/src/monad.mjs);
• законы моноида и группы;
• любой закон при морфизме — сделано, и проверяет его flang test, а не flang check: примеры автора проверяет ровно эта команда. Отчёт называет и стрелку, и закон (flang/src/compat.mjs). У НЕТОТАЛЬНОЙ стрелки проверка идёт под названным пределом шагов, и упор в предел — свой код FLANG_LAW_LIMIT: «не досчитано» — это не «нарушено», и путать их отчёт не вправе;
• обратимость изоморфизма — сделано там, где обе стрелки реализованы (flang/src/iso.mjs, FLANG_ISO_NOT_INVERSE); пара без даёт остаётся допущением автора, и проверка о ней молчит;
• три закона категории со своим равенством — сделано (flang/src/setoid.mjs): что объявленное равенство есть эквивалентность, что композиция его уважает и что композиция ассоциативна. Категория без равенства уходит в assumed. Сила проверки ассоциативности названа в разделе «Равенство морфизмов» прямо: композиция вычисляется применением, значит на реализованных стрелках она подтверждает, а не устанавливает;
• квадрат связи модулей — «перевести и сделать» = «сделать и перевести»; сделано там, где у объектов написан даёт (flang/src/functor.mjs, FLANG_FUNCTOR_SQUARE). Связь без переводов уходит в assumed. Сообщение предъявляет контрпример, а отчёт называет ещё и число РАЗЛИЧНЫХ исходов сетки: на постоянной сетке параллельные пути равны при любой реализации, и такую проверку нельзя выдавать за проверку молча;
• инъективность вложения и непустота общей части — сделано (flang/src/sets.mjs, FLANG_EMBED_NOT_INJECTIVE). Граница внутри этих двух проверок разная, и это записано в flang/cat/SETS.md: склейка у вложения — предъявленный контрпример и потому ОШИБКА, а ненайденный свидетель у общей части — не ошибка вовсе, потому что «не нашли» на конечной сетке не значит «нет». Такие отношения уходят в отдельный список assumed, и flang check о них молчит. Универсальность общей части (что она самая большая) не проверяется ничем и остаётся допущением автора — как и обратимость без даёт;
• свойства утилит — так уже работает FTS.

Одна строка из этого списка ушла вверх, в доказанное: законы функториальности и бифункториальности проверять на сетке не пришлось — они решаются сличением объявлений, потому что морфизм это объявление, а не значение. Обратимость изоморфизма уходила отсюда в сторону, в «не проверяется вовсе», и вернулась: условие возврата было названо тогда же — «сетка появится, когда у морфизма появится даёт». даёт появился.

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

Проверяется при выполнении — то, что заказано словами «и в runtime»:

напечатанный код по умолчанию проверяет требует, закон и законы структур на фактических значениях и отвечает диагностикой с кодом при нарушении. Это не доказательство, а страховка на настоящих данных: она ловит то, чего не было в сетке. Отключается ключом печати --без-законов — явным решением, а не умолчанием.

Чего нет и не будет без отдельной большой работы: доказательств свойств для всех входов. Для этого нужен либо SMT-решатель (тогда доказуемы линейная арифметика и равенства, но не всё), либо зависимые типы (тогда доказательство пишет автор, и язык перестаёт быть простым). Пока ни того ни другого нет, документация обязана говорить «проверено на N входах», а не «доказано».

Формулировка для README и курса: завершение доказано, типы доказаны, законы проверены — при компиляции на сетке, при выполнении на фактических данных.

Встраиваемость

Требование «вкорячить модуль в другой язык» наполовину выполнено.

Что есть. Бэкенд C печатает готовую библиотеку — <модуль>.c, <модуль>.h, рантайм, Makefile — и точку динамического вызова:

fl_status spiski_call(fl_ctx *ctx, const char *name, const fl_value *args,
                      size_t count, fl_value *result, fl_error *error);

Плюс прогонщик по JSON через трубу — работает из любого языка с подпроцессами. Остальные семь целей печатают пакет, крейт, модуль или сборку.

Чего не хватает:

1. Упаковки — package.json, go.mod, Cargo.toml, pyproject.toml, pom.xml, mix.exs. Сейчас напечатанное кладут в проект руками.
2. Обёртки под хозяина — вызывающий работает с fl_value вручную. Нужен слой, где функция flang видна как обычная функция языка-хозяина с его типами.
3. Границы ошибок — fl_error обязан становиться исключением в Java и Python, Result в Rust, вторым значением в Go, {:error, …} в Elixir.
4. Владения памятью — в C результат живёт в арене до fl_arena_reset; это обязано быть либо скрыто обёрткой, либо явно описано в её документации.

Отдельно про TypeScript. Вставки утилит в стиле FTS уже работают: ftsc печатает модель в TypeScript, а курс показывает это вкладкой «codegen» с проверкой, что показанный код байт в байт совпадает с напечатанным. Для монад и морфизмов нужен тот же путь: печать в TypeScript, где морфизм становится функцией, а в монаде — цепочкой вызовов.

Что это даёт связке «разработчик и ИИ»

Заявленная цель — чтобы проверяемый код мог писать не только человек. Отсюда требование к поверхности: диагностика обязана быть пригодна для машины. Это уже так — ошибки идут как { code, message, severity, span } в JSON — и должно сохраниться для новых конструкций. Несовпадение композиции, нарушенный закон функтора, необратимый изоморфизм, разорванная цепочка обязаны давать свой код, а не общий FLANG_TYPE: по коду машина понимает, что чинить.

Порядок работ

Разбито так, чтобы каждый шаг проверялся сверкой и ничего не ломал.

1. ✅ Категория, объект, морфизм, композиция, единица, цепочка — и закон при стрелке: даёт «Ф» называет функцию, которая стрелку считает, закон несёт примеры, на которых обещание проверяется. Устройство реализации доказывается (FLANG_MORPHISM_SHAPE), сам закон проверяется flang test и при падении называет и стрелку, и закон. Обратная совместимость: существующие функция работают без изменений, а стрелка без блока — прежняя стрелка, с тем же AST байт в байт. ✅ Категория называет свои стрелки (2026-08-14) — две её аксиомы, замкнутость под композицией и наличие единиц, ДОКАЗЫВАЮТСЯ сличением объявлений. ✅ Равенство морфизмов (2026-08-15) — категория объявляет своё отношение равенства на значениях объекта (объект «Х» даёт «Ф», ни одного нового слова), равенство стрелок выводится поточечно. Устройство доказывается; эквивалентность, согласованность с композицией и АССОЦИАТИВНОСТЬ проверяются на сетке. Категория без равенства уходит в «на веру». Остаток назван: композиции нужен собственный даёт, чтобы ассоциативность могла краснеть и на честной программе.
2. ✅ Функтор и бифунктор — три закона у каждого, и все ДОКАЗЫВАЮТСЯ, а не проверяются на примерах, как здесь предполагалось. Четвёртый — полнота на категории домена — появился вместе с категорией и до неё был обещанием без содержания. Общий вид бифунктора с переменными типа ждёт параметрического полиморфизма.
3. ✅ Моноид и группа — устройство доказывается, законы проверяются на сетке. Объявлений для существующих операций stdlib пока нет. ✅ Изоморфизм — устройство доказывается; обратимость проверяется на сетке там, где обе стрелки реализованы через даёт, и остаётся допущением автора там, где хотя бы одна — нет.
4. 🟡 **Монада и форма в монаде — СДЕЛАНЫ**; естественное преобразование — нет. Порядок вышел обратным задуманному, и это не небрежность: монаде преобразования не понадобились вовсе — η и μ названы обычными функциями, как операция у моноида. Предусловием оказался параметрический полиморфизм, и это не хотелка: имена вариантов уникальны на модуль, поэтому M(M) — отдельный тип с другими конструкторами, а законы монады трогают M³. Он сделан, и монада на нём выражается. Устройство монады доказывается, три закона связывания проверяются на сетке, форма разворачивается внутри разбора и печатается во все восемь целей даром: flang/cat/MONAD.md. Осталось преобразование — «из функтора «Список» в функтор «Возможно»» говорит про одну и ту же «А» в двух местах, и это фаза 3 в flang/cat/POLY.md. ✅ Естественное преобразование — СДЕЛАНО 2026-08-15, и порядок опять вышел обратным: предусловием оказалась не фаза 3, а равенство морфизмов — квадрат коммутирует есть равенство двух композиций. Объявляется тем же словом морфизм (преобразование ЕСТЬ морфизм в категории функторов), новых слов в таблице лексера ноль, прибавился один падеж. Устройство доказывается, закон естественности проверяется на сетке и КРАСНЕЕТ НА ЧЕСТНОЙ ПРОГРАММЕ — в отличие от ассоциативности. Осталась от шага 4 ровно фаза 3: преобразование между функторами над ПРИМЕНЕНИЯМИ параметрических типов («из функтора «Список» в функтор «Возможно»»).
5. Проверка законов в напечатанном коде — во всех восьми целях.
6. 🟡 Ввод-вывод — сделан, но НЕ монадой: машина продолжений, потому что монада упирается в шаг 1 (см. «Чем это не монада»). Слой исполнения сделан для одной цели из восьми — Node; печать программы с планом работает во всех восьми, чего не хватает семи — расписано в таблице выше.
7. Персистентные структуры в stdlib.
8. Упаковка и обёртки для восьми языков.
9. ✅ Связь модулей (2026-08-16) — интерфейс модуля объявляется его категорией, связь между модулями остаётся функтором, а нового в записи одно: даёт «Ф» у объекта функтора называет перевод данных. Устройство перевода доказывается, квадрат проверяется на сетке и предъявляет контрпример. Отдельной правкой закрыта дыра, без которой глава была бы пустой: связывание модулей не переносило категорий, и полнота связи МЕЖДУ МОДУЛЯМИ — то есть там, где она и нужна, — не проверялась вовсе. Что этот слой не проверяет и не будет — записано в его главе отдельным разделом, поимённо.
10. ✅ Отношения множеств — подобъект и предел (flang/cat/SETS.md). вложение даёт мономорфизм, пересечение — расслоенное произведение над объемлющим объектом. Устройство обоих доказывается сличением объявлений, инъективность и непустота проверяются на сетке автора, а универсальность общей части остаётся допущением и следствий из неё компилятор не выводит. Объединения среди слов нет: ко-произведение в языке уже есть.

Шаги 1–4 не трогают печать, поэтому идут параллельно с текущей работой. Шаг 5 затрагивает все восемь бэкендов и делается после того, как они устоятся.