Справочник конструкций

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

Другие страницы отвечают на другие вопросы:

Словарь: слова flang и привычные термины

Prover — часть компилятора, которая доказывает обеспечивает для всех возможных входов, а не только для ваших примеров. В выводе компилятора он называется «ядро», а строка обеспечивает — «постусловие».

Как читать примеры

Большая часть примеров ниже — целые программы, и каждая проходит команду:

flang check файл.flang

Где это не так, сказано в тексте. Куски без строки модуль показывают одну форму, а не программу. Примеры категорий, монад и процессов завершаются кодом 2, а не 0: разбор, типы, завершаемость и примеры проходят, но правила самих этих объявлений двоичный компилятор не проверяет и пишет об этом в выводе.

Блоки без подсветки — то, что компилятор печатает: ошибки и отчёты. Слово в начале строки (FLANG_TYPE, FLANG_PROOF_STEP) — код ошибки; каждый код объяснён в Справочнике отказов.

У каждого ключевого слова есть русское и английское написание (всего написаний четыре, они называются поверхностями). Это одно и то же слово, а не перевод: оба дают одно дерево разбора, и в одном файле можно писать любым. Понятий — 159; полный список с четырьмя написаниями — Словарь языка, как устроены написания — Четыре поверхности записи.

Имена — модулей, функций, типов, примеров, постусловий — пишутся в ёлочках «…» при любом написании ключевых слов.

Что набирается несколькими способами

Стрелка набирается →, -> или => — это одно и то же. Ниже везде стоит →; на клавиатуре её искать не надо.

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

Модуль и импорт

модуль «Report»
  экспортирует «Итог»
  использует «Lists»

тотальная функция «Итог»
  принимает элементы: список числа
  возвращает число
  пример «повторы не считаются дважды»
    дано элементы равно [3, 1, 3, 2, 1]
    ожидается 6
  «Сумма» от («Уникальные» от элементы)

Без нужды только не пишите. Оно не просто прячет имена: чего нет в списке, того нет в программе вовсе. А импортированные функции вызывают другие функции своего модуля — в теле и в постусловиях. Замените третью строку примера выше на использует «Lists» только «Сумма», «Уникальные» — и проверка не проходит:

$ flang check docs/examples/reference/ru/report-only.flang
модуль «Report»: функций 3, из них с доказанным завершением 0; типов 0; файлов вместе с импортами 2
без доказанного завершения: «Сумма» «Уникальные» «Итог»
место указано строкой и столбцом, но без файла: вместе с импортами проверено файлов 2, а диагностика компилятора имени файла не несёт
FLANG_UNKNOWN_NAME, строка 460, столбец 47: неизвестная функция «Шаг суммы»
FLANG_UNKNOWN_NAME, строка 453, столбец 74: неизвестная функция «Все не меньше»
FLANG_UNKNOWN_NAME, строка 453, столбец 130: неизвестная функция «Максимум»
FLANG_UNKNOWN_NAME, строка 564, столбец 59: неизвестная функция «Шаг уникальных»
FLANG_NOT_TOTAL, строка 460, столбец 47: тотальная функция «Сумма» вызывает неизвестную функцию «Шаг суммы»: завершение доказать нельзя
FLANG_NOT_TOTAL, строка 564, столбец 59: тотальная функция «Уникальные» вызывает неизвестную функцию «Шаг уникальных»: завершение доказать нельзя
docs/examples/reference/ru/report-only.flang: не проверено — замечаний 6
$ echo $?
1

Номера строк указывают в flang/stdlib/lists.flang. Строка 453 — постусловие самой «Сумма» («сумма неотрицательных не меньше наибольшего из них»), оно вызывает «Все не меньше» и «Максимум»; строка 460 — тело «Сумма», оно вызывает «Шаг суммы»; строка 564 — тело «Уникальные». только все их выбросило. Тот же файл с обычным использует «Lists» проходит с кодом 0.

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

модуль «Counting core»

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

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

модуль «Counting»
  использует «Counting core» только «Удвоить»

тотальная функция «Четыре»
  возвращает число
  пример «два удвоено»
    ожидается 4
  «Удвоить» от 2

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

Ищут в трёх местах и в таком порядке:

1. каталог самого файла, который пишет использует;
2. каждый каталог выше него — пока в каталоге лежит хоть один файл .flang;
3. библиотека, поставленная вместе с компилятором.

В подкаталоги поиск не заходит. Для модуля в другом месте перечислите его каталог в FLANG_MODULE_DIR (каталоги через двоеточие) или назовите файл прямо: использует «Модуль» из "путь". Путь считается от импортирующего файла и годится и для пакета: из "имя.flang-package".

Если найдено два модуля с одним именем, проверка не проходит и называет оба пути; молча компилятор не выбирает.

Ограничение: имена модулей не переводятся. Стандартный модуль списков называется «Lists» (первая строка flang/stdlib/lists.flang), и файл с русскими ключевыми словами импортирует его под этим же именем. использует «Списки» даёт FLANG_IMPORT_NOT_FOUND.

Слова раздела на всех четырёх поверхностях, из таблицы лексера:

Функция

Части идут в закреплённом порядке. Тело — последним, одним выражением.

модуль «Signature»

тотальная функция «Доля»
  принимает часть: неотрицательное, всего: неотрицательное
  возвращает число
  требует «делитель положителен» всего больше 0
  для всех часть обеспечивает «доля неотрицательна» результат не меньше 0
  пример «половина»
    дано часть равно 1
    дано всего равно 2
    ожидается 0.5
  часть делить на всего

Вызов — «Имя» от аргумент и аргумент. Слово и разделяет аргументы; логическое И пишется и притом, чтобы они не путались.

Ограничения:

• в сгенерированном коде требует проверяется только на границе программы, там, куда значение приходит снаружи. Внутренние вызовы за проверку не платят;
• у обеспечивает обязательно имя: под этим именем результат виден в отчёте flang check --proof, по нему на постусловие ссылается теорема;
• примеры прогоняются при каждой проверке. Упавший пример — ошибка FLANG_EXAMPLE, и код для программы не генерируется.

