flang 0.4.7 — монада, отказ значением, полиморфизм в репозитории

Версию 0.4.6 гейт публикации остановил — печать в Go давала два объявления с одним именем. Дефект починен, и здесь он вместе со всем, что сделано за день.

Монада

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

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

Форма разворачивается внутри разбора: продолжение не строится значением, отображение печатается на месте разбором по вариантам. Поэтому печать во все восемь целей, анализ завершаемости и оба слоя самоприменения получают её даром, а правок в self/parser.flang и self/types.flang — ноль.

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

Отказ стал значением

к числу или беда возвращает «Разобрано» со значением либо «Не разобрано» с кодом и текстом:

сумма 22 по 3 ячейкам; пропущено 2, первая — "abc":
  «к числу»: строка "abc" не является числом

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

Полиморфизм в самом репозитории

self/parser.flang и self/types.flang понимают параметры типа и функции-значения, поэтому библиотека схлопнута: «Возможно» от «А», «Результат» от «Значение» и «Беда». Библиотека высшего порядка переехала из теста в flang/stdlib/higher-order.flang — одна свёртка с функцией-значением даёт сумму, произведение и максимум вместо трёх функций с одинаковым телом.

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

«тотальная» перестала обещать больше, чем доказано

Числа в языке — IEEE-754 double, и выше 2⁵³ вычитание единицы ничего не меняет. Функция, доказанная числовой мерой, на таком входе не завершалась, хотя компилятор объявлял её тотальной.

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

