flang construct reference
flang 0.7.32 constructs with examples. Each example is checked by this compiler version when the page is built. Language documentation.
Programs and functions
Module and imports модуль, экспортирует, использует
A file starts with the module name. «экспортирует» makes functions visible to other modules; «использует» imports a standard library module.
модуль «Report»
экспортирует «Итог»
использует «Lists»
тотальная функция «Итог»
принимает элементы: список числа
возвращает число
пример «повторы не считаются дважды»
дано элементы равно [3, 1, 3, 2, 1]
ожидается 6
«Сумма» от («Уникальные» от элементы)Total function and a measure тотальная функция, убывает
«тотальная» means the compiler proved the function terminates on every input. For recursion it looks for a decreasing argument; «убывает б» names it explicitly.
модуль «Measure»
тотальная функция «НОД»
принимает а: число, б: число
возвращает число
убывает б
пример «двенадцать и восемнадцать»
дано а равно 12
дано б равно 18
ожидается 6
если б равен 0
то а
иначе «НОД» от б и (а остаток от б)«если» and examples если … то … иначе, пример
«если» is an expression and always has «иначе». An «пример» block is a test inside the function: «flang check» evaluates it and fails if the answer differs.
модуль «Branching»
тотальная функция «Сумма до»
принимает н: неотрицательное
возвращает число
пример «до нуля — ноль»
дано н равно 0
ожидается 0
пример «до трёх — шесть»
дано н равно 3
ожидается 6
если н не больше 0
то 0
иначе н плюс («Сумма до» от (н минус 1))«пусть», objects and records пусть, объект, запись
«объект» declares a record type, «запись … с … равным …» builds one. «пусть» names an intermediate value; there is no reassignment.
модуль «Binding»
объект «Позиция»
цена является числом
количество является числом
тотальная функция «Стоимость позиции»
принимает позиция: «Позиция»
возвращает число
пример «две штуки по триста»
дано позиция равно запись «Позиция» с цена равным 300 и количество равным 2
ожидается 660
пусть чистое равно позиция.цена умножить на позиция.количество
пусть налог равно 10 процентов от чистое
чистое плюс налогFunctions as values функция из … в …
A function can be passed as an argument. «функция «Прибавить» с а равным 10» fixes the first argument (partial application).
модуль «Function as a value»
тотальная функция «Удвоить»
принимает х: число
возвращает число
х умножить на 2
тотальная функция «Прибавить»
принимает а: число, б: число
возвращает число
а плюс б
тотальная функция «Применить дважды»
принимает ф: функция из числа в число, х: число
возвращает число
ф от (ф от х)
тотальная функция «Проба»
возвращает число
пример «пятёрка удвоена дважды»
ожидается 20
«Применить дважды» от функция «Удвоить» и 5
тотальная функция «Проба с захватом»
возвращает число
пример «десятка прибавлена дважды»
ожидается 25
«Применить дважды» от (функция «Прибавить» с а равным 10) и 5Data
Types with variants тип, вариант, иногда является
«тип» with «вариант» is a sum type, like an enum with data. «иногда является» makes a field optional.
модуль «Types»
объект «Позиция»
название является строкой
цена является числом
скидка иногда является числом
тип «Счёт» это список «Позиция»
тип «Ответ»
вариант Успех содержит значение: число
вариант Отказ содержит причина: строка
тотальная функция «Проверить цену»
принимает позиция: «Позиция»
возвращает «Ответ»
пример «цена есть»
дано позиция равно запись «Позиция» с название равным "болт" и цена равным 30
ожидается вариант Успех с значение равным 30
пример «ноль — не цена»
дано позиция равно запись «Позиция» с название равным "гайка" и цена равным 0
ожидается вариант Отказ с причина равным "цена не положительна"
если позиция.цена больше 0
то вариант Успех с значение равным позиция.цена
иначе вариант Отказ с причина равным "цена не положительна"Pattern matching разбор, случай
«разбор» goes over the variants of a type. The compiler requires every variant to be handled and proves that structural recursion terminates.
модуль «Tree»
тип «Дерево»
вариант Лист
вариант Узел содержит значение: число, левое: «Дерево», правое: «Дерево»
тотальная функция «Узлов»
принимает дерево: «Дерево»
возвращает число
пример «в листе узлов нет»
дано дерево равно вариант Лист
ожидается 0
разбор дерева
случай Лист
то 0
случай вариант Узел с левое как л и правое как п
то 1 плюс («Узлов» от л) плюс («Узлов» от п)Number types сотых, неотрицательное, требует
«число» is a plain double. «неотрицательное», «целое», «сотых» (money in cents) narrow the values, and the compiler uses that in proofs.
модуль «Exact types»
тотальная функция «Копейки заказа»
принимает цена: сотых, штук: неотрицательное
возвращает число
пример «три по 19.99»
дано цена равно 1999
дано штук равно 3
ожидается 5997
цена умножить на штук
тотальная функция «Доля»
принимает часть: неотрицательное, всего: неотрицательное
возвращает число
требует «делитель положителен» всего больше 0
пример «половина»
дано часть равно 1
дано всего равно 2
ожидается 0.5
часть делить на всегоStrings строка
A string in double or single quotes; a line break can be written right inside the literal.
модуль «Two spellings»
тотальная функция «Через перевод строки»
возвращает строка
пример «то же, что с \n»
ожидается "первая\nвторая"
"первая
вторая"
тотальная функция «Одинарными кавычками»
возвращает строка
пример «те же кавычки, только другие»
ожидается "текст"
'текст'Lists: filter and map отфильтровать, отобразить, разделить
Built-in list forms: «отфильтровать … где» (filter), «отобразить … как» (map), «разделить … по» (split). The language has no loops.
модуль «Built-in forms»
тотальная функция «Длинные слова»
принимает текст: строка
возвращает список строки
пример «короткое слово выброшено»
дано текст равно "раз дважды трижды"
ожидается ["дважды", "трижды"]
отфильтровать (разделить текст по " ") где слово → (длина слово) больше 3
тотальная функция «Длины слов»
принимает слова: список строки
возвращает список числа
пример «три слова»
дано слова равно ["раз", "дважды", "трижды"]
ожидается [3, 6, 6]
отобразить слова как слово → длина словоFold свёртка … начиная с … как
«свёртка» is reduce: one pass over a list with an accumulator.
модуль «Fold»
тотальная функция «Произведение»
принимает элементы: список числа
возвращает число
пример «три множителя»
дано элементы равно [2, 3, 4]
ожидается 24
свёртка элементы начиная с 1 как акк и эл → акк умножить на элProofs
Precondition требует
«требует» is a condition on the inputs. Callers must satisfy it, and the body may rely on it.
модуль «Precondition»
тотальная функция «Доля»
принимает часть: неотрицательное, всего: неотрицательное
возвращает число
требует «делитель положителен» всего больше 0
пример «половина»
дано часть равно 1
дано всего равно 2
ожидается 0.5
часть делить на всегоPostcondition обеспечивает
«обеспечивает» is a promise about the result for every input. «flang check --proof» reports whether it is proved.
модуль «Postcondition»
тотальная функция «Удвоить все»
принимает элементы: список числа
возвращает список числа
для всех элементы обеспечивает «длина сохраняется» (длина результат) равен (длина элементы)
пример «три элемента»
дано элементы равно [1, 2, 3]
ожидается [2, 4, 6]
отобразить элементы как э → э умножить на 2A property of every element для всех … из …:
«для всех п из результат: …» promises something about every element of a list.
модуль «For all after a filter»
тотальная функция «Только положительные»
принимает элементы: список числа
возвращает список числа
обеспечивает «все положительны» для всех п из результат: п больше 0
пример «Смесь»
дано элементы равно [3, 0, 5]
ожидается [3, 5]
отфильтровать элементы где э → э больше 0A statement утверждение
«утверждение» is a property outside any function: about specific values or «для всех» values of a type.
модуль «Free statements»
утверждение «длина пустого списка нулевая»
утверждаем (длина пустой список) равен 0
утверждение «ноль нейтрален при сложении»
для всех н: неотрицательное таких что н больше 0
утверждаем (н плюс 0) равен нA theorem теорема, индукция по, по предположению
When the compiler cannot derive a promise on its own, you write the proof as a theorem: induction, cases and a reason for each step.
модуль «Theorem»
тотальная функция «Сумма до»
принимает н: неотрицательное
возвращает число
для всех н обеспечивает «сумма до неотрицательна» результат не меньше 0
пример «шагов не осталось»
дано н равно 0
ожидается 0
если н не больше 0
то 0
иначе н плюс («Сумма до» от (н минус 1))
теорема «сумма до неотрицательна»
дано н: неотрицательное
утверждаем результат не меньше 0
индукция по н убывает н
случай 0
то по примеру «шагов не осталось»
случай любое
то по предположению
следовательно доказаноReusing a proved property по свойству
«по свойству» refers to an already proved promise of another function.
модуль «Property»
тотальная функция «Удвоить все»
принимает элементы: список числа
возвращает список числа
для всех элементы обеспечивает «удвоение длины не меняет» (длина результат) равен (длина элементы)
отобразить элементы как э → э умножить на 2
тотальная функция «Через удвоение»
принимает элементы: список числа
возвращает список числа
для всех элементы обеспечивает «через удвоение длина та же» (длина результат) равен (длина элементы)
«Удвоить все» от элементы
теорема «через удвоение длина та же»
дано элементы: список числа
утверждаем (длина результат) равен (длина элементы)
по свойству «удвоение длины не меняет»
следовательно доказаноInduction over your own type индукция по своему типу
Induction works over any declared type with variants, not only over numbers.
модуль «Own natural»
тип «Нат»
вариант «Ноль»
вариант «Следующий» содержит пред: «Нат»
тотальная функция «К числу»
принимает н: «Нат»
возвращает число
разбор н
случай вариант «Ноль»
то 0
случай вариант «Следующий» с пред как п
то («К числу» от п) плюс 1
утверждение «шаг растит счёт на один»
для всех н: «Нат»
утверждаем («К числу» от (вариант «Следующий» с пред равным н)) равно ((«К числу» от н) плюс 1)
теорема «шаг растит счёт на один»
дано н: «Нат»
утверждаем («К числу» от (вариант «Следующий» с пред равным н)) равно ((«К числу» от н) плюс 1)
индукция по н
случай вариант «Следующий» с пред как п
то по предположению
следовательно доказаноProcesses
Process and supervision процесс, надзор, прогон
«процесс» keeps state and handles messages with a pure function, «надзор» restarts it on failures, «прогон» tests a sequence of messages.
модуль «Counter»
объект «Счёт»
«всего»: число
объект «Отклик»
«состояние»: «Счёт»
«действия»: список «Действие»
тип «Команда»
вариант «прибавить» содержит «сколько»: число
процесс «Счётчик»
состояние «Счёт»
начинает с «пустой счёт»
принимает «Команда»
обрабатывает «шаг счёта»
надзор «Учёт»
процесс «Счётчик» стратегия «перезапустить»
порог отказов 3 за 5000 миллисекунд иначе «передать выше»
тотальная функция «пустой счёт»
возвращает «Счёт»
запись «Счёт» с «всего» равным 0
тотальная функция «шаг счёта»
принимает текущее: «Счёт», сообщение: «Команда»
возвращает «Отклик»
пример «прибавление меняет состояние и ничего не шлёт»
дано текущее равно (запись «Счёт» с «всего» равным 1)
дано сообщение равно (вариант «прибавить» с «сколько» равным 2)
ожидается (запись «Отклик» с «состояние» равным (запись «Счёт» с «всего» равным 3) и «действия» равным [])
разбор сообщение
случай вариант «прибавить» с «сколько» как сколько
пусть новое равно (запись «Счёт» с «всего» равным (текущее.«всего» плюс сколько))
запись «Отклик» с «состояние» равным новое и «действия» равным []
прогон «два прибавления»
семя 1
дано «Счётчик» принимает (вариант «прибавить» с «сколько» равным 2)
дано «Счётчик» принимает (вариант «прибавить» с «сколько» равным 3)
ожидается «Счётчик» равен (запись «Счёт» с «всего» равным 5)