Слова раздела на всех четырёх поверхностях, из таблицы лексера:

Тотальность и мера

Завершение функции с тотальная компилятор доказывает одним из пяти способов. Первые три ничего не стоят при работе, последние два добавляют проверку в сгенерированный код. Какой способ сработал у какой функции — в отчёте flang check --proof; счёт по всему репозиторию — на странице Зачем и как.

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

модуль «Measure»

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

Ограничение: мера должна быть целой и неотрицательной, это проверяется на каждом вызове. «НОД» от целых работает всегда; «НОД» от двух дробных останавливается с FLANG_MEASURE: цепочка дробных остатков может убывать вечно.

Тело: четыре формы

разбор, свёртка, если и пусть. Циклов нет.

разбор — pattern matching по типу с вариантами

модуль «Tree»

тип «Дерево»
  вариант Лист
  вариант Узел содержит значение: число, левое: «Дерево», правое: «Дерево»

тотальная функция «Узлов»
  принимает дерево: «Дерево»
  возвращает число
  пример «в листе узлов нет»
    дано дерево равно вариант Лист
    ожидается 0
  разбор дерева
    случай Лист
      то 0
    случай вариант Узел с левое как л и правое как п
      то 1 плюс («Узлов» от л) плюс («Узлов» от п)

Тип с вариантами — это enum с данными (tagged union). Образцы: случай Имя — вариант без полей; случай вариант Имя с поле как имя — вариант с полями, привязанными к именам; случай пусто и случай голова и хвост — список или строка; случай любое — всё остальное.

Что проверяет компилятор: обработан каждый вариант; пропущенный вариант — ошибка FLANG_MATCH_NOT_EXHAUSTIVE. Рекурсия на части значения завершается доказанно без меры. Индукция в теореме работает только по этой форме.

свёртка — reduce: один проход по списку

модуль «Fold»

тотальная функция «Произведение»
  принимает элементы: список числа
  возвращает число
  пример «три множителя»
    дано элементы равно [2, 3, 4]
    ожидается 24
  свёртка элементы начиная с 1 как акк и эл → акк умножить на эл

Завершение даром: список конечен, проход один.

Ограничение: тип накопителя не уточняется. неотрицательное в накопителе останется число.

если — if как выражение

модуль «Branching»

тотальная функция «Сумма до»
  принимает н: неотрицательное
  возвращает число
  пример «до нуля — ноль»
    дано н равно 0
    ожидается 0
  пример «до трёх — шесть»
    дано н равно 3
    ожидается 6
  если н не больше 0
    то 0
    иначе н плюс («Сумма до» от (н минус 1))

Ограничения: обе ветви обязательны, условие должно быть признаком (boolean). Условие сужает числовые границы в своей ветви, но prover его как факт не использует. Это постусловие не доказывается: check --proof пишет «объявлено, не доказано» и завершается кодом 3:

модуль «If as an expression»

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

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

пусть — константа

модуль «Binding»

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

тотальная функция «Стоимость позиции»
  принимает позиция: «Позиция»
  возвращает число
  пример «две штуки по триста»
    дано позиция равно запись «Позиция» с цена равным 300 и количество равным 2
    ожидается 660
  пусть чистое равно позиция.цена умножить на позиция.количество
  пусть налог равно 10 процентов от чистое
  чистое плюс налог

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

Типы

Скалярные

Вложение: неотрицательное ≤ целое ≤ число и неотрицательное ≤ вес ≤ число. Значение втекает в объявленную позицию, обратно — нет.

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

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

Какой числовой тип брать

модуль «Exact types»

тотальная функция «Копейки заказа»
  принимает цена: сотых, штук: неотрицательное
  возвращает число
  пример «три по 19.99»
    дано цена равно 1999
    дано штук равно 3
    ожидается 5997
  цена умножить на штук

тотальная функция «Доля»
  принимает часть: неотрицательное, всего: неотрицательное
  возвращает число
  требует «делитель положителен» всего больше 0
  пример «половина»
    дано часть равно 1
    дано всего равно 2
    ожидается 0.5
  часть делить на всего

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

$ flang check docs/examples/reference/ru/natural-sum.flang
модуль «Sum of naturals»: функций 1, из них с доказанным завершением 1; типов 0
FLANG_TYPE в файле docs/examples/reference/ru/natural-sum.flang, строка 6, столбец 5: функция «Сумма неотрицательное» объявлена как неотрицательное, а тело даёт число
docs/examples/reference/ru/natural-sum.flang: не проверено — замечаний 1
$ echo $?
1

Точные типы ставьте на параметры и поля записей: там их используют prover и проверка завершения. Возврат объявляйте число, если тело считает арифметикой.

Точные числа без потолка: точное целое и точное дробное

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

Литерал точного целого — список разрядов младшим вперёд по основанию 4 194 304 (2²²): [7] — семь, [0, 1] — 4 194 304, [] — ноль. Дробь — пара таких списков, числитель над знаменателем: [[1], [3]] — одна треть, [[], [1]] — ноль. Десятичной записи у литерала нет.

модуль «Exact numbers»

примечание "Разряды точного целого идут младшим вперёд по основанию 4194304"

тотальная функция «Сумма»
  принимает а: точное целое, б: точное целое
  возвращает точное целое
  пример «перенос через разряд»
    дано а равно [4194303]
    дано б равно [1]
    ожидается [0, 1]
  пример «два в пятьдесят третьей плюс один»
    дано а равно [0, 0, 512]
    дано б равно [1]
    ожидается [1, 0, 512]
  а плюс б

тотальная функция «Сумма дробей»
  принимает а: точное дробное, б: точное дробное
  возвращает точное дробное
  пример «одна десятая и одна пятая»
    дано а равно [[1], [10]]
    дано б равно [[1], [5]]
    ожидается [[3], [10]]
  а плюс б

тотальная функция «Ноль дробью»
  возвращает точное дробное
  [[], [1]]