$ flang run … --args '{"н": 18014398509481988}'
{"error":"тотальная функция «До нуля»: мера не убыла — аргумент 1 вызова
«До нуля» не стал меньше параметра «н». … Отказ здесь честнее зацикливания"}

Цена названа: +52% в собранном C на холостых витках, ровно +10 шагов вычислителя на виток.

Печать в Go

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

Проверено

На машине со всеми восемью тулчейнами: 1942 теста, 1942 прошли, пропусков ноль. Неподвижная точка самоприменения сошлась: семь напечатанных файлов C совпали побайтово у эталона, flang₁ и flang₂. Архив собран с нуля флагами формулы и запущен.

Установка

brew install digitable-lol/tap/flang

flang 0.4.6 — бинарник разговаривает с человеком

Что изменилось для того, кто ставит язык

До этой версии brew install flang давал бинарник, который на --help молчал и отвечал нулём: он понимал только JSON на stdin. Теперь:

$ flang --version
flang 0.4.6
$ flang check проба.flang
модуль «Проба»: функций 1, из них с доказанным завершением 1; типов 0
проба.flang: проверено — разбор, типы, завершаемость; замечаний нет     код: 0
$ flang check битая.flang
FLANG_TYPE в файле битая.flang, строка 5, столбец 3: функция «Плохая»
  объявлена как число, а тело даёт строка                              код: 1
$ flang repl
объявлено: тотальная функция «Куб» — завершение доказано
343
$ man flang

Оболочка вычисляет не интерпретатором — его в бинарнике нет, — а печатью сессии в C, сборкой системным cc против libkompilyator_flang.a и запуском. Нет cc — оболочка не выключается, а работает проверяющей и говорит об этом при запуске.

Старый режим «JSON на входе, JSON на выходе» цел байт-в-байт: без аргументов или по явному --json.

Что изменилось в языке

• Самоприменение понимает полиморфизм и функции первого класса. Библиотека высшего порядка переехала из теста в flang/stdlib/higher-order.flang (36 функций, все тотальные): одна свёртка, принимающая функцию-значение, даёт сумму, произведение и максимум вместо трёх функций с одинаковым телом. Монада перестала быть невыразимой.
• Связывание переносит категорные объявления через границу файла. Нарушенный закон функтора в импортированном модуле раньше давал valid: true и код возврата 0.
• Три новых модуля библиотеки: логика, словарь строка → строка, множество строк. Законы логики проверены исчерпывающим перебором: у признака два значения, поэтому «все 8 троек» — это все тройки, какие бывают.
• Конкурентность проверяется перебором тысячи семян, а не одним чередованием; модель измерена с названными условиями.
• Пример настоящей службы REST на 200 строк: разбор строки запроса, проверка полей, маршрутизация, коды ответов. Все функции тотальны, устойчивость проверена четырнадцатью нарочно кривыми запросами.

Известный дефект этой версии

Печать в Go ломается на программах с функциями-значениями. Проход дефункционализации даёт конструктору тега то же имя, что у самой функции, и Go отвергает файл: Chyotnoe redeclared in this block. Задет flang/stdlib/higher-order.flang — первая программа репозитория, которую этот проход переписывает.

Бинарника из этого архива дефект НЕ касается: C собирается -std=c99 -Wall -Wextra -Werror -pedantic без предупреждений, check и repl работают — проверено на архиве, распакованном и собранном с нуля.

Дефект прошёл мимо локальных прогонов потому, что тест печати в Go молча пропускается там, где Go не установлен. Чинится в 0.4.7 вместе с проверкой, которая ловит столкновение имён без тулчейна — на любой машине.

Проверено

Неподвижная точка самоприменения сошлась: семь напечатанных файлов C совпали побайтово у эталона, flang₁ и flang₂. Набор — 1638 тестов, 0 отказов на машине без тулчейнов Go, .NET и Elixir (53 пропуска).

Установка

brew install digitable-lol/tap/flang

flang 0.4.5 — ввод-вывод, процессы на BEAM, оболочка в бинарнике

brew install digitable-lol/tap/flang
flang repl

Оболочки в прошлом релизе не было, хотя мы говорили обратное. flang_repl.c лёг в репозиторий уже после тега v0.4.4, поэтому поставивший через brew получал компилятор без неё. Здесь она есть — проверено на архиве из чистой распаковки: собирается без Node, отвечает диагностикой с местом ввода.

Язык вышел наружу

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

Прочитать файл «адрес.txt» → "http://…/страница"
Запросить GET → код 200, тело "привет из сети"
Записать файл «отчёт.txt» → записано 22 байта

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

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

Процессы поехали на настоящей BEAM

Процесс печатается GenServer-ом, надзор — деревом супервизоров OTP. Вытеснение по редукциям, отдельная куча у каждого процесса, распределённость — настоящие, а не свои.

Сверять значения нельзя: семантика есть любое чередование. Поэтому эталон гоняется на 1000 семян, из итогов собирается множество допустимых исходов, и каждый запуск на BEAM обязан в него попасть. 275 запусков, 250 журналов, 178 различных чередований — сошлось.

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

Лексер самоприменения стал тотальным целиком

84 функции из 84, долгов не осталось ни одного — было 54 из 88. Печать в C 223 из 326, парсер 188 из 374.

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

Теоркат и типы

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

Языковой сервер flang-lsp. Справочник конструкций на портале — 41 карточка на все 112 форм языка.

Проверено: 1651 тест, ноль падений, неподвижная точка сошлась — семь файлов побайтово у эталона, flang₁ и flang₂.

flang 0.4.4 — языковой сервер, законы функтора, конкурентность

Установка без Node — в архиве компилятор, уже напечатанный в C99:

brew install digitable-lol/tap/flang

Полный инструментарий — восемь целей печати, интерпретатор, оболочка flang repl, языковой сервер flang-lsp — через npm, ему Node нужен:

npm install -g @digitable-lol/fts

Языковой сервер

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

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

Функтор перестал быть словом без гарантии

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

Законы не включаются по желанию: отображение, не сохраняющее композицию, функтором не является.

Конкурентность, шаг 1

Процесс — объявление, обработчик — чистая функция, действия описываются, а не выполняются. Обработчик атомарен в пределах своего процесса; процессы идут параллельно.

Чередование воспроизводится по семени, поэтому гонка предъявляется примером:

прогон «на семени 4172 первым успевает правый»
  семя 4172
  ожидается «Сборщик» равен (запись «Метки» с «строки» равным ["П1", "П2", "Л1", "Л2"])

Trojan Source закрыт целиком

Двунаправленные управляющие Unicode больше не уезжают в целевой код сырыми ни в одной из трёх поверхностей печати: восемь бэкендов flang, восемь ftsc и JIT виртуальной машины. До починки rustc и elixirc отказывались собирать такой вывод, а javac собирал молча — ради этого молчания атаку и придумали.

Тесты перебирают реестр целей, а не список в себе, и проверены на регресс подложенной девятой целью.

Ещё

Встроенная форма разложить … на символы — посимвольный проход стал доказуемым. Оболочка flang repl. Решения Rosetta Code. REST-пример examples/library-api и правила раскладки проекта. Описание языка docs/overview.ru.md.

flang 0.4.2 — две ветки сведены, память линейна, шаги считаются

Установка без Node — в архиве компилятор, уже напечатанный в C99:

brew install digitable-lol/tap/flang

Полный инструментарий (восемь целей печати, интерпретатор, языковой сервер) — npm install -g @digitable-lol/fts, ему Node нужен.

Что изменилось

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

Лимит шагов в напечатанном C. Программа с незавершающейся рекурсией теперь останавливается с FLANG_RECURSION_LIMIT — тем же кодом и тем же текстом, что у интерпретатора, — а не висит. Сам компилятор печатается с пределом, который ему нужен: 40 · 10⁶ шагов против 10⁶ по умолчанию.

Проверка релиза стала настоящей. Раньше она спрашивала собранный бинарник о трёхстрочном модуле. Теперь даёт ему разобрать self/parser.flang — 372 функции, 35 тысяч токенов. Дефект, который трёхстрочный модуль не показывал, был бы виден сразу.

Теоркат, шаг 1. Морфизм как стрелка между объектами, композиция словом после, цепочка в порядке чтения, единица. Стыковка композиции проверяется компилятором и относится к доказанному.

Описание языка целиком — docs/overview.ru.md, с честной границей между «доказано» и «проверено на конечной сетке».

Предыдущий v0.4.1 работоспособен; замены не требует.

flang 0.4.1 — компилятор, который ставится без Node

Компилятор flang, напечатанный в C99. Ставится там, где есть cc — Node не нужен.

Установка

tar -xzf flang-0.4.1-c.tar.gz && cd flang-0.4.1-c
make
./flang_cli

Никаких зависимостей, кроме libc и libm. Собирается cc -std=c99 -Wall -Wextra -Werror -pedantic без единого предупреждения.

Почему архив с C, а не бинарник

Компилятор языка написан на самом языке и печатается в C, поэтому релиз содержит уже напечатанный исходник. Так поступают самоприменяющиеся языки: Go долго возил сгенерированный C, Nim возит до сих пор. Проблема начальной загрузки остаётся только у того, кто развивает сам язык, — ему нужен Node, чтобы получить первый бинарник из исходников на flang.

Архив собран node scripts/build-release-c.mjs: тот же скрипт печатает C, собирает его в окружении без Node в PATH и запускает результат. Битый архив не уедет.

Переносимость

Рантайм не содержит архитектурно-зависимых конструкций. Проверено кросс-сборкой под RISC-V (riscv64-linux-gnu-gcc) и запуском под QEMU: те же значения, включая 0.1 плюс 0.2 = 0.30000000000000004, NaN и Infinity, до последнего знака.

Что в этой версии

• Самоприменение замкнулось: компилятор печатает сам себя, и второй проход даёт побайтово тот же C — все шесть файлов.
• Восемь целей печати: C, Go, Rust, Python, Java, C#, Elixir, JavaScript.
• Ядро FTS переписано на flang: 300 функций, все тотальные.
• Разбор суждений в основной проверке: недостижимые свойства, дыры в покрытии и перекрытия правил находятся с указанием строки и интервала контрпримера.
• Первый шаг теоркат-поверхности: стрелка, композиция, цепочка, единица — стыковка доказывается компилятором.

Через npm

npm install -g @digitable-lol/fts

Этот путь даёт весь инструментарий, включая семь остальных бэкендов, интерпретатор и языковой сервер, — и требует Node.