flang — спецификация

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

1. Два режима — главное архитектурное решение

Полнота по Тьюрингу и гарантия завершения несовместимы. Поэтому язык не выбирает одно, а разделяет программы на два класса, и класс проверяется компилятором, а не декларируется в документации.

Строка о печати требует уточнения, потому что первая редакция этой таблицы обещала «только JS/TS», а бэкенды печатают обычные функции во все цели — проверено на flang emit --target c для нетотального решения задачи 509. Правда такова:

• печать не ограничена классом ни в одном бэкенде, и запрещать её было бы неверно: обычная функция — законная часть языка, а не полуфабрикат;
• лимиты воспроизведены во ВСЕХ восьми целях. В C, Go, Rust, Python, Java, C#, Elixir и JavaScript незавершающаяся функция упирается в лимит и даёт FLANG_RECURSION_LIMIT. Шагом везде считается вход в функцию, оборот цикла хвостового самовызова и отскок батута; шаг интерпретатора мельче (замер: в 19–20 раз на той же работе), поэтому при одинаковом пределе он упирается первым, и напечатанный код не объявит исчерпанным то, что интерпретатор досчитал. Предел глубины есть везде, включая C, потому что переполнение стека в C — падение процесса, а не исключение. В семи целях из восьми совпадают и код, и ТЕКСТ отказа;
• счётчик глубины держит обещание только пока предел НИЖЕ стека хозяина, и стек этот теперь отводится под предел, а не достаётся какой есть. Счётчик считает кадры, а несёт их стек, и сколько их влезет, зависит от толщины кадра, то есть от программы. Замер холодными процессами (cc 15.2, -O2, стек 8 МиБ): у нехвостовой функции с одним параметром влезает 23 807 кадров (352 байта на кадр; -fstack-usage объявляет 464 сверху) — запас над объявленными 10 000 всего двукратный, — а у функции с сорока локальными связываниями только 1 518 (5 526 байт на кадр, объявлено 5 552). Разница между двумя ПРОГРАММАМИ — шестнадцатикратная, и вторая умирала на пределах ПО УМОЛЧАНИЮ: SIGSEGV, без кода, без текста, без возможности перехвата, тогда как интерпретатор на том же входе отказывает честно. То есть объявленный предел глубины пределом НЕ БЫЛ.

Закрыто тем же приёмом, которым закрыт Python, и второй половиной сверх него:

1. Пробег на потоке с ЯВНО ЗАДАННЫМ стеком, и размер соотнесён с пределом. fl_stack_wanted(max_depth) — max_depth кадров по 16 КиБ, в границах [8 МиБ, 1 ГиБ]. 16 КиБ не с потолка: cc -fstack-usage по всему корпусу репозитория (7 896 функций из 157 программ) дал ХУДШИЙ кадр 6 496 байт — у самого компилятора flang (Замены кириллицы из self/emit-c.flang), — и 16 КиБ несут его с запасом в 2,5 раза. Считать по средней программе было бы неверно: предел обещан всем, значит стек обязан нести худшую.

От компилятора C толщина кадра зависит куда меньше, чем от программы, и это тоже замерено: у ОДНОЙ И ТОЙ ЖЕ худшей функции gcc 15.2 даёт 6 496 байт при -O2 и 6 736 при -O0, clang 21.1 — 6 424 и 7 480. Разброс между двумя компиляторами на шесть мажорных версий врозь и обоими уровнями — 16 %, при запасе в 2,1 раза даже по самому толстому из четырёх. Поэтому число здесь не подгоняется под свой cc, а сторож и вовсе меряет БАЙТЫ настоящего кадра в настоящем прогоне: смена компилятора двигает запас, а не обещание.

1. **Сторож остатка стека в fl_enter — там же, где уже сходятся оба предела, а не третьим механизмом.** Никакой размер стека не покроет ЛЮБУЮ толщину кадра, поэтому вход в функцию сверяет ещё и остаток: запас под последним входом считается по самому толстому кадру, который эта программа уже показала. Исчерпание переводится в объявленный FLANG_RECURSION_LIMIT с текстом про хозяина — дословно тем же, что печатает JavaScript.

Цена в памяти — адресное пространство, а не расход: при пределе 10 000 поток просит 168 МиБ, а резидентно программа берёт ровно столько, сколько кадров коснулась (замер: VmSize 224 МиБ, VmRSS 54 МиБ на спуске до 10 000; на мелком вызове RSS растёт на 4 КиБ — на управляющий блок потока и только). Цена во времени — 0,6 нс на вход в функцию (минимум из семи прогонов по 10 млн входов: 65,7 нс против 65,1 нс со снятым сторожем), то есть меньше процента самого дешёвого входа. Под объявленным пределом адресного пространства стек берёт не больше ЧЕТВЕРТИ его — иначе он отнимал бы память у арены, и глубина покупалась бы отказом в другом месте (это нашлось замером: под ulimit -v 16384 восьми мегабайт стека хватало, чтобы прогон конкурентности перестал доходить до исхода). Где четверти не хватает и на системный минимум, поток не заводится вовсе, и обещание держит сторож: отказ объявленный, просто предел ниже.

Планировщик конкурентности (emit/c/flang_conc.c) с этим не спорит, а выигрывает: он обнуляет счётчик глубины на каждом пробеге обработчика, а стек к тому моменту уже подъеден его собственными кадрами — сторож меряет байты и потому прав там, где счётчик кадров был бы слеп.

Rust вылечен тем же приёмом. Поток с заданным стеком там был и раньше, но размер стоял константой 512 МиБ и не поднимался вместе с --max-depth: при 500 000 программа умирала не отказом, а fatal runtime error: stack overflow, aborting. Теперь стек считается из объявленного предела (rt::stack_wanted), и в Ctx::enter стоит тот же сторож. Замер: на той же функции с сорока связываниями --max-depth 500000 теперь ДОСТИГАЕТСЯ, а предел, поднятый запросом выше отведённого стеку, даёт объявленный отказ про хозяина на глубине около 101 000 вместо аварийного останова.

Go этим приёмом не лечится, и это измерено, а не предположено. У горутины нет явного размера стека: он растёт сам, ПЕРЕЕЗЖАЯ на новое место, поэтому отметка стека, снятая на входе в расчёт, после первого же переезда не значит ничего — проба показала разность то −28 МиБ, то −200 МиБ, то +616 байт на монотонно растущей глубине. Сторожа по адресам в Go завести нельзя. Растущий стек зато снимает вопрос по умолчанию: на той же функции с сорока связываниями Go проходит 70 788 кадров (кадр 15,2 КиБ, потолок горутины 1 ГиБ) и до объявленных 10 000 доходит с семикратным запасом, отказывая текстом эталона. Выше потолка Go остаётся смертельным: fatal error: stack overflow, и поднять потолок нечем — debug.SetMaxStack(8 ГиБ) рантайм срезает до 2 ГБ (проверено). Значит про Go честно ровно это: предел ПО УМОЛЧАНИЮ несётся стеком и отказ объявленный; предел, поднятый выше того, что несёт горутина, — не несётся, и там Go умирает.

Что долг был не про выдуманную программу, видно на самой близкой: **точка раскрутки bootstrap/ — компилятор flang, напечатанный в C, — умирала по SIGSEGV на исходнике из вложенных скобок.** flang_cli check на файле с 4 000 уровнями вложенности давал сигнал 11 и код возврата 139, не сказав ни слова; та же точка, перепечатанная после починки, отвечает FLANG_RECURSION_LIMIT: функция «Разобрать дизъюнкцию» превысила предел глубины вызовов (20000) и кодом возврата 1. Компилятор, который молча умирает на пользовательском файле, — это ровно тот случай, ради которого набор видов отказа и делался закрытым.

Проверяется всё это flang/test/emit-depth.test.mjs на худшей форме, а не на средней, и с зубами: тот же напечатанный C собирается там ТРЕМЯ способами — как печатается (предел 10 000 достигнут), без потока (объявленный отказ про хозяина) и без потока со снятым сторожем (SIGSEGV). Последний вариант и есть доказательство изъятием: выломают починку — тест покраснеет, а не промолчит;

• в JavaScript объявленных 10 000 кадров не существовало НИ ДЛЯ ОДНОЙ программы, и теперь они есть. Здесь стояло, что предел глубины упирается в стек хозяина раньше, чем в себя, «а поднять стек изнутри модуля нечем: в Python это делает поток с заданным стеком, в JS такого рычага нет». Первая половина была верна и хуже, чем написано, вторая — просто неверна.