тотальная функция «Доля»
  принимает часть: точное дробное, всего: точное дробное
  возвращает точное дробное
  требует «всего не ноль» всего больше «Ноль дробью»
  пример «треть на две пятых»
    дано часть равно [[1], [3]]
    дано всего равно [[2], [5]]
    ожидается [[5], [6]]
  часть делить на всего

тотальная функция «Целых в дроби»
  принимает дробь: точное дробное
  возвращает точное целое
  пример «семь вторых — три целых»
    дано дробь равно [[7], [2]]
    ожидается [3]
  пример «треть — ноль целых»
    дано дробь равно [[1], [3]]
    ожидается []
  целая часть дробь

Ограничения:

• точные числа не смешиваются с число: а плюс 1 над точное целое — отказ FLANG_TYPE: «add»: точное целое и число не смешиваются, нужен названный перевод;
• значений ниже нуля нет: [1] минус [2] при работе — FLANG_PROPERTY, молчаливого нуля не бывает; деление на нулевую дробь — тоже FLANG_PROPERTY;
• дробь в литерале обязана быть сокращена: [[2], [4]] — отказ проверки типов «дробь не сокращена»;
• литерал становится точным числом только там, где тип задан: в параметре, в возвращает, в аргументе. В сравнении всего больше [[], [1]] он остаётся списком, поэтому ноль в примере выше вынесен в функцию «Ноль дробью».

Устройство целиком — в Спецификации языка, раздел «Типы».

Список

список Тип — однородный. Литерал — [1, 2, 3], пустой — пустой список. Ковариантен: список неотрицательное годится там, где ждут список числа.

список из — то же самое другими словами: список из числа в позиции типа и список из 1 и 2 и 3 в позиции значения.

Запись (структура)

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

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

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

Тип с вариантами (enum)

тип «Ответ»
  вариант Успех содержит значение: число
  вариант Отказ содержит причина: строка

Строится вариант Успех с значение равным 30, разбирается формой разбор.

Так пишут Optional и Result: «нашлось» и «не нашлось» — разные варианты, и вызывающий обязан сделать по ним разбор. ничто (null) для этого не берут.

Всё вместе, одной программой:

модуль «Types»

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

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

тип «Ответ»
  вариант Успех содержит значение: число
  вариант Отказ содержит причина: строка

тотальная функция «Проверить цену»
  принимает позиция: «Позиция»
  возвращает «Ответ»
  пример «цена есть»
    дано позиция равно запись «Позиция» с название равным "болт" и цена равным 30
    ожидается вариант Успех с значение равным 30
  пример «ноль — не цена»
    дано позиция равно запись «Позиция» с название равным "гайка" и цена равным 0
    ожидается вариант Отказ с причина равным "цена не положительна"
  если позиция.цена больше 0
    то вариант Успех с значение равным позиция.цена
    иначе вариант Отказ с причина равным "цена не положительна"

Поле, объявленное иногда является, в примерах писать не обязательно.

Псевдоним и generic-тип

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

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

Параметры типа (generics) вводятся словом от и им же подставляются. При вызове они выводятся из значений; записать их явно негде.

Ограничение: у слова это английского написания нет; в файле с английскими ключевыми словами оно пишется русским словом.

Тип функции

функция из числа и строки в признак — словесная запись; число → число — стрелочная. Обе дают один тип.

Ограничение: с английскими ключевыми словами словесная запись function from number to number не разбирается — to number занято встроенной формой «к числу». Пишите стрелкой: number → number.

Выражения

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

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

Ограничение: не меньше по-английски пишется is at least, не больше — is at most. Обороты по аналогии не работают; написание берите из словаря.

Перенос внутри круглых скобок

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

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

Ошибка внутри такого выражения называет свою настоящую строку. Внутри […] перевод строки по-прежнему разделяет элементы списка, как запятая, поэтому длинный элемент списка берут в круглые скобки и переносят внутри них. Слова из нескольких слов — и притом, не меньше — на две строки не делят.

Строка в несколько строк

Литерал "…" переживает перевод строки: значение продолжается на следующей строке, и перевод строки входит в него как есть. Одинарные кавычки '…' — тот же литерал. Эти две записи дают одну и ту же строку:

модуль «Two spellings»

тотальная функция «Через перевод строки»
  возвращает строка
  пример «то же, что с \n»
    ожидается "первая\nвторая"
  "первая
вторая"

тотальная функция «Одинарными кавычками»
  возвращает строка
  пример «те же кавычки, только другие»
    ожидается "текст"
  'текст'

Граница: отступ строк продолжения входит в значение буква в букву. Строка "первая⏎ вторая" равна "первая\n вторая", поэтому текст внутри тела функции пришлось бы начинать с первого столбца. Для текста в несколько строк внутри отступа есть блок текста.

