Синтаксис по факту: модули, функции, выражения, образцы

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

Файл целиком

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

модуль «Синтаксис»

объект «Позиция»
  цена является числом
  количество является числом

тотальная функция «Стоимость позиции»
  принимает цена: число, количество: число
  возвращает число
  пример «Три по десять»
    дано цена равно 10
    дано количество равно 3
    ожидается 30
  пусть поз равно запись «Позиция» с цена равным цена и количество равным количество
  поз.цена умножить на поз.количество

тотальная функция «Деление и остаток»
  принимает а: число, б: число
  возвращает число
  пример «Семь и два»
    дано а равно 7
    дано б равно 2
    ожидается 4.5
  (а делить на б) плюс (а остаток от б)

тотальная функция «Скидка»
  принимает сумма: число
  возвращает число
  пример «Десять процентов от тысячи»
    дано сумма равно 1000
    ожидается 100
  10 процентов от сумма

$ flang test синтаксис.flang
синтаксис.flang: примеров 3, прошло 3, не прошло 0

Заголовок модуля

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

модуль «Проба импорта»
  использует «Lists»

тотальная функция «Сумма пробы»
  принимает элементы: список числа
  возвращает число
  «Сумма» от элементы
  пример «Четыре числа»
    дано элементы равно [1, 2, 3, 40]
    ожидается результат равен 46

Так написан docs/examples/import-check.flang в репозитории языка (там модуль называется «Import check»). «Lists» — модуль библиотеки, которая ставится вместе с компилятором в share/flang/stdlib; компилятор ищет модуль в каталоге файла, выше по каталогам, в FLANG_MODULE_DIR и затем в этой библиотеке. Форма с путём — использует «Lists» из "../stdlib/lists.flang" — тоже разбирается, но путь отсчитывается от файла и годится только внутри дерева репозитория языка.

Есть и вторая форма — взять из модуля не всё, а перечисленное:

модуль «Печать в C»
  использует «Печать JSON» только «Значение», «Скаляр», «Поле значения», «Замена», «Заменить всё», «Замены», «Экранировать», «Печать строки», «Печать массива»