Замер холодными процессами (Node 26.7, стек V8 по умолчанию): у самой тонкой рекурсивной функции — один параметр, ни одного связывания — влезает 7 386 кадров, у функции с сорока живыми связываниями 1 379, у функции с двумястами 304. То есть объявленное число не было пределом ни при каких условиях: до него не доходила даже тонкая, а отказ приходил НЕ ТОТ — текст называл хозяина там, где интерпретатор на том же входе называет предел. Это расхождение в НЕбезопасную сторону: напечатанный код объявлял исчерпанным то, что интерпретатор досчитывает.

Рычаг оказался тот же, что в Python и C: поток с ЯВНО ЗАДАННЫМ стеком — worker_threads и resourceLimits.stackSizeMb. Замер, сколько кадров несёт стек заданного размера, дал 137 Б на кадр у тонкой формы, 733 Б у сорока связываний и 3 310 Б у двухсот (линейно, ≈16 Б на живое связывание). Отсюда цена кадра в расчёте — 8 КиБ, вдвое с лишним больше худшего измеренного, тем же правилом, каким взяты 16 КиБ у FL_STACK_PER_FRAME в C; под объявленные 10 000 кадров это 79 МиБ стека. На нём все три формы доходят до предела ЯЗЫКА (10 001) и отказывают текстом эталона, включая ту, что до починки умещалась в 304 кадра.

Обычный запуск рычаг получил не сразу. Сперва он работал только через $callDeep, то есть только когда его зовут руками, — а у цели не было прогонщика, единственной из восьми, и «запустить программу» означало «позвать функцию напрямую», на стеке вызывающего. Теперь прогонщик есть (src/emit/js/flang_cli.js, печатается по умолчанию, снимается --no-cli), и весь прогон идёт в потоке со стеком под объявленный предел — ровно как fl_call_deep вокруг всего прогонщика в C и rt.call_with_deep_stack вокруг serve в Python. Поток заводится ОДИН на процесс, а не один на запрос: он стоит 38 мс, а запросов в трубе сколько угодно. Размер стека не считается дважды: он посчитан при печати тем же $stackMb и приезжает в модуле полем $PROGRAM.stackMb.

Чего у цели по-прежнему нет, и это сказано числом, а не умолчанием:

• прямой вызов экспортированной функции считает на стеке того, кто позвал: рычаг работает через прогонщик либо через $callDeep. Ровно так же устроен C — библиотека, вызванная мимо fl_call_deep, считает на стеке вызывающего;
• в браузере рычага нет — worker_threads там не существует, а стек Worker'а не настраивается; прогонщик туда и не едет: он соседний файл, а не часть модуля, и модуль без него полон;
• выше 131 072 объявленных кадров стек упирается в потолок 1 ГиБ (замер: 1 474 617 кадров у формы с сорока связываниями).

Везде, где рычага нет, обещание держит сторож: переполнение стека переводится в объявленный FLANG_RECURSION_LIMIT — код из закрытого набора, — а текст честно называет хозяина, а не предел, до которого не добрались. Отказ всегда объявленный, и он никогда не зависание, не RangeError и не смерть вкладки. Проверяется это flang/test/emit-depth.test.mjs на той же худшей форме, что и C, и с теми же зубами: тот же напечатанный модуль зовётся ДВУМЯ способами — через $callDeep (предел 10 000 достигнут) и прямо (отказ про стек хозяина много раньше предела). Второй вариант и есть доказательство изъятием: выломают поток — первый сравняется со вторым, и тест покраснеет. То же самое, но уже на ОБЫЧНОМ запуске, проверяет flang/test/emit-js-cli.test.mjs: напечатанный каталог запускается настоящим процессом, и рядом стоит тот же вход прямым вызовом, который до предела не доходит (замер: 1 354 кадра против 10 001). Рассуждение и замеры — в шапке src/emit/js.mjs;

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

Ключевое следствие: вся существующая FTS-модель — это валидная программа flang, целиком лежащая в тотальном классе. Обратная совместимость не опциональна: flang обязан принимать любой .fts без правок и давать тот же результат, что ядро FTS. Это проверяется тестом на всех моделях репозитория.

Факт-чекинг (встраиваемый режим) допускает только тотальные функции: система, которая должна ответить «факт подтверждён или нет», не имеет права зависнуть.

2. Значения

Значение := Скаляр | Список | Запись | Вариант
Скаляр   := строка | число | признак | ничто
Список   := [Значение, …]                 однородный
Запись   := { поле: Значение, … }         объект FTS
Вариант  := Имя(Значение?)                конструктор суммы типов

Числа — IEEE-754 double, как в ядре FTS: расхождение по арифметике с уже сгенерированным кодом недопустимо. Точный натуральный тип нат (раздел 3) НОВОГО ВИДА ЗНАЧЕНИЯ НЕ ЗАВОДИТ: его значения — те же double, и восемь исполнителей о нём не знают ничего.

3. Типы

Тип := строка | число | нат | целое | признак | ничто
     | список Тип
     | «Имя объекта»          запись
     | «Имя типа»             сумма
     | «Имя типа» от Тип и Тип   применение параметрического типа
     | «Имя параметра»        параметр типа внутри своего объявления
     | ( Тип )                скобки (читаемость; применение и так правоассоциативно)
     | функция из Тип и Тип в Тип   тип функции (она же — значение)
     | Тип → Тип              он же, стрелочной записью

Точное натуральное: нат и целое

Три числовых имени, вложенных друг в друга (четвёртое, вес, — в следующем разделе):

нат ≤ целое ≤ число

нат — целое из отрезка [0, 2^53−1]; целое — целое из [−(2^53−1), 2^53−1]; число — любое конечное double. Это УТОЧНЕНИЯ, а не новые виды значения: носитель у всех трёх один, и всё, что принимало число, принимает его по-прежнему.

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

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

Чего нат НЕ делает: делить натурального не даёт (деление в flang — IEEE-деление); накопитель свёртки не уточняется (его тип обязан быть неподвижной точкой цикла, а объявить его негде); границы читаются только из сравнений имени с ЛИТЕРАЛОМ, но не имени с именем.

Зачем это нужно — раздел «Тотальность»: объявленный нат даёт убыванию и дно (0), и потолок (2^53−1), внутри потолка н минус c при целом c ≥ 1 точен, и постоянный шаг доказывается СТАТИЧЕСКИ — сторож в рантайме для этого класса не печатается вовсе. В ведомости это пятый носитель обещания, «точным шагом».

Отрезок с бесконечностью: вес

вес — неотрицательное число, у которого **+∞ есть значение, а не край**: отрезок [0, +∞]. Пишется пятью поверхностями — вес, стоимость, weight, pezo, 权重. Уточнение, не новый вид значения: носитель тот же IEEE-754 double, и +∞ в нём уже есть — все восемь целей печати давно умеют её записывать.

Вкладывается так: нат ≤ вес ≤ число. число в вес НЕ втекает, и это его главное свойство: у число дна нет вовсе, значит в нём живут и отрицательные, и «не число».

Зачем: стоимости, расстояния, таймауты, ёмкости — везде, где «бесконечность» значит «недостижимо» или «без предела». Обычная замена — сторожевое число (−1, ноль, 999999) — плоха тем, что участвует в арифметике наравне с настоящими: −1 побеждает минимум, ноль объявляет недостижимое бесплатным, 999999 однажды складывается с другим таким же. +∞ ведёт себя правильно сама: поглощает при сложении, нейтральна для минимума, больше всякого числа.

Что на весе разрешено, и почему именно это. Список закрыт и обоснован вычислением (flang/test/infinity.test.mjs, раздел УЛИКА):

Соглашение теории меры 0 · ∞ = 0 спасло бы замкнутость умножения и не взято: оно потребовало бы перехвата операции в рантайме у восьми целей, то есть носитель перестал бы быть тем же double — ради одной пары значений.

Какой моноид на нём есть, а какого нет. Есть моноид минимума (единица +∞) и максимума (единица 0): обе операции ВЫБИРАЮТ операнд и потому не округляют, ассоциативны точно, и обе единицы лежат внутри типа. Моноида по СЛОЖЕНИЮ нет, и язык это предъявляет отказом сборки:

FLANG_MONOID_ASSOC: моноид «Сумма»: операция не ассоциативна:
  на 0.1, 0.1, 0.6 слева вышло 0.8, справа 0.7999999999999999