Блок текста """

Три двойные кавычки открывают блок; текст начинается со следующей строки; общий отступ снимается:

тотальная функция «Справка»
  возвращает строка
  """
  Команды:
    .помощь   эта справка
    .выход    закончить
  """

Значение — "Команды:\n .помощь эта справка\n .выход закончить\n". Токен тот же, что у литерала с \n: блок — запись, а не новый вид строки.

тотальная функция «Без перевода строки в конце»
  возвращает строка
  пример «закрывающие кавычки на последней строке текста»
    ожидается "первая\nвторая"
  """
  первая
  вторая"""

тотальная функция «С отступом внутри»
  возвращает строка
  пример «закрывающие кавычки левее текста задают общий отступ»
    ожидается "  первая\n"
  """
    первая
  """

Границы: незакрытый блок — отказ FLANG_LEX на месте открывающих кавычек; негодный \uXXXX внутри блока — отказ на строке и в столбце самой обратной черты. Подстановки значений в блоке нет. Решение и полный разбор случаев — ADR-0052.

Слова раздела на всех четырёх поверхностях, из таблицы лексера:

Встроенные формы над списками и строками

модуль «Built-in forms»

тотальная функция «Длинные слова»
  принимает текст: строка
  возвращает список строки
  пример «короткое слово выброшено»
    дано текст равно "раз дважды трижды"
    ожидается ["дважды", "трижды"]
  отфильтровать (разделить текст по " ") где слово → (длина слово) больше 3

тотальная функция «Длины слов»
  принимает слова: список строки
  возвращает список числа
  пример «три слова»
    дано слова равно ["раз", "дважды", "трижды"]
    ожидается [3, 6, 6]
  отобразить слова как слово → длина слово

У каждой формы свои закреплённые предлоги:

модуль «Strings»

тотальная функция «Второе слово»
  принимает текст: строка
  возвращает строка
  пример «два слова»
    дано текст равно "раз дважды"
    ожидается "дважды"
  элемент 2 в (разделить текст по " ")

тотальная функция «Первые три»
  принимает текст: строка
  возвращает строка
  пример «отрезано с головы»
    дано текст равно "абвгде"
    ожидается "абв"
  подстрока текст с 1 по 3

тотальная функция «Склеено»
  принимает части: список строки
  возвращает строка
  пример «через запятую»
    дано части равно ["а", "б"]
    ожидается "а,б"
  соединить части по ","

тотальная функция «Первая буква»
  принимает текст: строка
  возвращает строка
  пример «голова строки»
    дано текст равно "абв"
    ожидается "а"
  символ 1 в текст

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

Посимвольно, отпечаток и логика

модуль «Character by character»

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

тотальная функция «Отпечаток»
  принимает текст: строка
  возвращает строка
  пример «отпечаток пустой строки»
    дано текст равно ""
    ожидается "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855"
  хеш256 текст

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

тотальная функция «Слова»
  принимает текст: строка
  возвращает список из строки
  пример «два слова»
    дано текст равно "раз два"
    ожидается ["раз", "два"]
  разделить текст по " "


тотальная функция «Ничего»
  принимает текст: строка
  возвращает ничто
  пример «значение пустоты»
    дано текст равно "а"
    ожидается ничто
  ничто

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

модуль «Field by word»

объект «Точка»
  «х»: число
  «у»: число

тотальная функция «Абсцисса»
  принимает точка: «Точка»
  возвращает число
  пример «первая координата»
    дано точка равно запись «Точка» с «х» равным 3 и «у» равным 4
    ожидается 3
  поле «х» у точка

тотальная функция «Ордината»
  принимает точка: «Точка»
  возвращает число
  пример «вторая координата»
    дано точка равно запись «Точка» с «х» равным 3 и «у» равным 4
    ожидается 4
  поле «у» из точка

Слова раздела на всех четырёх поверхностях, из таблицы лексера:

Функции как значения

модуль «Function as a value»

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

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

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

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

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

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

Ограничение: применить можно только функцию, которую программа где-то берёт формой функция «Имя». Функция-значение, пришедшая снаружи и нигде в программе не взятая, отвергается с FLANG_APPLY. Раздельной компиляции нет: функции-значения разрешаются по всей программе сразу.

Контракты и доказательства

Эти слова говорят о функции больше, чем её тип. Каждое проверяется по-своему.

требует — предусловие

требует «имя» условие — что должно быть верно, чтобы вызов был допустим.

модуль «Precondition»

тотальная функция «Доля»
  принимает часть: неотрицательное, всего: неотрицательное
  возвращает число
  требует «делитель положителен» всего больше 0
  пример «половина»
    дано часть равно 1
    дано всего равно 2
    ожидается 0.5
  часть делить на всего

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

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

обеспечивает — постусловие

для всех п обеспечивает «имя» условие — что верно для результат на любом входе. результат в условии — возвращённое значение.

модуль «Postcondition»

тотальная функция «Удвоить все»
  принимает элементы: список числа
  возвращает список числа
  для всех элементы обеспечивает «длина сохраняется» (длина результат) равен (длина элементы)
  пример «три элемента»
    дано элементы равно [1, 2, 3]
    ожидается [2, 4, 6]
  отобразить элементы как э → э умножить на 2

Prover сначала пробует условие доказать. Доказал — в сгенерированном коде проверки нет. Не доказал — условие проверяется на каждом возврате, и нарушение останавливает вычисление. Что доказано, а что нет, показывает flang check --proof.

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

для всех … из …: — свойство каждого элемента списка

Чтобы сказать что-то про каждый элемент списка, квантор пишут прямо в постусловии. Его тело отделяется двоеточием.

модуль «For all after a filter»

тотальная функция «Только положительные»
  принимает элементы: список числа
  возвращает список числа
  обеспечивает «все положительны» для всех п из результат: п больше 0
  пример «Смесь»
    дано элементы равно [3, 0, 5]
    ожидается [3, 5]
  отфильтровать элементы где э → э больше 0

Prover доказывает такое постусловие по ФОРМЕ списка, который строит тело, а не прогоном. Он принимает четыре формы: пустой список; отфильтровать Л где х → У, когда У и есть доказываемое свойство; добавить Х к Л и приписать Х к Л, когда свойство верно и про Х, и про Л; если У то А иначе Б, когда верно в обеих ветвях. Выписанный поэлементно список, отобразить (map) и вызов другой функции не принимаются — правила для них у prover'а нет.

Тело после двоеточия — снова условие, поэтому кванторы вкладываются:

  обеспечивает «каждый с каждым положителен» для всех х из результат: для всех м из результат: м больше 0

Для «существует» значение называете вы сами: есть такой м, а именно х, что …. Без а именно prover ищет его среди подтермов цели (не больше восьми) и по значениям не ищет; негодное названное значение он отказывает кодом FLANG_PROOF_STEP, а не молчит. Квантор стоит и внутри условия — под и притом и под если … то … иначе.

Ограничение: первое двоеточие верхнего уровня заканчивает квантор, всё правее — его тело. Квантор внутри условия и переменная в для всех н обеспечивает … — разные вещи, и prover их не путает.

теорема

Теорему пишут, когда prover не доказал постусловие сам.

модуль «Theorem»

тотальная функция «Сумма до»
  принимает н: неотрицательное
  возвращает число
  для всех н обеспечивает «сумма до неотрицательна» результат не меньше 0
  пример «шагов не осталось»
    дано н равно 0
    ожидается 0
  если н не больше 0
    то 0
    иначе н плюс («Сумма до» от (н минус 1))

теорема «сумма до неотрицательна»
  дано н: неотрицательное
  утверждаем результат не меньше 0
  индукция по н убывает н
    случай 0
      то по примеру «шагов не осталось»
    случай любое
      то по предположению
  следовательно доказано

Как понять, что теорема нужна, и как её довести до «доказано», — на странице Доказательство руками.

Индукция не обязательна; короткая теорема — одно обоснование:

модуль «Property»

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

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

теорема «через удвоение длина та же»
  дано элементы: список числа
  утверждаем (длина результат) равен (длина элементы)
  по свойству «удвоение длины не меняет»
  следовательно доказано

Ограничение: часто теорема не нужна — сначала напишите постусловие и посмотрите, докажет ли его prover сам. Индукция работает только по разбор по типу с вариантами и по убывающему числу.

утверждение — свойство не при функции

Свойство можно записать само по себе, без функции.

модуль «Free statements»

утверждение «длина пустого списка нулевая»
  утверждаем (длина пустой список) равен 0

утверждение «ноль нейтрален при сложении»
  для всех н: неотрицательное таких что н больше 0
  утверждаем (н плюс 0) равен н

Prover проверяет его так же, как постусловие, и оно попадает в flang check --proof --json. Строка для всех имя: тип таких что условие задаёт переменные и допущение. Допущение здесь важно: неотрицательное при работе принимает минус ноль, и без н больше 0 второе свойство ложно.

Доказать свойство можно и теоремой с тем же именем, написанной рядом.

Индукция по своему объявленному типу

индукция по работает не только для встроенных типов, но и для ваших типов с вариантами: принцип индукции берётся из объявления типа.

модуль «Own natural»

тип «Нат»
  вариант «Ноль»
  вариант «Следующий» содержит пред: «Нат»

тотальная функция «К числу»
  принимает н: «Нат»
  возвращает число
  разбор н
    случай вариант «Ноль»
      то 0
    случай вариант «Следующий» с пред как п
      то («К числу» от п) плюс 1

утверждение «шаг растит счёт на один»
  для всех н: «Нат»
  утверждаем («К числу» от (вариант «Следующий» с пред равным н)) равно ((«К числу» от н) плюс 1)

теорема «шаг растит счёт на один»
  дано н: «Нат»
  утверждаем («К числу» от (вариант «Следующий» с пред равным н)) равно ((«К числу» от н) плюс 1)
  индукция по н
    случай вариант «Следующий» с пред как п
      то по предположению
  следовательно доказано

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

Обоснования шага

У каждого шага должно быть обоснование, иначе он не разберётся. Обоснований четыре.

по свойству

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

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

$ flang check docs/examples/reference/refused/circular-property.flang
модуль «Circle»: функций 1, из них с доказанным завершением 1; типов 0
FLANG_PROOF_STEP в файле docs/examples/reference/refused/circular-property.flang, строка 12, столбец 3: шаг 1, теорема «длина сохраняется»: «по свойству «длина сохраняется»» ссылается на то самое постусловие, которое сейчас доказывается — это круг. Часть значения обосновывает «по предположению», а не ссылка на саму цель. к этому месту не известно ничего, кроме гипотез «дано»
docs/examples/reference/refused/circular-property.flang: не проверено — замечаний 1
$ echo $?
1

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

по предположению

Берёт допущение. Их два вида: гипотеза индукции (то же свойство для меньшей части значения) и предусловие функции (строка требует). Теорема «Сумма до» выше опирается на гипотезу индукции.

Если нет ни того, ни другого, проверка не проходит и называет, чего не хватает:

$ flang check docs/examples/reference/refused/missing-hypothesis.flang
модуль «Without a hypothesis»: функций 1, из них с доказанным завершением 1; типов 0
FLANG_PROOF_INDUCTION_STEP в файле docs/examples/reference/refused/missing-hypothesis.flang, строка 12, столбец 3: шаг 1, теорема «половина неотрицательна»: «по предположению» стоит вне индукции, а допущений у этой цели нет ни одного: ни посылки индукции (её даёт `индукция по`), ни предусловия функции (его даёт `требует`). Предполагать не о чем. к этому месту не известно ничего, кроме гипотез «дано»
docs/examples/reference/refused/missing-hypothesis.flang: не проверено — замечаний 1
$ echo $?
1

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

по примеру

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

случай вариант Узел с левое как л покрывает бесконечно много значений, и один пример его не доказывает. Там берите по предположению.

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

по закону

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

$ flang check docs/examples/reference/refused/unknown-law.flang
модуль «Without a law»: функций 1, из них с доказанным завершением 1; типов 0
FLANG_PROOF_STEP в файле docs/examples/reference/refused/unknown-law.flang, строка 12, столбец 3: теорема «то же»: шаг 1 (чего не бывает, без основания): правило «чего не бывает» ведомости ядро пока не проверяет; проверяет шесть: Н1, Н3, Н5, О1, О10, Разв2
docs/examples/reference/refused/unknown-law.flang: не проверено — замечаний 1
$ echo $?
1

Сообщение значит: правило «чего не бывает» prover не проверяет; он проверяет шесть правил — Н1, Н3, Н5, О1, О10 и Разв2.

Шаг, который называет правило

Шаг может назвать правило вывода, которое применяет, и факты, на которые опирается. Тогда prover проверяет это применение правила, а не ищет доказательство сам.

теорема «результат не больше десяти»
  дано а: число
  дано б: число
  утверждаем результат не больше 10
  затем а не больше б по закону «О1» из строки 5
  затем б не больше 10 по закону «О1» из строки 6
  затем а не больше 10 по закону «О10» из 1 и 2
  по закону «Разв2» из 3 и строки 9
  следовательно доказано

из строки N — строка исходника, откуда берётся факт (предусловие, тело); из K и из K L — номера предыдущих шагов этой же теоремы. Имена правил перечислены в flang/proof/tables/inference-rules.tsv.

Строки таблицы для трёх семейств, которые называют шесть проверяемых правил:

Зачем называть правило: независимая проверка доказательств (flang/proof/checker/checker.c) перепроверяет шаг с названным правилом, а шаг без имени ей приходится принимать на слово prover'а.

Ограничение: prover проверяет шесть правил — Н1, Н3, Н5, О1, О10, Разв2; любое другое имя — ошибка (см. вывод выше).

Сколько доказывается без теоремы и какими правилами — Зачем и как и Спецификация prover'а.

Категории: конвейер, объявленный данными

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

модуль «Order pipeline»

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

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

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

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

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

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

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

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

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

Целая программа: категория, изоморфизм, функтор

модуль «Orders and payments»

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

объект «Платёж»
  копейки является числом
  возвращён является числом

объект «Квитанция»
  копейки является числом
  возвращена является числом

тотальная функция «Отменить заказ»
  принимает заказ: «Заказ»
  возвращает «Заказ»
  пример «обычный заказ отменяется»
    дано заказ равно запись «Заказ» с сумма равным 500 и отменён равным 0
    ожидается запись «Заказ» с сумма равным 500 и отменён равным 1
  запись «Заказ» с сумма равным заказ.сумма и отменён равным 1

тотальная функция «Вернуть платёж»
  принимает платёж: «Платёж»
  возвращает «Платёж»
  пример «обычный платёж возвращается»
    дано платёж равно запись «Платёж» с копейки равным 50000 и возвращён равным 0
    ожидается запись «Платёж» с копейки равным 50000 и возвращён равным 1
  запись «Платёж» с копейки равным платёж.копейки и возвращён равным 1

тотальная функция «Платёж по заказу»
  принимает заказ: «Заказ»
  возвращает «Платёж»
  пример «рубли становятся копейками»
    дано заказ равно запись «Заказ» с сумма равным 500 и отменён равным 0
    ожидается запись «Платёж» с копейки равным 50000 и возвращён равным 0
  запись «Платёж» с копейки равным (заказ.сумма умножить на 100) и возвращён равным заказ.отменён

тотальная функция «Квитанция платежа»
  принимает платёж: «Платёж»
  возвращает «Квитанция»
  пример «копейки переходят в квитанцию»
    дано платёж равно запись «Платёж» с копейки равным 50000 и возвращён равным 0
    ожидается запись «Квитанция» с копейки равным 50000 и возвращена равным 0
  запись «Квитанция» с копейки равным платёж.копейки и возвращена равным платёж.возвращён

тотальная функция «Платёж по квитанции»
  принимает квитанция: «Квитанция»
  возвращает «Платёж»
  пример «копейки возвращаются в платёж»
    дано квитанция равно запись «Квитанция» с копейки равным 50000 и возвращена равным 0
    ожидается запись «Платёж» с копейки равным 50000 и возвращён равным 0
  запись «Платёж» с копейки равным квитанция.копейки и возвращён равным квитанция.возвращена

морфизм «выписать» из «Платёж» в «Квитанция»
  даёт «Квитанция платежа»

морфизм «по квитанции» из «Квитанция» в «Платёж»
  даёт «Платёж по квитанции»

морфизм «отменить заказ» из «Заказ» в «Заказ»
  даёт «Отменить заказ»

морфизм «вернуть платёж» из «Платёж» в «Платёж»
  даёт «Вернуть платёж»

единица «Заказ»
единица «Платёж»

категория «Заказы»
  морфизм «отменить заказ»

категория «Платежи»
  морфизм «вернуть платёж»

изоморфизм «Платёж и квитанция» из «Платёж» в «Квитанция»
  прямой морфизм «выписать»
  обратный морфизм «по квитанции»

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

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

Образ полей и бифунктор

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

модуль «Order pairs»

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

объект «Платёж»
  копейки является числом
  возвращён является числом

объект «Пара заказов»
  первый является «Заказ»
  второй является «Заказ»

тотальная функция «Отменить заказ»
  принимает заказ: «Заказ»
  возвращает «Заказ»
  пример «обычный заказ отменяется»
    дано заказ равно запись «Заказ» с сумма равным 500 и отменён равным 0
    ожидается запись «Заказ» с сумма равным 500 и отменён равным 1
  запись «Заказ» с сумма равным заказ.сумма и отменён равным 1

тотальная функция «Вернуть платёж»
  принимает платёж: «Платёж»
  возвращает «Платёж»
  пример «обычный платёж возвращается»
    дано платёж равно запись «Платёж» с копейки равным 50000 и возвращён равным 0
    ожидается запись «Платёж» с копейки равным 50000 и возвращён равным 1
  запись «Платёж» с копейки равным платёж.копейки и возвращён равным 1

тотальная функция «Отменить оба»
  принимает пара: «Пара заказов»
  возвращает «Пара заказов»
  пример «отменяются оба заказа»
    дано пара равно запись «Пара заказов» с первый равным (запись «Заказ» с сумма равным 500 и отменён равным 0) и второй равным (запись «Заказ» с сумма равным 300 и отменён равным 0)
    ожидается запись «Пара заказов» с первый равным (запись «Заказ» с сумма равным 500 и отменён равным 1) и второй равным (запись «Заказ» с сумма равным 300 и отменён равным 1)
  запись «Пара заказов» с первый равным («Отменить заказ» от пара.первый) и второй равным («Отменить заказ» от пара.второй)

тотальная функция «Платёж по заказу»
  принимает заказ: «Заказ»
  возвращает «Платёж»
  пример «рубли становятся копейками»
    дано заказ равно запись «Заказ» с сумма равным 500 и отменён равным 0
    ожидается запись «Платёж» с копейки равным 50000 и возвращён равным 0
  запись «Платёж» с копейки равным (заказ.сумма умножить на 100) и возвращён равным заказ.отменён

морфизм «отменить заказ» из «Заказ» в «Заказ»
  даёт «Отменить заказ»

морфизм «вернуть платёж» из «Платёж» в «Платёж»
  даёт «Вернуть платёж»

морфизм «отменить оба» из «Пара заказов» в «Пара заказов»
  даёт «Отменить оба»

единица «Заказ»
единица «Платёж»
единица «Пара заказов»

категория «Заказы»
  морфизм «отменить заказ»
  морфизм «отменить оба»

категория «Платежи»
  морфизм «вернуть платёж»

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

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

Проверка отвечает кодом 2 и называет bifunctors среди объявлений, которых двоичный компилятор не судит: бифунктор разобран, но его законы не посчитаны. Строки образа полей разбираются, но с полями объектов не сверяются.

Часть объекта и общая часть двух объектов объявляются вложение и пересечение:

модуль «Order circles»

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

объект «Срочный»
  номер является числом

объект «Оплаченный»
  номер является числом

тотальная функция «Срочный заказ»
  принимает срочный: «Срочный»
  возвращает «Заказ»
  пример «первый»
    дано срочный равно запись «Срочный» с номер равным 1
    ожидается запись «Заказ» с номер равным 1 и срочность равным 1
  пример «второй»
    дано срочный равно запись «Срочный» с номер равным 2
    ожидается запись «Заказ» с номер равным 2 и срочность равным 1
  запись «Заказ» с номер равным срочный.номер и срочность равным 1

тотальная функция «Оплаченный заказ»
  принимает оплаченный: «Оплаченный»
  возвращает «Заказ»
  пример «второй»
    дано оплаченный равно запись «Оплаченный» с номер равным 2
    ожидается запись «Заказ» с номер равным 2 и срочность равным 1
  запись «Заказ» с номер равным оплаченный.номер и срочность равным 1

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

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

Моноид и свёртка кусками

модуль «Monoids»

тотальная функция «Сложить точные»
  принимает а: точное целое, б: точное целое
  возвращает точное целое
  пример «перенос через разряд»
    дано а равно [4194303]
    дано б равно [1]
    ожидается [0, 1]
  а плюс б

тотальная функция «Точный ноль»
  возвращает точное целое
  []

моноид «Сумма точных»
  носитель точное целое
  операция «Сложить точные»
  единица []

тотальная функция «Итог»
  принимает суммы: список точное целое
  возвращает точное целое
  пример «три слагаемых»
    дано суммы равно [[1], [2], [3]]
    ожидается [6]
  свёртка суммы начиная с «Точный ноль» как акк и эл → «Сложить точные» от акк и эл

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

тотальная функция «Противоположное»
  принимает а: число
  возвращает число
  пример «три»
    дано а равно 3
    ожидается -3
  0 минус а

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

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

тотальная функция «Квадраты»
  принимает числа: список число
  возвращает список число
  пример «три числа»
    дано числа равно [1, 2, 3]
    ожидается [1, 4, 9]
  отобразить числа как х → х умножить на х

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

$ flang check docs/examples/reference/ru/monoids.flang
моноид «Сумма чисел»: сетка 5 значений, троек 125, нарушений 0 — ПОСЧИТАНО НА СЕТКЕ, не доказано
свойство «коммутативность» у «Сложить числа»: сетка 3 значений, пар 9, нарушений 0 — ПОСЧИТАНО НА СЕТКЕ, не доказано
модуль «Monoids»: функций 6, из них с доказанным завершением 6; типов 0
моноид «Сумма точных»: сочетательность и единица доказаны ядром — свёртка операцией «Сложить точные» считается кусками на всех потоках
моноид «Сумма чисел»: сочетательность и единица ядром НЕ доказаны — свёртка операцией «Сложить числа» идёт по порядку на одном потоке
docs/examples/reference/ru/monoids.flang: проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет

Если законы доказаны, свёртка, тело которой — ровно вызов операции от накопителя и элемента, в напечатанном коде считается кусками на нескольких потоках. Над число сочетательность ложна, и такая свёртка идёт по порядку. отобразить, тело которого зовёт только тотальные функции, печатается так же; на куски напечатанный код режет список, когда первые элементы показали, что счёт долгий. Какие цели печати считают кусками, а какие по порядку, — Параллельный отобразить и свёртка по моноиду. обратный элемент «Ф» объявляет моноид с обращением, а свойство — закон одной операции (коммутативность, идемпотентность и другие имена, закреплённые языком). Такие законы двоичный компилятор считает на сетке значений и пишет об этом: ПОСЧИТАНО НА СЕТКЕ, не доказано. Ограничение: свойство с незнакомым именем не проверяется вовсе, и flang check об этом молчит — имя пишите ровно так, как в Словаре и спецификации категорий.

Что компилятор проверяет, а что нет

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

$ flang check flang/ct/order-shipment.flang
категория «Отгрузки»: сетка 5 значений на 3 объектах, троек стрелок 7, нарушений 0 — ПОСЧИТАНО НА СЕТКЕ, не доказано
изоморфизм «Отгрузка и накладная»: сетка 2 значений, нарушений 0 — ПОСЧИТАНО НА СЕТКЕ, не доказано
модуль «Order shipment»: функций 6, из них с доказанным завершением 6; типов 3
flang/ct/order-shipment.flang: проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет

То есть: 5 значений на 3 объектах, 7 троек стрелок, нарушений 0 — посчитано на этих значениях, не доказано. Нарушение — ошибка с кодом 1 и значениями, на которых закон ломается, и код не генерируется. Так же с естественным преобразованием: FLANG_TRANSFORM_NOT_NATURAL с обоими путями и их значениями.

Не проверяет: форму объявлений. Замкнутость под композицией, единицы у объектов, совпадение концов у составленных стрелок, форму функтора двоичный компилятор не проверяет. Он пишет об этом отдельной строкой и завершается кодом 2, так что за успех это не сойдёт. В частности:

• переставленный порядок композиции («отгрузить» после «выставить») ошибки не даёт, хотя контракт языка описывает FLANG_COMPOSE_MISMATCH;
• стрелка, не совпадающая со своей функцией, ошибки не даёт, хотя FLANG_MORPHISM_SHAPE описан;
• некоммутирующий квадрат функтора ошибки не даёт: функторы не проверяются вовсе, и FLANG_FUNCTOR_SQUARE не срабатывает.

Итого сегодня объявление категории документирует намерение и проверяет свои законы на значениях примеров; форму оно не проверяет. С полными прогонами — Категорная поверхность.

Прежде чем брать:

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

Полный контракт — Категории и функторы. Где кончается «доказано» и начинается «проверено» — Что доказано, а что нет.

Монада и в монаде: цепочка шагов, каждый из которых может не дать ответа

модуль «Discount»

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

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

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

тотальная функция «Сплющить» от «А»
  принимает вложенное: «Возможно» от («Возможно» от «А»)
  возвращает «Возможно» от «А»
  разбор вложенное
    случай вариант «Есть» с значение как внутри
      то внутри
    случай «Нет»
      то вариант «Нет»

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

тотальная функция «Скидка по цене»
  принимает цена: число
  возвращает «Возможно» от числа
  если цена не меньше 400
    то вариант «Есть» с значение равным (цена делить на 10)
    иначе вариант «Нет»

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

Компилятор разворачивает блок во вложенные разбор по вариантам типа. Цепочку «если нет — вернуть нет» на каждом шаге писать не нужно — та же идея, что ? в Rust или do в Haskell.

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

Процессы и надзор

Состояние принадлежит процессу, как у актора в Erlang. Обработчик — обычная тотальная функция: принимает состояние и сообщение, возвращает новое состояние и список действий. Отправка сообщения — действие в этом списке, а не side effect.

модуль «Counter»

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

объект «Отклик»
  «состояние»: «Счёт»
  «действия»: список «Действие»

тип «Команда»
  вариант «прибавить» содержит «сколько»: число

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

надзор «Учёт»
  процесс «Счётчик» стратегия «перезапустить»
  порог отказов 3 за 5000 миллисекунд иначе «передать выше»

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

тотальная функция «шаг счёта»
  принимает текущее: «Счёт», сообщение: «Команда»
  возвращает «Отклик»
  пример «прибавление меняет состояние и ничего не шлёт»
    дано текущее равно (запись «Счёт» с «всего» равным 1)
    дано сообщение равно (вариант «прибавить» с «сколько» равным 2)
    ожидается (запись «Отклик» с «состояние» равным (запись «Счёт» с «всего» равным 3) и «действия» равным [])
  разбор сообщение
    случай вариант «прибавить» с «сколько» как сколько
      пусть новое равно (запись «Счёт» с «всего» равным (текущее.«всего» плюс сколько))
      запись «Отклик» с «состояние» равным новое и «действия» равным []

прогон «два прибавления»
  семя 1
  дано «Счётчик» принимает (вариант «прибавить» с «сколько» равным 2)
  дано «Счётчик» принимает (вариант «прибавить» с «сколько» равным 3)
  ожидается «Счётчик» равен (запись «Счёт» с «всего» равным 5)

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

модуль «Counter with limits»

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

объект «Отклик»
  «состояние»: «Счёт»
  «действия»: список «Действие»

тип «Команда»
  вариант «прибавить» содержит «сколько»: число

процесс «Счётчик»
  состояние «Счёт»
  начинает с «пустой счёт»
  принимает «Команда» с ящиком 4 сообщений
  обрабатывает «шаг счёта» с запасом 2000 витков

надзор «Учёт»
  процесс «Счётчик» стратегия «перезапустить»
  порог отказов 3 за 5000 миллисекунд иначе «передать выше»

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

функция «шаг счёта»
  принимает текущее: «Счёт», сообщение: «Команда»
  возвращает «Отклик»
  пример «прибавление меняет состояние и ничего не шлёт»
    дано текущее равно (запись «Счёт» с «всего» равным 1)
    дано сообщение равно (вариант «прибавить» с «сколько» равным 2)
    ожидается (запись «Отклик» с «состояние» равным (запись «Счёт» с «всего» равным 3) и «действия» равным [])
  разбор сообщение
    случай вариант «прибавить» с «сколько» как сколько
      пусть новое равно (запись «Счёт» с «всего» равным (текущее.«всего» плюс сколько))
      запись «Отклик» с «состояние» равным новое и «действия» равным []

прогон «два прибавления»
  семя от 1 до 3
  дано «Счётчик» принимает (вариант «прибавить» с «сколько» равным 2)
  дано «Счётчик» принимает (вариант «прибавить» с «сколько» равным 3)
  ожидается «Счётчик» равен (запись «Счёт» с «всего» равным 5)

flang test исполняет блок прогон планировщиком flang/self/conc.flang и сверяет его ожидания; блок считается одним примером, и ложное ожидание валит файл кодом 1. flang check блок разбирает и сверяет, но не исполняет. Планировщик печатается и вместе с кодом целей c, elixir, js и ts — см. Процессы.

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

Модель целиком — Процессы и отказоустойчивость.

Слова, которых нет в примерах выше

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

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

$ flang check docs/examples/reference/refused/mixed-theorem-forms.flang
FLANG_PARSE в файле docs/examples/reference/refused/mixed-theorem-forms.flang, строка 11, столбец 1: теорема «цена та же» смешала две формы: дано «Объект» имеет «поле» — из старой, а рядом стоят слова доказательства. Выберите одну форму
docs/examples/reference/refused/mixed-theorem-forms.flang: не проверено — замечаний 1
$ echo $?
1

Так же ведут себя в данных, по морфизму и следовательно «вывод».

Слова раздела на всех четырёх поверхностях, из таблицы лексера:

Чего в языке нет

Дальше

• Словарь языка — все 159 понятий с четырьмя написаниями
• Операции языка — задача → чем она решается
• Учебник — то же по шагам, с нуля
• Спецификация языка — контракт целиком
• Известные ограничения — что язык не делает и не будет
• Справочник библиотеки — модули стандартной библиотеки и что берут из каждого