Это первая строка ввоза в flang/self/emit-c.flang, то есть строка изнутри самого компилятора: модуль «Печать JSON» лежит в его дереве (flang/core/), а не в библиотеке. Установленный двоичный его не находит — FLANG_IMPORT_NOT_FOUND … не найден модуль «Печать JSON»; песочница на /flang/ везёт модули ядра с собой и строку принимает. Имена перечисляются через запятую, и всё, что в список не попало, из модуля не приходит вовсе — обращение к нему даёт обычный FLANG_UNKNOWN_NAME. У этой формы в 0.7.29 есть граница: функции, на которые опираются взятые, тоже надо перечислить (digitable-lol/flang#447) — разбор с настоящим отказом в главе «Стандартная библиотека».

Ключевое слово экспортирует перечисляет, что модуль отдаёт наружу; так написаны docs/examples/package/discount.flang и docs/examples/reference/ru/report-only.flang. Без него виден весь модуль. Подробнее про связывание — глава «Стандартная библиотека».

Комментарии — // до конца строки и /* … */. Лексер их выбрасывает, поэтому в библиотеке их нет вовсе: что функция обещает, записано обещаниями (обеспечивает) и именами примеров, и это проверяет компилятор.

Объявление типов

Записи объявляются словом объект — прямо как в FTS:

объект «Группа»
  ключ является строкой
  слова является список строки

Это из docs/examples/leetcode/049-group-anagrams.flang. Суммы типов — словом тип, с перечислением вариантов:

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

Это начало optional.flang из библиотеки; от «А» делает тип параметрическим (раздел про полиморфизм ниже). Вариант либо несёт поля (содержит имя: тип, через запятую), либо не несёт ничего. Имена вариантов обязаны быть уникальны в пределах модуля.

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

Функции

тотальная функция «Первый элемент или запасное»
  принимает элементы: список числа, запасное: число
  возвращает число
  пример «Список не пуст»
    дано элементы равно [4, 5]
    дано запасное равно 0
    ожидается 4
  пример «Пустой список даёт запасное»
    дано элементы равно пустой список
    дано запасное равно 42
    ожидается 42
  «Значение или запасное» от («Первый элемент» от элементы) и запасное

Это упрощённая функция из модуля «Optional» библиотеки: там она объявлена от «А» для списка любого типа и несёт ещё три обещания обеспечивает. Разбираем по строкам:

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

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

Форма ожидается 4 — короткая. Полная — ожидается результат равен 46 — тоже принимается: так написан пример в import-check.flang.

Типы в сигнатурах

Скаляры: число, строка, признак, ничто. Формы склонений тоже читаются — лексер знает числа, числом, числу, строки, строкой, строку, признака, признаком. Отсюда естественное список числа вместо список число.

Списки: список числа, список строки, список «Группа», и даже вложенно — список список строки (из решения про анаграммы).

Именованные типы пишутся в ёлочках: возвращает «Возможно» от числа.

Числовых типов несколько, и выбор типа меняет то, что компилятор докажет: число — обычное IEEE-754, неотрицательное — целое из [0, 2⁵³−1], целое, сотых и тысячных (деньги в минорных единицах), точное целое и точное дробное без округления. Подробно — в главе «Система типов».

Унаследованные от FTS имена деньги и дата лексер знает; тайпчекер приравнивает Деньги к числу, а Дата — к строке.

Выражения

Связывание

пусть удвоенное равно «Умножить значение» от («Первый элемент» от элементы) и 2
«Значение или запасное» от удвоенное и запасное

пусть не требует слова в: тело идёт следующей строкой того же уровня.

Ветвление

Блочная форма:

если акк начинается с "!"
  то акк
  иначе
    если "([{" содержит буква
      то соединить акк с буква
      иначе …

И однострочная — из того же файла (docs/examples/leetcode/020-valid-parentheses.flang):

если закрывающая равен "]" то "[" иначе "{"

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

модуль «Связки»

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

Вызов

«Длина» от хвоста
«Значение или запасное» от удвоенное и запасное
«Символы с позиции» от текст и (позиция плюс 1)

Имя функции — всегда в кавычках, аргументы соединяются словом и. Функция без аргументов зовётся одним именем: («Сорок два») плюс 1.

Арифметика и сравнения

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

FLANG_PARSE в файле остаток.flang, строка 6, столбец 3: не разобрана конструкция: неожиданное 'остаток от' — это слово занято языком, именем оно быть не может: напишите имя в ёлочках («остаток от») или переименуйте; а если слово попало в форму лишним — уберите его

Правильно — а остаток от б.

Сравнения унаследованы от FTS: равен, не равен, больше, меньше, не больше, не меньше. Формы равна, равно, равным — то же самое.

Порядок сравнения (больше/меньше) работает только для чисел. На строках получите отказ ещё на check:

FLANG_TYPE в файле строки.flang, строка 6, столбец 3: левый операнд сравнения «gt» имеет тип строка: сравнения порядка допустимы только для чисел
FLANG_TYPE в файле строки.flang, строка 6, столбец 12: правый операнд сравнения «gt» имеет тип строка: сравнения порядка допустимы только для чисел

Записи и варианты

Конструирование записи и вариантa устроено одинаково — словом с и перечислением полей через и:

запись «Группа» с ключ равным ключ и слова равным (добавить слово к группа.слова)
вариант «Есть число» с значение равным голова

Вариант без полей пишется просто: вариант «Нет числа».

Доступ к полю — через точку: группа.ключ, диагностика.код. Единственная точка в языке, где точка вообще используется.

Записи нельзя записать литералом. Очевидная попытка:

$ … дано поз равно {цена: 10}
FLANG_PARSE в файле запись.flang, строка 10, столбец 20: не разобрана конструкция: неожиданное '{'

Записи строятся конструктором запись «…» с …, и в примерах тоже: дано поз равно запись «Позиция» с цена равным 10 и количество равным 3.

Сопоставление с образцом

разбор элементов
  случай пусто
    то 0
  случай голова и хвост
    то 1 плюс «Длина» от хвоста

Образцы, которые встречаются в репозитории:

Обратите внимание на голова и хвост: имена не выбираются, это фиксированная форма из таблицы ключевых слов (голова и хвост:headTail в flang/self/lexer.flang).

Форма случай вариант «Имя» с поле как имя — явная, с ключевым словом вариант. Именно ей пользуется стандартная библиотека, и не из вкуса. В docs/flang/SPEC.md описано известное ограничение: лексер решает, что перед ним, до того как становится известен тип, поэтому вариант, названный ключевым словом, в образце не разбирается.

Первая строка проверена: тип с вариантами Да и Нет разбирается, а образец нет:

FLANG_TYPE: образец-литерал имеет тип признак, а разбирается «Ответ»
FLANG_TYPE: образец-литерал имеет тип признак, а разбирается «Ответ»
FLANG_MATCH_NOT_EXHAUSTIVE в файле ответ.flang, строка 10, столбец 3: разбор «Ответ» не покрывает «Да», «Нет»

Спецификация тут же признаёт долг: сообщение не называет настоящую причину — что имя варианта совпало со словом языка, — потому что на этом месте разбор ещё не знает, что слово было именем варианта. В 0.7.29 у двух строк FLANG_TYPE нет даже места в файле. С вариантами в ёлочках (вариант «Да», случай вариант «Да») тот же файл проходит check без единой диагностики.

Встроенные формы над коллекциями

map/filter/fold принимают не функцию, а тело. Функция при этом тоже значение (раздел ниже), но формы остаются основным способом обхода: тело не требует объявлять функцию ради одного выражения:

свёртка элементы начиная с [первый] как акк и эл → добавить эл к акк
отобразить группы как группа → группа.слова
отфильтровать элементы где эл → эл не равен значение

Стрелка → отделяет тело от заголовка в однострочной записи; в многострочной тело просто уходит на следующий уровень отступа:

свёртка группы начиная с нет как акк и группа
  если акк равен да то да иначе группа.ключ равен ключ

Также есть добавить … к … (дописывает в конец), приписать … к … (ставит в начало) и длина. «Приписать в начало» в lists.flang сводится к приписать первый к элементы.

Строки

длина текст
символ 2 в текст
подстрока акк с 1 по ((длина акк) минус 1)
соединить акк с буква
разделить текст по буква
"([{" содержит буква
акк начинается с "!"
к строке (…)
к числу (…)

Две семантические детали зафиксированы в спецификации и повторяются всеми слоями: индексация с 1, включительно с обоих концов, и длина в кодовых точках, а не в единицах UTF-16. Второе проверяется так:

тотальная функция «Длина текста»
  принимает текст: строка
  возвращает число
  пример «Эмодзи считается одним»
    дано текст равно "мир 🌍"
    ожидается 5
  длина текст

Пример проходит. Обоснование в спецификации прямое: «иначе кириллица и эмодзи считаются неверно».

символ 2 в текст проходит check и возвращает "и" от "мир" — это тоже проверено примером.

Литералы

42, -3, 0.5, "строка", да, нет, ничто, [1, 2, 3], пустой список.

Экспоненциальная запись читается: пример с телом 1e3 и ожиданием 1000 проходит flang test.

Категорная поверхность: стрелка, композиция, цепочка, единица

Замысел объяснён в контракте docs/ct/spec.md репозитория языка: семантика языка категорная, и у неё есть слова. Тип — это объект, функция — морфизм, вложенный вызов — композиция, запись — произведение, сумма типов — копроизведение, ничто — терминальный объект. Записываются эти конструкции словами, без ∘ и прочих знаков, которых нет на обычной клавиатуре.

модуль «Продажи»

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

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

объект «Счёт»
  итог является числом

морфизм «отгрузить» из «Заказ» в «Отгрузка»
морфизм «выставить» из «Отгрузка» в «Счёт»

морфизм «оформить» это «выставить» после «отгрузить»

единица «Заказ»

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

flang check на этом файле отвечает не «замечаний нет», а «проверено не до конца», кодом 2:

$ flang check продажи.flang
законы категории НЕ СЧИТАЛИСЬ: стрелки объявлены, а категории нет — равенство, через которое закон только и выразим, объявляет категория
модуль «Продажи»: функций 0, из них с доказанным завершением 0; типов 3
законы этих объявлений НЕ СЧИТАЛИСЬ — стрелки без категории: устройство сверено, а закон не посчитан ни на одном значении, и ответ «замечаний нет» читался бы как «закон проверен», а это неправда
продажи.flang: проверено НЕ ДО КОНЦА — разбор, типы, завершаемость, ядро и примеры прошли

Разберём по словам.

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

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

Стыковка проверяется компилятором — и это доказательство

Вот ради чего стоит читать этот раздел, даже если теоркат вам безразличен. В контракте композиция стоит на доказанной стороне вместе с завершением и типами: «Б» после «А» не соберётся, если кодомен «А» не равен домену «Б»; цепочка не соберётся, если рвётся в середине.

Это утверждение обо всех входах, без решателя и без примеров. Проверяется оно ровно так, как обещано, — переставим множители местами:

$ flang check продажи.flang
…
FLANG_COMPOSE_MISMATCH в файле продажи.flang, строка 15, столбец 1: морфизм «оформить»: «отгрузить» после «выставить» не собирается — «выставить» ведёт в «Счёт», а «отгрузить» начинается в «Заказ»
…
продажи.flang: не проверено — замечаний 1

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

FLANG_COMPOSE_MISMATCH в файле цепочка.flang, строка 20, столбец 1: морфизм «провести · шаг 1»: «оплатить» после «отгрузить» не собирается — «отгрузить» ведёт в «Отгрузка», а «оплатить» начинается в «Счёт»
FLANG_COMPOSE_MISMATCH в файле цепочка.flang, строка 20, столбец 1: морфизм «провести»: «выставить» после «провести · шаг 1» не собирается — «провести · шаг 1» ведёт в «Счёт», а «выставить» начинается в «Отгрузка»

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

Функтор, бифунктор, изоморфизм, моноид, монада

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

Функтор. Отображение категории в категорию: объектам объекты, стрелкам стрелки.

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

Строк сохраняет композицию и сохраняет единицы в поверхности нет, и это решение: «отображение, не сохраняющее композицию, функтором не является, и разрешение на проверку закона продавало бы имя вместо содержания». Устройство функтора сверяется по объявленным именам, а закон — квадрат «образ стрелки после образа объекта» — считается на значениях. Для этого у образа объекта должна быть функция перевода (объект «Заказ» отображается в «Платёж» даёт «Платёж по заказу»), а у стрелок — свои даёт. Тогда отчёт говорит так (файл docs/examples/reference/ru/orders-and-payments.flang):

функтор «Заказ в платёж»: сетка 2 значений, квадратов 1, нарушений 0 — ПОСЧИТАНО НА СЕТКЕ, не доказано

Без даёт у объектов — «функтор «Заказ в счёт»: НЕ СЧИТАЛСЯ — ни у одного объекта нет «даёт»: переводить нечем, сравнивать нечего», и код 2. Тем же кодом 2 и без отдельной диагностики в 0.7.29 проходит и функтор, у которого выброшена строка объект «Отгрузка» отображается в «Акт», хотя стрелка «отгрузить» в «Отгрузка» и ведёт; бифунктор в таком случае отвечает FLANG_BIFUNCTOR_OBJECT_MISSING.

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

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

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

Граница «доказано / посчитано на сетке» проходит внутри одной конструкции

Возьмём моноид:

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

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

Теперь главное. В одной этой конструкции граница честности проходит посередине.

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

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

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

$ flang check вычитание.flang
моноид «Вычитание чисел»: сетка 3 значений, троек 2, нарушений 3 — ПОСЧИТАНО НА СЕТКЕ, не доказано
…
FLANG_MONOID_IDENTITY в файле вычитание.flang, строка 29, столбец 1: моноид «Вычитание чисел»: единица не нейтральна слева: операция от единицы и 7 дала -7
FLANG_MONOID_ASSOC в файле вычитание.flang, строка 29, столбец 1: моноид «Вычитание чисел»: операция не ассоциативна: на 0, 0, 7 слева вышло -7, справа 7
FLANG_GROUP_INVERSE в файле вычитание.flang, строка 29, столбец 1: моноид «Вычитание чисел»: обращение не даёт единицу: на 7 вышло -14 слева и 14 справа
…

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

Есть и третий ответ. У моноида над точными числами ядро доказывает сочетательность и единицу само: в том же docs/examples/reference/ru/monoids.flang отчёт печатает «моноид «Сумма точных»: сочетательность и единица доказаны ядром», а про «Сумму чисел» над число — «ядром НЕ доказаны».

Изоморфизм считается на сетке, если у стрелок есть тела.

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

Когда у «выписать» и «по накладной» есть даёт, отчёт говорит «изоморфизм «Платёж и квитанция»: сетка 2 значений, нарушений 0 — ПОСЧИТАНО НА СЕТКЕ, не доказано» (orders-and-payments.flang). Когда тел нет, — «изоморфизм «Заказ и накладная»: НЕ СЧИТАЛСЯ — у стрелки нет «даёт»: вычислять нечего», код 2. И здесь граница 0.7.29, которую стоит знать: без тел стрелок изоморфизм с перепутанным направлением (обратный морфизм «выписать») и изоморфизм без единица «Накладная» проходят с тем же кодом 2 и без отдельной диагностики (digitable-lol/flang#451).

Монада есть: монада «Возможно» от «А» со строками возврат «Обернуть» и соединение «Сплющить», а запись в монаде «Возможно» со строками пусть … и возврат … — это do-нотация словами: компилятор разворачивает её в вызовы объявленных возврат и соединение. Законы монады считаются на сетке, как законы моноида (docs/examples/reference/ru/discount.flang):

монада «Возможно»: сетка 2 значений, троек 32, нарушений 0 — ПОСЧИТАНО НА СЕТКЕ, не доказано

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

Три разных ответа на вопрос «а это точно так?» внутри одной поверхности одного языка — и код возврата их различает: 0, 2 («проверено не до конца») или отказ. Тот, кто читает только слово «доказуемый» на титульной странице, все три прочитает одинаково.

И одно уточнение, без которого весь раздел читается неверно. Морфизм не заменяет функцию и не отменяет её. Это отдельное объявление. Контракт (docs/ct/spec.md) объясняет: сделать функцию частным случаем морфизма было бы красивее, но пришлось бы переписать 1711 объявлений в репозитории. Тотальная функция — это доказанное завершение вычисления; морфизм — стрелка между объектами, которую функция может считать (даёт). Разные вещи, и обе остаются.

Функция как значение — и ни одного нового слова

Функция — значение, и поверхность не стоила языку ни единого нового слова.

тотальная функция «Удвоить»
  принимает х: число
  возвращает число
  х плюс х

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

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

flang check отвечает «функций 3, из них с доказанным завершением 3» — все три тотальны, и это главное. flang test даёт «примеров 1, прошло 1».

Три формы, и все на занятых словах:

Почему ни одного нового слова — проверяется счётом по репозиторию языка (дерево метки v0.7.29):

$ grep -rowE --include=*.flang "«функция»" . | wc -l
3285
$ grep -rowE --include=*.flang "«из»|«в»|«и»|«от»" . | wc -l
1911

Больше пяти тысяч вхождений — и ни одно не пострадало, потому что имя в ёлочках ключевым словом не становится никогда. Причём 3220 из 3285 вхождений «функция» — в самом компиляторе, написанном на flang, то есть в тех самых файлах, которые обязаны продолжать собираться. Новое слово сломало бы ровно их.

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

Чем за это заплачено

функция «Обернуть» при полиморфной «Обернуть» даёт FLANG_TYPE_PARAM, а не значение: у полиморфной функции типов столько, сколько подстановок, а у значения он один:

FLANG_TYPE_PARAM в файле обернуть.flang, строка 29, столбец 18: функция «Обернуть» объявлена от 1 параметра и значением стать не может: у значения тип один, а …

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

Функции-значения ничего не стоят выведенному коду: перед выводом компилятор одним проходом превращает их в обычные вызовы, и граф вызовов остаётся конечным (подробно — в главе «Система типов»). Этому проходу нужна вся программа целиком. В библиотеке на функциях-значениях построен модуль «Higher order» (higher-order.flang): свёртка, отображение, фильтр, сортировка и композиция принимают функцию аргументом.

Параметрический полиморфизм

Тоже без единого нового слова: от и и были в таблице с первого дня.

модуль «Полиморфизм»

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

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

тотальная функция «Двойное»
  принимает значение: число
  возвращает «Возможно» от («Возможно» от числа)
  пример «Вложение того же типа»
    дано значение равно 5
    ожидается вариант «Есть» с значение равным (вариант «Есть» с значение равным 5)
  вариант «Есть» с значение равным («Обернуть» от значение)

Одно объявление обслуживает обе подстановки, а «Возможно» от («Возможно» от числа) — это тот же тип, а не второй; flang test даёт «примеров 3, прошло 3». от после имени объявления вводит параметры, от после имени типа в позиции типа подставляет аргументы — читается одинаково, «Возможно от А».

Одна настоящая двусмысленность есть, и она разведена заглядыванием: и — и разделитель аргументов типа, и разделитель полей варианта. Правило: и + имя + двоеточие начинает поле, всё остальное — аргумент; за типом двоеточие не идёт никогда.

Библиотека пользуется полиморфизмом сама: «Длина», «Обратить» и «Приписать в начало» в «Lists» объявлены от «А», «Возможно» в «Optional» и «Результат» в «Result» — параметрические суммы.

Запрос к среде и план: как чистый язык читает файл

Здесь стоит остановиться, потому что это самое неожиданное решение в языке.

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

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

Видов запроса в 0.7.29 двадцать семь (список — функция «Варианты поручения» в flang/self/parser.flang): файлы («Прочитать файл», «Записать файл», чтение и запись октетов, «Удалить файл», «Перечислить каталог», «Завести временный каталог»), сеть («Запросить», соединения, датаграммы), процессы («Запустить процесс» и два его варианта), экран («Показать», «Ждать событие», «Размер экрана»), а ещё «Текущее время», «Случайное число», «Случайные октеты», «Прочитать переменную среды» и «Прочитать доводы». Набор закрыт и задан в компиляторе: программа не может завести свой вид запроса, потому что исполнять его было бы некому.

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

Само объявление — три строки и одно новое слово, план:

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

состояние, начинает с и обрабатывает уже были ключевыми — теми же тремя словами объявляется процесс, и контракт настаивает, что это не экономия слов, а утверждение: план и процесс устроены одинаково.

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

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

  пример «Первым делом читается файл с адресом»
    дано ход равно вариант «Читаем адрес»
    дано отклик равно вариант «Пока ничего»
    ожидается вариант «Сделать» с поручение равным (вариант «Прочитать файл» с путь равным "адрес.txt") и потом равным (вариант «Идём в сеть»)

Ни файла, ни сокета при этом нет. Отсюда два свойства, которые обычно теряются вместе с чистотой, и оба проверены запуском на docs/examples/io/link-report.flang — программе, которая читает файл, ходит в сеть и пишет отчёт:

$ flang check docs/examples/io/link-report.flang
модуль «Link report»: функций 7, из них с доказанным завершением 7; типов 4
docs/examples/io/link-report.flang: проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет
$ flang test docs/examples/io/link-report.flang
docs/examples/io/link-report.flang: примеров 10, прошло 10, не прошло 0

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

Вывод кода при этом работает как у любой программы: C из flang emit … --target c --out lr-c собирается make под -std=c99 -Wall -Wextra -Werror -pedantic и отвечает тем же описанием запроса, что вычислитель внутри flang:

$ echo '{"fn":"Дальше","args":[{"v":"Читаем адрес","f":[]},{"v":"Пока ничего","f":[]}]}' | ./flang_cli
{"ok":true,"value":{"v":"Сделать","f":[["поручение",{"v":"Прочитать файл","f":[["путь",{"s":"адрес.txt"}]]}],
                                        ["потом",{"v":"Идём в сеть","f":[]}]]}}

Причина простая: план — это две обычные функции и три обычные суммы, и при выводе кода они не отличаются от остального. Исполняет план сам двоичный: flang io <файл> — это и есть среда исполнения, которая читает файлы, ходит в сеть и зовёт «Дальше» с откликом; ключ --in-dir запрещает пути за пределы каталога файла, --seed N делает «Случайное число» повторимым, а --no-net, --no-write и соседние ключи отнимают права по одному. Выведенная на C программа исполняет план сама: ./flang_cli --plan <имя>.

Почему это не монада — и что мы за это отдали

Контракт называет разницу одной фразой:

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

То есть монада, у которой продолжение записано данными, а не функцией. Отдано за это три вещи, и все видны в коде: связывание не является выражением (каждая точка ожидания — отдельный объявленный вариант, в link-report.flang их четыре); тип результата запроса не отслеживается («Отклик» — одна закрытая сумма на все виды запроса); законов монады у плана нет.

Граница честности, названная в самом контракте

Сокет — у среды исполнения, не у языка. На flang пишется то, что запрос описывает и что с ответом делать. Разбор HTTP-сообщений и клиент TLS 1.3 при этом написаны на flang (модули «Requests and responses» и «TLS client» в библиотеке), и flang io ходит по HTTPS без curl.

Процесс и надзор: и то, и другое выводится в настоящую BEAM

Та же дисциплина, тот же вид объявления:

процесс «Работник»
  состояние «Счёт»
  начинает с «нулевой счёт»
  принимает «Задача»
  обрабатывает «шаг работника»

надзор «Цех»
  процесс «Работник» стратегия «перезапустить»
  порог отказов 2 за 5000 миллисекунд иначе «остановить»

Обработчик — обычная чистая функция: получает состояние и сообщение, возвращает новое состояние и список описанных действий. Действия не выполняются, а описываются — по той же причине, что и запросы плана.

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

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

прогон «упал и вернулся ровно к началу»
  семя 1
  дано «Работник» принимает (вариант «прибавить» с «сколько» равным 4)
  дано «Работник» принимает (вариант «подавиться» с «почему» равным "испортился вход")
  ожидается «Работник» стратегия «перезапустить» 1 раз
  ожидается «Работник» равен (запись «Счёт» с «всего» равным 0)
  ожидается «Учётчик» равен (запись «Записи» с «строки» равным ["4"])

flang test flang/concurrency/examples/supervision.flang даёт «примеров 5, прошло 5»: два примера обработчиков и три прогона. flang check на том же файле отвечает кодом 2: имена, типы сообщений и обработчики сверены, а достижимость отказа внутри тотальной функции двоичный не судит и говорит об этом отдельной строкой. flang emit … --target elixir выводит процессы и надзор в модули Elixir. Перезапуск здесь возвращает состояние к начальному значению, и дочищать после отказа нечего — состояние неизменяемо, наполовину применённой мутации не бывает, потому что мутаций нет вовсе.

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

Чего в синтаксисе нет

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

Список сверен с flang 0.7.29: функции как значения, обобщённые типы, вызов функции без аргументов, логические связки и монада в языке есть. Список того, чего нет, стареет быстрее всего остального в тексте про язык — сверяйте его с версией, которая у вас стоит (flang --version).

Дальше — глава «Система типов», про то, как всё это проверяется.