Тот же отказ дословно приходит и на носителе число. Это не совпадение, а суть дела: ассоциативность ломает ОКРУГЛЕНИЕ, а не «не число», и убрать из структуры вычитание — значит убрать NaN, а не округление. Сложение остаётся в типе как замкнутая монотонная операция и как то, над чем минимум дистрибутивен точно (a + min(b,c) = min(a+b, a+c)) — это тропическое полукольцо, то есть буквально кратчайший путь.

Как из типа выйти. Доказать конечность сторожем: если д не больше 100 сужением снимает признак вместе с бесконечностью, и внутри такой ветви вычитание законно. Отказ снимается доказательством, а не приведением типа.

Цена, которую надо назвать. Литерала +∞ в языке нет: записать её можно только выражением, а ожидается … в примере принимает значение. Поэтому утверждения о недостижимости пишутся косвенно — сравнением, которое верно для неё и ложно для всякого числа (flang/examples/paths/shortest-path.flang).

Ядру доказательства объявленный вес даёт факт «не меньше 0» — тот же, что даёт нат, — и это не аксиома, а вывод из объявленного дна и проверки типов (flang/proof/reduce.mjs, сДномПоТипу). Замер прироста: node flang/scripts/weight-gain.mjs.

Точное десятичное: сотых и тысячных

Деньги, доли и проценты. Значение — ЦЕЛОЕ ЧИСЛО МИНОРНЫХ ЕДИНИЦ: рубль пятьдесят это 150 типа сотых, десятая доля — 10, две десятых — 20, и 10 плюс 20 равно 30 ТОЧНО. Это то же самое уточнение, что нат, плюс одно число — МАСШТАБ:

сотых     = целое из [0, 2^53−1], толкуемое как сотые доли
тысячных  = то же, тысячные

Почему не пара «мантисса + масштаб» и не дробь из двух целых: то и другое — НОВЫЙ ВИД ЗНАЧЕНИЯ, который увидели бы восемь целей печати, протокол JSON, мост FTS и побайтовая сверка самоприменения. Целое число минорных единиц не видит никто: kind остаётся "number", носитель — тот же double, в JSON едет то же число. Довод тот же, по которому нат сделан уточнением, и здесь он сильнее.

Что чинится этим типом — вычисление, а не рассуждение: на число 0.1 плюс 0.2 даёт 0.30000000000000004, (0.1 плюс 0.2) плюс 0.3 — 0.6000000000000001, а 0.1 плюс (0.2 плюс 0.3) — 0.6, то есть одно выражение в разном порядке даёт два ответа.

Масштаб ведёт себя как ЕДИНИЦА ИЗМЕРЕНИЯ, а не как границы:

Точно известное значение (литерал) годится в любом масштабе: цена плюс 50 — это «плюс пятьдесят копеек». Переполнение ловится тем же расширением, что у нат: за 2^53−1 теряется целость, а вместе с ней и масштаб.

Надевается масштаб РОВНО В ОДНОМ МЕСТЕ — в подписи: принимает сумма: сотых и возвращает сотых. Второе пропускает только целое внутри точной сетки: полкопейки копейкой не бывает. Аргумент вызова масштаба не надевает — иначе «Итог» от количество перестало бы быть ошибкой.

Ядро доказательства читает с этой подписи ТРИ факта: дно 0, потолок 2^53−1 и ЦЕЛОСТЬ. Третий — новый, и он несёт вес: правило а остаток от Л лежит в [0, Л−1] верно только для целого а (5.5 остаток от 2 равно 1.5).

Деление: решение названо, а не умолчано

Одна треть в десятичной записи не записывается — ни в двух знаках, ни в трёх, ни в скольких угодно. Значит у деления в точном типе есть ровно три исхода, и выбран из них ОДИН:

Что вместо деления, когда копейки терять нельзя. Деление С ОСТАТКОМ, где остаток не выбрасывается, а возвращается второй функцией: «Доля при дележе» и «Копеек в неделимом остатке». Сто копеек на три части — это 33 каждому и одна копейка неделимого остатка, и 33 · 3 + 1 = 100 ТОЧНО. Проверено вычислением на 501 сумме и шести делителях (flang/test/decimal.test.mjs).

Округления в языке нет ни явного, ни молчаливого: то, что нельзя разделить нацело, остаётся видимым остатком. Это и есть разница между «потерял копейку» и «знает, где копейка».

Чего точное десятичное НЕ делает сверх этого: знаковых денег (возврат, сальдо) нет — оба имени неотрицательны, как нат.

Функции первого класса

Функция является значением. Ограничение снято, и снято способом, который ничего не стоит ни печати, ни доказуемости, — дефункционализацией (Reynolds, 1972). Значение-функция это ТЕГ: функция «Удвоить» не строит замыкания, а называет объявленную функцию, а применение ф от 5 — это применить(тег, 5), один диспетчер с конечным списком случаев.

тотальная функция «Применить дважды»
  принимает ф: функция из числа в число, х: число
  возвращает число
  ф от (ф от х)

тотальная функция «Проба»
  возвращает число
  «Применить дважды» от функция «Удвоить» и 5

Что это сохраняет:

• печать в восемь целей. У пяти из них нет замыканий в том виде, что есть в JS. Тег и switch есть у всех восьми;
• доказуемость завершения. При настоящем высшем порядке «кто кого зовёт» неразрешимо. После дефункционализации граф вызовов конечен и известен целиком, и структурный анализ работает как прежде (flang/src/totality.mjs).

Цена названа честно и уплачена заранее: дефункционализация требует видеть ВСЮ программу, а раздельной компиляции у языка нет и не планируется. Отсюда же правило времени выполнения: применить можно только тот тег, который программа где-то строит формой функция «Имя». Тег, поданный снаружи через evaluate и нигде не построенный, отвергается кодом FLANG_APPLY — у диспетчера нет такого случая. Напечатанный код отвергает его тоже, но своими словами: случая нет и у напечатанного разбор, и отказ приходит кодом FLANG_MATCH_NOT_EXHAUSTIVE. Это единственное место, где напечатанное и интерпретатор расходятся текстом отказа, и почему иначе не выходит — в flang/cat/HOF.md. Без самого правила тотальность можно было бы обесценить законным по типам значением (комбинатор Ω выражается на одних тотальных функциях — там же).

Что из этого сделано на 2026-08-07. Разбор, проверка типов, анализ завершаемости, вычисление интерпретатором — и печать во все восемь целей: дефункционализация сделана одним проходом перед печатью (flang/src/defunc.mjs), после которого программа снова первопорядковая, а бэкенды печатают её теми же узлами, что и всегда. Напечатанное собрано настоящими тулчейнами и сверено с интерпретатором на сетке входов (flang/test/hof-emit.test.mjs).

Слои self/ новой формы по-прежнему не знают, поэтому ни одна программа репозитория — включая stdlib и examples — ею не пользуется и пользоваться не вправе, пока self/ не научится: корпус сверки с flang₁ собирается по маске каталога. Порядок оставшихся фаз — flang/cat/HOF.md.

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

Суммы типов

тип «Токен»
  вариант Слово содержит текст: строка
  вариант Число содержит значение: число
  вариант Конец

Коллекции

тип «Строка счёта» это список «Позиция»

Параметрические типы

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

тип «Возможно» от «А»
  вариант «Есть» содержит значение: «А»
  вариант «Ничего»

объект «Пара» от «Первый» и «Второй»
  первое: «Первый»
  второе: «Второй»

тотальная функция «Обернуть» от «А»
  принимает значение: «А»
  возвращает «Возможно» от «А»
  вариант «Есть» с значение равным значение

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

Монада и форма в монаде

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

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

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

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

Устройство монады доказывается сличением объявлений, три закона связывания проверяются на конечной сетке. Подробности, счёт занятых слов и границы — flang/cat/MONAD.md.

4. Синтаксис

Отступный, без скобок — как в FTS. Поверхностей четыре — русская, английская, эсперантская и китайская, — все равноправны и компилируются в один AST. Слова берутся из одной таблицы (flang/src/lexer.mjs, KEYWORDS), поэтому парсер не знает, на каком языке написан исходник; знает это только диагностика, чтобы цитировать слова той поверхности, на которой файл написан.

Поверхность не обязана быть полной. У восьми понятий из 138 на какой-то из поверхностей слова нет, и это записано в самой таблице поимённо с причиной: выбор слова в языке — решение владельца, а не подстановка из словаря. Файл на такой поверхности пишет недостающее понятие словом другой (examples/surfaces).

У китайской поверхности пробелов внутри фразы нет — слово там всегда один токен, — а полноширинные ： ， （ ） делят поток наравне с пробелом и значат ровно то же, что : , ( ).

Функция

