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

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

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

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

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

flang check файл.flang

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

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

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

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

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

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

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

Модуль и ввоз

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

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

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

FLANG_UNKNOWN_NAME, строка 635, столбец 74: неизвестная функция «Все не меньше»
FLANG_UNKNOWN_NAME, строка 635, столбец 130: неизвестная функция «Максимум»

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

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

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

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

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

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

Границы: имена модулей не переводятся. Русский «Списки» ввозится под этим именем и из файла, написанного английскими словами.

Функция

Порядок частей закреплён. Тело — последним, одной формой.

модуль «Подпись»

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

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

Границы:

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

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

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

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

модуль «Мера»

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

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

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

Ветвление, разбор суммы, свёртка, связывание. Циклов нет.

разбор — по сумме типов

модуль «Дерево»

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

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

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

Что даёт: исчерпывающность считает проверка типов — пропущенный вариант это отказ, а не молчание. Рекурсия по части значения тотальна по построению. Индукция в теореме цепляется только к этой форме.

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

модуль «Свёртка»

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

Что даёт: тотальность по построению — список конечен, проход один.

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

если — ветвление

модуль «Ветвление»

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

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

пусть — связывание имени

модуль «Связывание»

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

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

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

Типы

Скалярные

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

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

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

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

модуль «Точные типы»

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

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

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

FLANG_TYPE, строка 6, столбец 5: функция «Сумма неотрицательное» объявлена как неотрицательное, а тело даёт число

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

Список

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

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

Запись

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

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

Границы: запись инвариантна. Замены поля нет — значения неизменяемы, строится новая запись.

Сумма типов

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

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

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

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

модуль «Типы»

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

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

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

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

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

Псевдоним и параметрический тип

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

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

Параметры вводятся словом от и им же подставляются. Аргументы при вызове выводятся из значений — писать их негде.

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

Тип функции

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

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

Выражения

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

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

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

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

модуль «Встроенные формы»

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

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

Предлоги закреплены, и они разные у разных форм:

модуль «Строки»

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

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

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

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

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

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

модуль «Функция как значение»

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

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

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

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

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

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

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

Утверждения о поведении

Четыре слова обещают о функции больше, чем её тип. Проверяются они по-разному, и разницу видно сразу.

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

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

модуль «Предусловие»

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

Что даёт: внутри функции условие становится допущением — на него ссылается по предположению в теореме, даже когда индукции нет.

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

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

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

модуль «Постусловие»

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

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

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

теорема

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

модуль «Теорема»

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

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

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

модуль «Свойство»

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

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

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

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

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

Шаг без обоснования отвергается разбором. Обоснований четыре, и каждое работает в своём месте.

по свойству

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

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

FLANG_PROOF_STEP, строка 12, столбец 3: шаг 1, теорема «длина сохраняется»: «по свойству «длина сохраняется»» ссылается на то самое постусловие, которое сейчас доказывается — это круг. Часть значения обосновывает «по предположению», а не ссылка на саму цель

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

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

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

Без обоих отказ называет, чего именно не хватило:

FLANG_PROOF_INDUCTION_STEP, строка 12, столбец 3: шаг 1, теорема «половина неотрицательна»: «по предположению» стоит вне индукции, а допущений у этой цели нет ни одного: ни посылки индукции (её даёт `индукция по`), ни предусловия функции (его даёт `требует`). Предполагать не о чем

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

по примеру

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

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

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

по закону

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

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

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

Категорная поверхность

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

модуль «Проводка заказа»

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

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

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

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

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

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

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

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

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

Что она даёт разработчику сегодня

Одно даёт, а трёх обещанных отказов не даёт, и путать это нельзя. Проверено прогоном 21 августа 2026.

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

категория «Отгрузки»: сетка 5 значений на 3 объектах, троек стрелок 7,
нарушений 0 — ПОСЧИТАНО НА СЕТКЕ, не доказано

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

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

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

Все три кода в исходниках есть, правила записаны — а до них у двоичного не доходят руки. Читать это надо так: объявление категории сегодня документирует намерение и даёт счёт законов на сетке; сверкой устройства оно не является. Подробнее с прогонами — Категорная поверхность.

По-деловому это значит «отменённый заказ отменён везде», и отказ предъявляет заказ, на котором два пути разошлись.

Границы, и их надо знать до того, как браться:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

модуль «Счётчик»

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

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

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

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

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

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

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

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

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

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

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

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

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

FLANG_PARSE, строка 12, столбец 1: теорема «цена та же» смешала две формы: дано «Объект» имеет «поле» — из старой, а рядом стоят слова доказательства. Выберите одну форму

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

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

Дальше

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