тотальная функция «Длина»
  принимает элементы: список числа
  возвращает число
  разбор элементов
    случай пусто
      то 0
    случай голова и хвост
      то 1 плюс «Длина» от хвоста

тотальная требует, чтобы каждый рекурсивный вызов получал структурно меньший аргумент (хвост списка, поле варианта) либо параметр, уменьшенный на постоянный шаг и ограниченный снизу. Постоянным шагом годится и число (н минус 1), и другой параметр (н минус ш), если он приезжает в вызов неизменным и про него известно ш больше 0. Не доказал — ошибка FLANG_NOT_TOTAL.

У доказательства по числовой мере есть одна опора вне формы программы: числа — IEEE-754 double, и при большом |x| шаг x минус 1 не меняет x. Поэтому компилятор доказательством не ограничивается: на каждый доказанный мерой вызов он вставляет проверку убывания. Не убыло — FLANG_MEASURE, одинаковый у вычислителя и у всех восьми целей. Ни на одном входе тотальная не зацикливается: она либо завершается, либо отказывает.

Объявленная мера

Постоянный шаг покрывает не всё. У Евклида шаг а остаток от б зависит от значения, у деления пополам — (низ плюс верх) делить на 2; убывание там есть, но оно не в форме вызова, а в арифметике, и вывести его нечем. Такую меру называет автор:

тотальная функция «НОД»
  принимает а: число, б: число
  возвращает число
  убывает б
  если б равен 0
    то а
    иначе «НОД» от б и (а остаток от б)

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

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

Проверяется мера тем же приёмом, что и мера постоянного шага, и по той же причине: анализ проверяет форму обещания, а само обещание — сторож на каждом витке. Условий у него три:

Целость — не придирчивость. Именно на ней держится отказ от Евклида над вещественными числами: остатки пары (φ, 1) — 0.618, 0.382, 0.236 … — убывают строго, ограничены снизу и не кончаются никогда. «НОД» от целых работает всегда, «НОД» от (φ, 1) отказывает с FLANG_MEASURE на первом же витке.

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

Выражения

пусть имя равно выражение          локальное связывание
если условие то выражение иначе выражение
разбор выражения / случай …        сопоставление с образцом
«Имя функции» от аргумента         вызов по имени
функция «Имя функции»              функция как значение (тег)
значение от аргумента              применение значения-функции
поле записи                        доступ
Вариант с поле равным выражение    конструктор

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

Запятая закрывает поля конструктора, и их продолжает

Поля конструктора продолжает **только и. Запятая их закрывает всегда** — она принадлежит списку, и другого смысла у неё нет:

[вариант «М» с а равным 1 и б равным 2]   один элемент, два поля
[вариант «М» с а равным 1, б равен 2]     два элемента: он и сравнение

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

Разделить пришлось именно запятую, потому что она дешевле. Цена мерялась разбором всех 149 программ репозитория до и после — 91 на flang и 58 на поверхности FTS, которую читает тот же разборщик: запятая продолжала поля в семи местах двух файлов, и ни одного такого места не было внутри списочного литерала — значит ни одна программа не сменила смысл молча, обе отказали вслух, а после переписи семи мест на и деревья всех 149 совпали узел в узел.

Другие пути стоили дороже. Обязательные скобки вокруг конструктора-элемента: элементами списка стоят 502 конструктора в 21 файле, 440 из них уже в скобках — переписывать пришлось бы 62 места в 9 файлах. Отдельный знак между полями: 1665 конструкторов в 45 файлах. Разбор по объявленным именам полей не переписал бы ничего, но и неоднозначности бы не снял: он лишь заменил бы одну догадку другой, и разбор файла стал бы зависеть от того, что подключено (подключить).

и остаётся у полей и у аргументов вызова сразу, и разводится оно заглядыванием на два токена: поля выигрывают, только если дальше имя равным. Чтобы передать конструктор не последним аргументом, его берут в скобки.

Имена и падежи — важное правило

Ядро FTS решает этот вопрос однозначно: «Компилятор намеренно не угадывает грамматические падежи имён» (docs/language.md), поэтому в 10 процентов от поля сумма имя стоит без изменения формы.

По-русски конструкции вида «Длина» от хвоста и разбор элементов просятся в родительном падеже, и писать от хвост было бы насилием над языком, ради читаемости которого всё и затевалось. Поэтому flang делает один шаг дальше ядра, но не превращает это в угадывание:

• имя ищется в области видимости точным совпадением;
• если точного нет — сопоставление по неизменяемой основе среди уже связанных локальных имён (параметры, пусть, привязки образцов);
• совпало ровно одно — связываем; совпало несколько — ошибка FLANG_AMBIGUOUS_NAME с перечислением кандидатов; не совпало ничего — FLANG_UNKNOWN_NAME.

Правило действует только для локальных имён. Имена функций, типов, вариантов и полей записей — строго точные: они часть контракта, и их склонение сделало бы диагностики непредсказуемыми.

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

Арифметика: плюс, минус, умножить на, делить на, остаток от, процентов от. Сравнения: как в FTS (равен, не равен, больше, меньше, не больше, не меньше).

Логика: не, и притом, или. Приоритеты, от самого слабого к самому крепкому:

или  <  и притом  <  не  <  сравнения  <  плюс минус  <  умножить делить  <  от  .

Значит не а и притом б или ц читается ((не а) и притом б) или ц, а не х равен 1 — это не (х равен 1).

Конъюнкция названа СОСТАВНЫМ словом, а не голым и, и это часть контракта, а не украшение: и разделяет аргументы вызова, а арность вызываемой функции разборщику неизвестна (объявление законно стоит ниже вызова, импортированное имя приезжает без арности). Поэтому:

«Оба верны» от а и б          // ДВА аргумента
«Оба верны» от а и притом б   // ОДИН аргумент, и вся запись — конъюнкция

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

Все три записи разворачиваются в если (а и притом б → если а то б иначе нет), поэтому правый операнд не вычисляется, когда левый всё решил, а операнды обязаны быть признаками — этого требует уже само если.

Эсперантской поверхности у не нет: ne в таблице занято литералом нет.

Цена слова названа прямо: не, или, not, or, aŭ, и притом, and also, kaj ankaŭ, 并且, 或者, 非 больше не бывают именами. В репозитории голых вхождений ни у одного из них не было (проверено токенизацией всех 150 файлов .flang и .fts), но в чужом файле принимает или: число перестанет разбираться. Фраза к числу или беда при этом цела: склейка идёт от длинной к короткой, и четыре слова бьют одно.

Строки как данные

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

Образцы пусто и голова и хвост разбирают не только список, но и СТРОКУ: у неё ровно два случая — пустая либо «первый символ и остаток», третьего нет. Голова строки — строка из одной кодовой точки, хвост — строка из остальных; отдельного типа символа в языке нет. Рекурсия по такому хвосту доказывается структурно, как и по хвосту списка, поэтому посимвольный проход по строке теперь пишется без смены сигнатуры:

тотальная функция «Обратно»
  принимает текст: строка
  возвращает строка
  разбор текст
    случай пусто
      то ""
    случай голова и хвост
      то соединить («Обратно» от хвост) с голова

код символа СТРОКА даёт кодовую точку ПЕРВОГО символа строки числом — единственный мост из строк в числа. Пустая строка прекращает вычисление отказом FLANG_BUILTIN_ARGS; проверить её заранее стоит одного случай пусто.

Форма из двух слов, а не из одного: одинокое «код» — рабочее имя (одно только случай вариант «Не разобрано» с код как код из этой же спецификации), и занять его значило бы сломать чужой код. Счёт голых вхождений — 226 против нуля у пары — под тестом в flang/test/lexer.test.mjs.

Берётся именно первый символ, а не «ровно один»: голова строки, элемент разложить … на символы и символ N в … уже дают ровно один символ, а на всём остальном «первый» — это в точности символ 1 в …. Деление по кодовым точкам, как и везде: эмодзи даёт одно число, а не два суррогата.

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

Что этой формой стало выразимо, и почему она вообще появилась: порядок на строках и хеш строки — оба пишутся НА ЯЗЫКЕ и оба доказываются тотальными. Сравнения больше/меньше по-прежнему допустимы только для чисел, и девятой реализации compare в рантайме не завелось: лексикографический порядок это рекурсия по хвосту строки, и живёт он в библиотеке, где его видно и можно проверить примерами (flang/stdlib/tree.flang, «Строка раньше»). На нём же стоит первый в языке словарь с логарифмическим доступом — дерево поиска с приоритетом по хешу ключа, замер в flang/test/stdlib.test.mjs.

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

Отказ встроенной формы

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

У одной формы такая проверка стоила дороже всего, и ровно у неё отказ теперь возвращается ЗНАЧЕНИЕМ — тем же приёмом, каким описывается ввод-вывод:

разбор (к числу или беда текст)
  случай вариант «Разобрано» с значение как н
    то н
  случай вариант «Не разобрано» с код как код и сообщение как весть
    то 0

к числу или беда отказать не может вовсе. Она возвращает «Разобрано» со значением либо «Не разобрано» с кодом и текстом — ТЕМИ ЖЕ, какими отказала бы к числу: реализация вызывает к числу и переводит её отказ в значение, а не повторяет разбор, поэтому разойтись тексты не могут ни у интерпретатора, ни у восьми целей печати.

Почему именно эта форма и почему набор закрыт. Пригодность строки для к числу проверить заранее можно — но только ПОВТОРИВ саму форму: набор пробельных кодовых точек JS (их 25, среди них U+00A0, U+3000 и U+FEFF) и границу IEEE-754, за которой 1e999 перестаёт быть конечным числом. Сверить повторение с оригиналом в языке нечем: разошлись — узнаешь падением на пользовательских данных. Чего это стоило, видно в flang/stdlib/result.flang: единственный безопасный разбор строки в число, написанный до этой формы, разбирает РОВНО ОДНУ цифру. У остальных встроенных форм проверка ничего не повторяет (случай пусто для списка, сравнение с длина для строки), поэтому вторая такая форма стоила бы восьми рантаймов и не давала бы ничего, что нельзя написать сегодня. Обоснование измерением — в шапке flang/src/builtins.mjs; программа, которая без формы не писалась, — flang/examples/errors/column-total.flang.

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

Долг назван: форму знает лексер на flang (flang/self/lexer.flang), но не знает flang/self/parser.flang. Поэтому ни stdlib, ни examples/leetcode ею пользоваться не вправе — они входят в корпус сверки самоприменения целиком. Улика на запрет — в flang/test/claims.test.mjs.

Коллекции

пусто, голова, хвост, элемент … в …, добавить … к …, отобразить … как …, отфильтровать … где …, свёртка … начиная с … как …, длина.

элемент N в СПИСОК берёт элемент по номеру. Индексация с 1 и включительно — та же, что у символ N в СТРОКЕ, и оборот тот же намеренно: понятие одно («возьми N-й»), значит и способ сказать один. Номер вне списка прекращает вычисление отказом FLANG_BUILTIN_ARGS; проверить его заранее стоит одного сравнения с длина, и потому формы «элемент или беда» нет.

Замены элемента по номеру НЕТ: список читается по номеру, но не правится. Значения flang неизменяемы, а «список с заменённым N-м» пришлось бы собирать целиком — то есть форма выглядела бы дешёвой, а стоила бы линейно. Пока такой формы нет, таблицы динамики и кучи по-прежнему не пишутся; это записано недостачей в flang/examples/leetcode/index.json.

Стоимость встроенных форм — она НЕ одинакова у восьми целей

Язык обещает одинаковые ЗНАЧЕНИЯ и одинаковые тексты отказов. Одинаковой стоимости он не обещает, и делать вид, что обещает, нельзя: у восьми целей разные структуры данных, и одна и та же форма стоит у них разного.

Go в скобках у хвоста стоит по той же причине, что C и Rust: в flang/src/emit/go/flang_runtime.go обе дороги хвоста — BTail встроенной формы и ChainTail цепочки — возвращают List(items[1:]), срез того же массива, а не новый. Копия остаётся у вычислителя, JS, Python, Java и C#: там хвост это slice(1), Arrays.copyOfRange и Items[1..].

Строка про добавить — не про удобство, а про обещание, и вот чем она за него платит. Шаг напечатанного кода — это вход в функцию, виток хвостового цикла и отскок батута; если ОДИН такой шаг стоит O(длины), то предел шагов перестаёт ограничивать работу, и объявленные 5 000 000 шагов кончаются не за секунду. Измерено на точке «Строить скобки» от 42 и 0 и 0 и "" и [] (flang/examples/leetcode/022-generate-parentheses.flang) при пределах 5 000 000 шагов и 10 000 кадров: вычислитель упирается в предел за 950 мс, а напечатанное — за 1,4 с (C), 1,7 с (Java), 3,3 с (Rust), 4,0 с (C#), 4,1 с (Go) и 25,2 с (Python) на обе точки сразу, 8,3 с (Elixir) на одну и 0,8 с (JS) на каждую. До продления за постоянное время та же точка брала в Rust больше 1200 с — от вечного цикла неотличимо, — в C# 273 с, в Java 63,7 с, в JS не отвечала и за 90 с, в Python снималась по сроку на 60 084 мс, в Elixir — по сроку 90 с, и вместе с нею не завершались целиком ни flang/test/emit-rust.test.mjs, ни flang/test/emit-go.test.mjs, ни flang/test/emit-python.test.mjs, ни flang/test/emit-elixir.test.mjs, ни flang/test/emit-js.test.mjs. Значит предел шагов стал сроком у всех восьми целей — долг, который здесь назывался, закрыт, а не спрятан под общим «отказ всегда объявленный».

Как это чинится, видно в семи местах сразу: fl_b_dobavit (flang/src/emit/c/flang_runtime.c), Items::grown (flang/src/emit/rust/flang_runtime.rs), BAppend (flang/src/emit/go/flang_runtime.go), bAppend (flang/src/emit/java/Flang.java), BAppend (flang/src/emit/csharp/Flang.cs), b_append (flang/src/emit/python/flang_runtime.py) и $b_dobavit (flang/src/emit/js.mjs). Приём один: у общего массива есть отметка «сколько ячеек уже занято», и занять ячейку за концом списка вправе единственный список — тот, чей конец совпал с этой отметкой. Отсюда неизменяемость: ячейки внутри списка не пишет никто, а ветвление двух добавить от одного значения даёт две независимых копии. Массив в Java и C# неизменной длины, поэтому длина списка там хранится отдельно от длины массива (Value.count и Value.Count), а обход свёртки и отобразить идёт по массиву ровно нужной длины (Value.elements, Value.Elements) — иначе for-по-элементам прошёл бы по чужим ячейкам за концом. И цена, и неизменяемость проверяются программой: «накопление списка линейно» и «добавить за постоянное время не портит исходный список» в flang/test/emit-rust.test.mjs, flang/test/emit-go.test.mjs, flang/test/emit-java.test.mjs, flang/test/emit-csharp.test.mjs, flang/test/emit-python.test.mjs и flang/test/emit-js.test.mjs.

У JS приём тот же, а носитель другой, и разница принципиальна. Список этой цели — обычный массив JS, и это часть протокола значений: его читают тесты, прогонщик, сверки с интерпретатором и всякий, кто модуль импортировал. Два массива JS с РАЗНОЙ длиной разделить хранилище не могут — длина у массива своя, среза (вида на чужие ячейки) язык не даёт, — то есть всякое добавить, отдающее обычный массив, обязано скопировать n элементов. Это не недоделка, а невозможность, и обойдена она без единой правки протокола: значение остаётся МАССИВОМ по всем наблюдениям, но перестаёт быть массивом по хранению — добавить отдаёт Proxy над общим буфером со своей длиной. Что вид неотличим от массива, проверяет отдельный тест (Array.isArray, length, чтение за концом, JSON.stringify, [...x], Object.keys, deepStrictEqual, getPrototypeOf — двадцать наблюдений). Плата названа там же, где приём (шапка flang/src/emit/js.mjs): чтение элемента у списка, выданного добавить, идёт сквозь ловушку прокси — 341 нс против 7 нс у обычного массива, — класс сложности при этом прежний.

У Python приём тот же, а причина копии была другая, и это стоит знать: append списка Python амортизирован сам по себе, и копия бралась не из-за него, а ради НЕИЗМЕНЯЕМОСТИ — [*items, item] строит новый список ровно затем, чтобы исходный не изменился. Отметкой занятого служит сама длина общего массива, а своя длина списка лежит в поле end значения. Второе место, которого нет ни у Go, ни у Rust: свёртка, отобразить и отфильтровать обходят массив циклом самого Python, а их тело — чужой код и вправе позвать добавить к тому же значению, по которому идёт обход. Поэтому require_list отдаёт растущему списку копию: иначе for … in увидел бы дописанное и ушёл за собственный конец. Это проверяется третьим тестом — «Свёртка по себе».

Elixir починен ДРУГИМ приёмом, и это не прихоть. «Массив с запасом» к списку BEAM не прикладывается вовсе: список односвязный, ячейки не переписывает никто (машина этого не умеет), запаса за концом не бывает. Обменять список на кортеж или :array значило бы сделать дорогим хвост, который сегодня бесплатен, — то есть переложить стоимость, а не убрать её. Поэтому значение-список здесь — пара {:list, начало, конец_наоборот}, логически равная начало ++ Enum.reverse(конец); добавить кладёт одну ячейку в голову конца, а порядок держится тем, что конец хранится наоборот по определению. Это очередь Окасаки, и она ложится на flang точно: язык читает список с ГОЛОВЫ (голова, хвост, образец «голова и хвост»), а добавить пишет в КОНЕЦ — то есть ровно head и tail против snoc. Разбор и инвариант — в @moduledoc файла flang/src/emit/elixir/flang_runtime.ex, раздел 5.

Неизменяемость в Elixir доказывать нечем и не надо: ни одна ячейка не переписывается, и два добавить от одного значения дают две головы поверх общего неизменяемого конца — ветвление здесь даже не уходит на копию, в отличие от C, Go и Rust. Отвечать надо за ПОРЯДОК, и за него отвечает «добавить за постоянное время не портит исходный список: ветвление и хвост» в flang/test/emit-elixir.test.mjs; цену там же держат «накопление списка линейно» (50 000 / 100 000 / 200 000 за 0,9 / 1,2 / 1,8 с против 7,7 / 29,3 / 146,9 с до починки) и «точка сетки, на которой печать зависала». Итог виден на самом прогоне: flang/test/emit-elixir.test.mjs целиком снимался по сроку 1500 с, а теперь доходит до конца за 406 с — 38 из 38, ноль пропусков, 94 программы и 8 796 сверенных входов в главной сверке.

Плата за приём названа: элемент N при N за границей начала идёт по всему списку, а не по N звеньям, и хвост постоянного времени В СРЕДНЕМ, а не всегда (каждый элемент переезжает из конца в начало не более одного раза за жизнь списка). голова, пусто и сам добавить — постоянного времени всегда.

добавить выпадает иначе, и это не мелочь, а цена ПРЕДЕЛА ШАГОВ. Один шаг — вход в функцию, виток хвостового цикла, отскок батута — стоит у семи целей из восьми столько, сколько длинен список: значит maxSteps ограничивает число шагов, но НЕ ограничивает работу. Измерено на flang/examples/leetcode/022-generate-parentheses.flang («Правильные скобки» от 42, глубина 10 000, программа ПОМЕЧЕННАЯ — та же, что печатает настоящая команда) — время до отказа FLANG_RECURSION_LIMIT при одном и том же бюджете шагов:

(миллисекунды; отказ во всех клетках — FLANG_RECURSION_LIMIT.)

У C и у вычислителя время растёт ЛИНЕЙНО с бюджетом: рост бюджета в 16 раз даёт рост времени в 12,8 и 10 раз. Там цена шага ограничена — у C потому, что копии нет вовсе, у вычислителя потому, что его шаг в 130,6 раза мельче и на тот же бюджет он успевает набрать список в 130,6 раза короче. У остальных семи время растёт быстрее квадрата: удвоение бюджета стоит от трёх до шести раз времени. Разница между целями при одном бюджете доходит до 639 раз (C 663 мс против Go 423 436 мс), и это разница НЕ в счётчике — счётчики у всех восьми целей совпадают знак в знак, — а в цене копии одного элемента: у Go значение это структура в 88 байт с тремя указателями внутри, у Java и C# — ссылка в 8 байт, у C копии нет.

**ЭТА ТАБЛИЦА — ЗАМЕР НА ДЕРЕВЕ, ГДЕ добавить ЕЩЁ КОПИРОВАЛ, и читать её надо так.** Долг, ради которого её сняли, к моменту сборки work/svodka2 уже закрыт у семи целей из восьми: продление за постоянное время сделано в C, Go, Rust, Java, C#, Python и JS (work/interpret-append, work/limits-*; приём и его доказательство — строкой добавить … к … в таблице выше и разделом «„добавить“: удлинение списка за постоянное время» в flang/src/emit/c/flang_runtime.c), а у Elixir его заменяет очередь Окасаки. Значит числа выше НЕ описывают сегодняшнее дерево: они описывают, чего стоила копия, и стоят здесь затем, чтобы цена была названа числом, а не словом «медленно». Перемерять их на нынешнем дереве никто не перемерял, и выдавать их за нынешние нельзя.

Что из замера пережило починку и проверяется программой: счётчики шагов у всех восьми целей совпадают знак в знак — это и есть «Восемь целей считают шаги одинаково» той же ветки, — а точки, на которых бюджет шагов у эталона и у цели расходится больше, чем на РАЗМАХ_СЧЁТЧИКОВ, названы поимённо в flang/test/corpus-grid.mjs (УБЕГАЮЩИЕ) и сверяются отказом по пределу.

Обе крайности проверяются программой, а не словами: «стоимость взятия по номеру» в flang/test/emit-c.test.mjs (массив — удвоение длины удваивает РАБОТУ прохода, считанную в шагах, а не во времени) и в flang/test/emit-elixir.test.mjs (там же проверено, что рантайм идёт по звеньям через Enum.at: появится массив — проверка покраснеет, и эту таблицу придётся переписать). Что до хвост, за срез отвечают тесты «хвост списка — срез, а не копия» в emit-c, emit-go и emit-rust: во всех трёх по исходнику рантайма проверено, что на дороге хвоста нет ни обхода, ни копирования, а у C и Rust сверх того замерен аппетит к ПАМЯТИ — наименьший предел ulimit -v, при котором прогонщик ещё отвечает верно, против потолка, растущего линейно по длине списка. У Go такой меры нет намеренно: копия там не стоит памяти вовсе (сборщик забирает её сразу), и квадрат виден только во времени, а время на общей машине шумит вдвое — числа и довод записаны над самим тестом. Что стоимость сделала с доказательством завершения — раздел «Индексный доступ» в flang/src/totality.mjs.

Строку про хвост стережёт flang/test/emit-guard.test.mjs: у каждой из семи целей левого столбца и у вычислителя он держит точный кусок рантайма и класс — срез или копия, — и требует, чтобы скобка называла ровно те цели, что берут срез. До него скобка называла только C и Rust: таблица занижала цель молча, а по ней выбирают цель для горячего пути.

Постоянная шага у Elixir: обвинение со словаря процесса снято

Класс сложности у восьми целей один, а ПОСТОЯННАЯ шага разная, и у Elixir она худшая. Числа сняты в один день на одной машине, чтобы их можно было сравнивать между собой:

Виноватым числился словарь процесса: счётчики шагов и глубины живут там, и Process.get/put зовутся на каждый вход. Обвинение проверено изъятием — тело step, enter и leave заменено на :ok — и снято:

• счётчик стоит 50 нс на шаг (135 против 85 без него);
• самый дешёвый ЧЕСТНЫЙ счётчик (убывающий запас, сырые :erlang.get/put, шесть обращений к словарю на вызов вместо восьми) даёт 121 нс — снять можно 14 нс из 50, не больше;
• даже счётчик, снятый ЦЕЛИКОМ, оставляет 85 нс против 65 у Go, а на документированной точке теряется вовсе: парный опыт (оба варианта считают одновременно, 12 пар) дал дешёвому счётчику 2,6% при 7 победах из 12 — неотличимо от шума.

Дешевле, чем словарь процесса, на BEAM ничего нет: :counters вчетверо дороже (213 нс/шаг), ETS дороже ещё, а неизменяемое протаскивание контекста (как *Ctx в Go) в Elixir невозможно без монады через каждое выражение. Поэтому счётчики оставлены как есть, и это результат замера, а не умолчание.

Разрыв 4,3× живёт в другом месте, и оно названо профилем (:eprof на той же точке): трёхуровневая развязка каждого действия над числами — add/2 → arithmetic/3 → num_add/2, lt/2 → num_order/2 → ordered/2, eq/2 → same_number/2 → equal/2 — 43% профиля против 27% у счётчиков, плюс упаковка каждого числа в {:num, float}. Это отдельный долг, и он записан.

5. AST — контракт между слоями

Парсер выдаёт ровно это; тайпчекер, интерпретатор и кодогенераторы читают только это. Ни один слой не разбирает текст повторно.

{
  "flang": 1,
  "module": "Компилятор",
  "types": [
    { "kind": "record", "name": "Позиция",
      "fields": [{ "name": "цена", "type": { "kind": "number" } }] },
    { "kind": "sum", "name": "Токен",
      "variants": [{ "name": "Слово", "fields": [{ "name": "текст", "type": { "kind": "string" } }] },
                   { "name": "Конец", "fields": [] }] }
  ],
  "functions": [
    { "name": "Длина", "total": true,
      "params": [{ "name": "элементы", "type": { "kind": "list", "of": { "kind": "number" } } }],
      "returns": { "kind": "number" },
      "body": { /* Expr */ },
      "examples": [{ "name": "…", "args": { "элементы": [1, 2] }, "expected": 2 }] }
  ]
}

Expr — размеченное объединение:

{ "kind": "literal",  "value": 1 }
{ "kind": "var",      "name": "элементы" }
{ "kind": "field",    "target": Expr, "field": "цена" }
{ "kind": "let",      "name": "x", "value": Expr, "in": Expr }
{ "kind": "if",       "cond": Expr, "then": Expr, "else": Expr }
{ "kind": "call",     "name": "Длина", "args": [Expr] }
{ "kind": "fnref",    "name": "Удвоить" }                  функция как значение (тег)
{ "kind": "apply",    "fn": Expr, "args": [Expr] }         применение значения-функции
{ "kind": "binary",   "op": "add|sub|mul|div|mod|percent|eq|neq|gt|lt|gte|lte|concat", "left": Expr, "right": Expr }
{ "kind": "construct","variant": "Слово", "fields": { "текст": Expr } }
{ "kind": "record",   "type": "Позиция", "fields": { "цена": Expr } }
{ "kind": "list",     "items": [Expr] }
{ "kind": "match",    "target": Expr,
  "cases": [{ "pattern": Pattern, "body": Expr }] }
{ "kind": "fold",     "over": Expr, "init": Expr, "acc": "сумма", "item": "поз", "body": Expr }
{ "kind": "map",      "over": Expr, "item": "поз", "body": Expr }
{ "kind": "filter",   "over": Expr, "item": "поз", "body": Expr }
{ "kind": "builtin",  "name": "длина|символ|символы|элемент|подстрока|соединить|разделить|содержит|к числу или беда|…", "args": [Expr] }

Pattern := { "kind": "empty" }                                  пустая цепочка: список или строка
         | { "kind": "cons", "head": "г", "tail": "х" }         голова и хвост
         | { "kind": "variant", "name": "Слово", "bind": { "текст": "т" } }
         | { "kind": "literal", "value": … }
         | { "kind": "any", "bind": "имя" }

У каждого узла — необязательное span ({line, column}) для диагностик.

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

{ "kind": "sum", "name": "Возможно", "typeParams": ["А"], "variants": [ … ] }
{ "kind": "record", "name": "Пара", "typeParams": ["Первый", "Второй"], "fields": [ … ] }
{ "name": "Обернуть", "typeParams": ["А"], "params": [ … ], "returns": { … } }
{ "kind": "named", "name": "Возможно", "args": [{ "kind": "number" }] }

Тип функции — обычный узел типа, такой же конструктор с детьми, как список. Записей в AST две, и это временный долг: словесная (функция из числа в число) даёт params/returns, стрелочная (число → строка) — прежние from/to, потому что её узел сверяется побайтово с тем, что строит self/parser.flang. Проверка типов принимает обе и даёт один тип; сводятся они в фазе самоприменения (flang/cat/HOF.md).

{ "kind": "fn", "params": [{ "kind": "number" }], "returns": { "kind": "number" } }
{ "kind": "fn", "from":   { "kind": "number" },   "to":      { "kind": "number" } }

Значение-функция в примерах (дано ф равно функция «Удвоить») записывается тем же JSON, что вариант без полей, — { "variant": "Удвоить", "fields": {} }. Это не совпадение и не экономия: после дефункционализации значение-функция и ЕСТЬ тег, то есть вариант с захваченными полями, а в первой фазе захватывать нечего.

Конкурентность

Контракт модели — flang/conc/SPEC.md. В AST она добавляет три необязательных списка верхнего уровня; появляются они только там, где соответствующие объявления в файле есть, — как morphisms и legacy.

"processes":   [{ "kind": "process", "name": "Счётчик", "state": "Счёт",
                  "initial": "пустой счёт", "accepts": "Команда счёта",
                  "handler": "шаг счёта", "budget": 100000 | null }],
"supervisors": [{ "kind": "supervisor", "name": "Учёт",
                  "watch":  [{ "process": "Счётчик", "strategy": "перезапустить" }],
                  "nested": [{ "supervisor": "Смена", "strategy": "перезапустить" }],
                  "threshold": { "failures": 3, "window": 5000,
                                 "otherwise": "передать выше" } | null }],
"runs":        [{ "kind": "run", "name": "…", "seed": 4172,
                  "inbox":    [{ "process": "Счётчик", "message": … }],
                  "expected": [{ "kind": "state",    "process": "Счётчик", "state": … },
                               { "kind": "strategy", "process": "Счётчик",
                                 "strategy": "перезапустить", "times": 1 }] }]

Программе с процессами парсер приписывает сумму «Действие» — словарь языка, а не объявление пользователя (flang/src/conc.mjs). Поэтому у такой программы в types есть тип, которого нет в исходнике.

Ввод-вывод

Контракт — flang/cat/SPEC.md, раздел «Эффекты и HTTP». Язык остаётся чистым: вариант «Прочитать файл» с путь равным … строит ОПИСАНИЕ действия — значение, — а исполняет его хозяин. В AST это один необязательный список верхнего уровня:

"plans": [{ "kind": "plan", "name": "Сходить по ссылке", "state": "Ход",
            "initial": "Начать", "handler": "Дальше" }]

Монада

Объявление добавляет ещё один необязательный список верхнего уровня; форма в монаде в AST не появляется вовсе — к концу разбора она уже развёрнута в call и match (flang/cat/MONAD.md).

"monads": [{ "kind": "monad", "name": "Возможно", "param": "А",
             "unit": "Обернуть", "join": "Сплющить" }]

Программе, где встретилось имя из словаря ввода-вывода (или объявлен план), парсер приписывает три суммы — «Поручение», «Отклик», «Продолжение» (flang/src/io.mjs), по тому же правилу и по той же причине, что сумму «Действие» выше. Программа, которая ими не пользуется, остаётся побайтово прежней.

Постусловия функции

Свойства утилиты FTS («результат не больше 20 процентов от поля сумма») — это постусловия, и без них раздел 9 невыполним. Поэтому у функции есть:

"postconditions": [
  { "name": "Скидка ограничена", "expr": Expr, "bind": "результат",
    "code": "FTS_UTILITY_PROPERTY", "message": "нарушено свойство …" }
]

bind связывает результат функции внутри expr. code и message едут в AST данными: перевод из FTS обязан давать ровно ту же ошибку, что ядро, иначе совместимость сломается на первом же отказе. Без code — FLANG_PROPERTY.

С появлением слоя доказательства постусловие пишет и обычная функция flang — словом обеспечивает (flang/proof/SPEC.md). Форма в AST та же: ни одного нового поля, ни одной новой проверки в рантайме, ни строки в восьми целях печати. Единственная добавка — необязательное forall с именем параметра, по которому утверждение потом доказывают индукцией; рантайм его не читает вовсе, и без него узел побайтово тот же, что кладёт compat.mjs:

"postconditions": [
  { "name": "высота неотрицательна", "expr": Expr, "bind": "результат",
    "code": "FLANG_PROPERTY", "message": "нарушено свойство …",
    "forall": "стопка" }
]

Предусловия функции

Слово требует (flang/proof/SPEC.md). Поле появляется только у функции с предусловием — программа без него даёт побайтово прежний AST:

"preconditions": [
  { "name": "дно неотрицательно", "expr": Expr,
    "code": "FLANG_PRECONDITION", "message": "не выполнено требование …" }
]

bind здесь нет и быть не может: предусловие говорит о том, что было ДО вызова, а результата до вызова не существует. forall нет по той же причине, по которой он есть у постусловия: квантор называет параметр для индукции, а предусловие индукцией не доказывается — оно снимается у каждого вызова.

Снимает предусловие вызывающий. У каждого вызова внутри программы это обязательство проверки (FLANG_PRECONDITION_CALL при отказе); внутри тела предусловие — допущение обязательства (assumptions), на которое опирается ядро. В рантайме оно считается ровно в одном месте — на границе программы (interpret.mjs, callFunction: --args, значения примеров, всё внешнее), — и ни строкой не печатается ни в одну из восьми целей. Последнее измерено побайтовым сравнением печати с предусловием и без него (flang/test/precondition.test.mjs).

Теорема

Слово теорема несёт две формы, и различает их не слово, а содержимое блока (flang/proof/SPEC.md, «Две формы под одним словом»). Старая — наследие FTS (дано «Объект» имеет …, в данных, по морфизму, следовательно «вывод») — уезжает в legacy узлом ftsLegacy, как уезжала всегда, и её байты не изменились. Новая добавляет необязательный список верхнего уровня:

"theorems": [
  { "kind": "theorem", "name": "высота неотрицательна",
    "claim": { "expr": Expr },
    "vars": [{ "name": "стопка", "type": { "kind": "named", "name": "Стопка" } }],
    "given": [{ "expr": Expr }],
    "induction": { "param": "стопка", "measure": Expr,
                   "cases": [{ "pattern": Pattern, "steps": [Step] }] },
    "steps": [Step],
    "qed": true }
]

Step — шаг доказательства: { "by": { "rule": …, "name": … }, "claim": Expr, "next": true }. Правило (rule) одно из четырёх: property, example, law, hypothesis; у hypothesis имени нет. claim и next необязательны. Обоснование обязательно всегда — шаг без названного факта отвергается разбором, потому что ядро ничего не ищет.

Pattern — тот же образец, что у разбор: исчерпывающность случаев считает типизатор, и считает он её по этим образцам. Своих образцов у индукции нет.

Семантика, которая обязана совпадать у всех слоёв

Интерпретатор, кодогенераторы и мост совместимости обязаны вести себя одинаково. Зафиксировано:

6. Слои реализации

flang/
  src/
    lexer.mjs        текст → токены (отступы значимы: INDENT/DEDENT)
    parser.mjs       токены → AST
    types.mjs        проверка типов, вывод типов, исчерпывающность разбора
    totality.mjs     анализ завершаемости: часть значения и числовая мера;
                     помечает вызовы, чьё доказательство держится на мере
    defunc.mjs       понижение перед печатью: сторож меры и дефункционализация
    interpret.mjs    вычисление AST
    conc.mjs         конкурентность: словарь действий и планировщик эталона
    io.mjs           ввод-вывод: словарь поручений, проверка плана, исполнитель
                     (эффектов не делает и ничего из node: не импортирует)
    host/node.mjs    хозяин ввода-вывода для Node — единственное место с эффектами
    builtins.mjs     строки, списки, числа
    factcheck.mjs    встраиваемый режим: утверждения о данных
    emit/js.mjs      печать в JavaScript
    compat.mjs       мост: FtsDocument → AST flang
    repl.mjs         сессия оболочки: ввод → объявление или значение (терминала не знает)
  bin/flang.mjs      CLI: check | run | test | ast | facts | emit | io | repl
  test/
  SPEC.md

Печать не печатает непроверенного

emit зовёт те же проверки, что check, и отказывается печатать программу, которую check отвергает. Это не удобство команды, а условие, при котором обещания языка вообще что-то значат: тотальная обещает завершение, надзор — разобранный отказ, тип — форму, и все три держатся на том, что программа, которая обещания не держит, НЕ СОБИРАЕТСЯ. Пока проверки жили только в check, обещание кончалось на границе команды: flang/conc/examples/supervision.flang без блока надзор «Цех» давал check с кодом 1 и FLANG_UNCOVERED_FAILURE — и он же давал emit --target go с кодом 0 и 80 155 байтами Go, которые собираются и запускаются.

Ключ --no-check снимает проверку и существует для отладки самой печати, когда смотрят на порождённый код, а не на программу. У остальных команд этот ключ — ошибка вызова: молча проглоченный ключ выглядит верным и не работает.

Граница входа напечатанной программы

У напечатанной программы два входа, и обещания у них разные.

Библиотечный — <префикс>_call, program::call, Flang.call, экспорт модуля — это вычислитель. Он обязан совпадать с интерпретатором значение в значение и ошибку в ошибку, и никаких проверок сверх интерпретатора не делает.

Прогонщик (flang_cli, ключ --cli) — это вход ИЗВНЕ, и у него стоит та же граница, что у flang run --args: значения приезжают JSON-ом, программой не являются и сверяются с объявленными типами параметров ДО вычисления. Отказ — FLANG_TYPE (либо FLANG_UNKNOWN_NAME у значения-функции) с тем же текстом, что даёт flang run.

Это не удобство сообщения, а условие, при котором обещание тотальная вообще что-то значит в напечатанном коде. Доказательство завершения стоит НА ТИПЕ: у нат есть дно 0 и потолок 2^53−1, ниже которого н минус 1 точно меньше н, и сторож убывания в такую функцию не печатается вовсе. Значение вне типа выносит вместе с типом и доказательство — 1e300 минус 1 равно 1e300, цепочка вечна, и поймать её нечем. До этой границы «Факториал» принимает н: нат спокойно считался при н равном −3 и 2.5, а при 1e300 отказывал FLANG_RECURSION_LIMIT, то есть кодом, который отведён ОБЫЧНОЙ функции.

Печатается граница ДАННЫМИ — таблицей объявленных типов рядом с программой, — а сверяет её один и тот же код рантайма, напечатанный байт в байт для всех программ. Строит таблицу тот же слой типов, что отвечает на вопрос «подходит ли значение типу» для --args, facts и io: восемь целей читают один ответ, а не заводят восемь.

Разделение «данные в программе, обход в рантайме» держится и там, где рантайма как отдельного файла нет. У JavaScript модуль обязан оставаться самодостаточным и работать в браузере, поэтому таблица ($PROGRAM.entry) уезжает в модуль — данными, которые браузеру ничего не стоят, — а обход по ней живёт в прогонщике flang_cli.js, соседнем файле, который в браузер не едет вовсе и снимается ключом --no-cli вместе с самой таблицей.

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

7. Коды диагностик

Формат ядра FTS: { code, message, severity, span }.

8. Встраиваемый факт-чекинг

import { checkFacts } from "flang"

const verdict = checkFacts(program, { facts: {...}, claims: ["…"] })
// → { ok: boolean, results: [{ claim, holds, why }] }

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

Факт, подставляемый в аргумент, сверяется с объявленным типом до вычисления, и сверяется тем же checkArguments, каким проверяются --args и значения примеров: одно понимание слов «значение подходит типу» на исходник и на вход. Это не удобство сообщения, а условие первой гарантии. Доказательство завершения тотальной стоит на типе — у нат есть потолок 2^53−1, ниже которого н минус 1 точно меньше н, и сторож убывания в такую функцию не печатается вовсе, — поэтому факт вне типа выносит вместе с типом и доказательство: на {"н": 1e300} доказанная функция упиралась в FLANG_RECURSION_LIMIT. Факт, не подходящий типу, даёт status: "refused" с кодом FLANG_TYPE в объяснении.

Ввод-вывод этому не мешает и мешать не может: checkFacts вычисляет функции, а функция способна лишь ПОСТРОИТЬ поручение — значение вроде «Прочитать файл» с путь равным "…". Исполнять поручения умеет только хозяин (src/host/*), а факт-чекингу хозяин не выдаётся вовсе. Именно ради этого свойства эффекты и описываются, а не выполняются.

9. Совместимость с FTS — обязательна и проверяема

compat.mjs переводит FtsDocument в AST flang: объект → запись, утилита → тотальная функция (начальное значение + правила как последовательность if, свойства как постусловия, примеры как examples). Тест обязан прогнать все модели репозитория через оба движка и потребовать совпадения результатов, включая коды ошибок при нарушении свойств.

10. Известные ограничения

Имя варианта не должно совпадать с ключевым словом

Лексер решает, что перед ним, до того как становится известен тип, поэтому вариант, названный ключевым словом языка, в образце не разбирается:

Обходится переименованием варианта либо явной формой случай вариант «Имя», которой пользуется stdlib. Долг здесь оплачен наполовину: сообщение FLANG_PARSE теперь перечисляет разрешённые образцы целиком, и явная форма вариант «Имя» в нём названа — то есть по тексту отказа программу уже можно починить, не читая этот раздел. Чего сообщение по-прежнему не говорит, так это настоящей причины: что имя варианта совпало со словом языка. Это остаток долга, и он не в тексте, а в разборе — чтобы назвать причину, парсеру надо знать, что слово в позиции образца было ИМЕНЕМ варианта, а на этом месте он этого ещё не знает.

Ограничение обнаружено при связывании модулей и не связано с ним: тот же код в одном файле ведёт себя так же.