Файл, модуль и типы — из чего состоит программа. Карточек: 5.

• Имя для типа: тип «…» это список «…»

  это списокlist

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

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

• Модуль: имя файла и его экспорт

  модульmodule экспортируетexports

  модуль «Формулы»
    экспортирует «С НДС», «Копейки в рубли»

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

• Запись: объект «…» и его поля

  объектobject записьrecord

  объект «Клиент»
      ожидается (запись «Клиент» с «имя» равным "Мария" и «покупок» равным 0)
    запись «Клиент» с «имя» равным имя и «покупок» равным 0

  Запись — произведение: набор полей с типами. Слова «объект» и «запись» означают здесь одно и то же (в модели FTS то же самое пишут словом «структура»), а имя типа поля — часть контракта и потому точное.

• Сумма типов: тип «…» и его варианты

  типtype вариантvariant

  тип «Оплата»
    вариант «Карта» содержит «последние четыре»: строка
    вариант «Наличные»
    вариант «Счёт» содержит «номер»: строка, «отсрочка дней»: число
      дано оплата равно (вариант «Карта» с «последние четыре» равным "4242")

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

• Импорт: использует «…» из "…" только «…»

  используетuses толькоonly изfrom

    использует «Формулы» из "module.flang" только «С НДС»

  Единственная конструкция языка, которой нужен диск. Пример проверяется командой: `flang check` рядом с файлом читает module.flang, связывает и прогоняет примеры — это и записано в отчёте npm test. «Только» сужает импорт до перечисленных имён: без него модуль вносит все свои, и одного совпадения хватит, чтобы связывание отказало.

Функции и примеры — объявление, вызов, тест внутри. Карточек: 3.

• Вызов функции: «Имя» от аргумента и аргумента

  отof иand

    пусть ставка равно «Ставка» от сумма
    («Скидка с потолком» от первый и 1000) плюс («Скидка с потолком» от второй и 1000)

  Вызов пишется предлогом: «Имя» от X. Второй и следующие аргументы присоединяются словом «и». Функции не являются значениями: передать функцию в функцию нельзя, и это плата за печать в языки без замыканий.

• Пример: тест внутри объявления

  примерexample даноgiven ожидаетсяexpected

    пример «Ниже порога — ничего»
      дано сумма равно 900
      ожидается 0
    пример «Ровно на пороге»
      дано сумма равно 1000

  Пример — часть функции, а не отдельный файл рядом. «Дано» задаёт аргумент по имени, «ожидается» — результат. Их выполняет `flang test`, и они же выполняются на этой странице во вкладке «Примеры».

• Функция: принимает, возвращает, тело

  тотальнаяtotal функцияfunction принимаетaccepts возвращаетreturns

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

  Объявление из трёх строк: имя, что принимает, что возвращает. Дальше — тело, одно выражение. Слово «тотальная» — обещание завершения, и компилятор его проверяет: не доказал убывания — FLANG_NOT_TOTAL, а не предупреждение.

Выражения — ветвление, разбор, локальные имена. Карточек: 5.

• Доступ к полю: поле «…» у значения

  полеfield уat

    (поле «цена» у позиция) умножить на позиция.«количество»

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

• Ветвление: если … то … иначе …

  еслиif тоthen иначеelse

    если покупок не меньше 20
      то "золотой"
      иначе если покупок не меньше 3
        то "постоянный"
        иначе "новый"

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

• Локальное имя: пусть … равно …

  пустьlet

    пусть доставка равно вес умножить на 50
    пусть надбавка равно если вес больше 10 то доставка умножить на 2 иначе доставка

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

• Разбор списка: разбор … случай пусто … случай голова и хвост …

  разборmatch случайcase пустоempty голова и хвостhead and tail

    разбор числа
      случай пусто
      случай голова и хвост

  Цикла в языке нет; список обходится разбором на пустой и «голова и хвост». Хвост — часть исходного значения, поэтому рекурсия по нему структурно убывает, и «тотальная» доказывается. Незакрытый случай — не забытая ветка на проде, а FLANG_MATCH_NOT_EXHAUSTIVE при проверке.

• Образцы варианта: случай вариант «…» с «…» как …, случай любое

  любоеany какas

      случай вариант «Успех» с значение как число
      случай вариант «Отказ» с причина как текст
      случай любое

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

Списки — вместо циклов. Карточек: 5.

• Отбор: отфильтровать … где имя → условие

  отфильтроватьfilter гдеwhere

    отфильтровать суммы где сумма → сумма не меньше 10000

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

• Свёртка: свёртка … начиная с … как накопитель и элемент → выражение

  свёрткаfold начиная сstarting with

    свёртка цены начиная с 0 как итог и цена → итог плюс цена
    свёртка цены начиная с 0 как лучшее и цена → если цена больше лучшее то цена иначе лучшее

  Свёртка заменяет цикл со счётчиком: накопитель и элемент — два имени, и после стрелки написано, чем накопитель станет. Начальное значение называет автор, а не подставляет рантайм, — тот же принцип, что у «начинает с» в утилите FTS.

• Голова, хвост, длина

  головаhead хвостtail длинаlength

    голова позиции
    длина (хвост позиции)

  Три встроенные формы над списком. «Длина» работает и над строкой — там она считает кодовые точки, а не единицы UTF-16, поэтому кириллица и эмодзи считаются по-человечески.

• Списки: пустой список, список из …, добавить … к …

  пустой списокempty list список изlist of добавитьadd вto

    добавить (первое плюс 2) к (добавить (первое плюс 1) к (добавить первое к пустой список))
    список из 100, 200, 300

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

• Отображение: отобразить … как имя → выражение

  отобразитьmap

    отобразить цены как цена → цена умножить на 1.2

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

Строки — строка как данные. Карточек: 5.

• Превращения: к числу, к строке

  к числуto number к строкеto text

    к числу текст
    к строке согласен

  «К строке» от признака даёт «да» или «нет», а не true/false: поверхность языка русская, и все восемь целей печати обязаны повторять именно её. «К числу» на непригодной строке прекращает вычисление целиком — безопасный разбор строится вариантом «Успех»/«Ошибка», как в модуле stdlib «Результат».

• Разложение строки: разложить … на символы

  разложитьdecompose на символыinto characters

    свёртка (разложить текст на символы) начиная с "" как перевёрнутое и буква → соединить буква с перевёрнутое
    длина (разложить текст на символы)

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

• Склейка и разбиение: соединить … с …, разделить … по …

  соединитьjoin разделитьsplit поby сwith

    соединить (соединить имя с " ") с фамилия
    разделить адрес по ","

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

• Символ и подстрока: символ … в …, подстрока … с … по …

  символchar подстрокаsubstring

    символ 1 в имя
    подстрока телефон с 4 по 6

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

• Проверки строки: содержит, начинается с

  содержитcontains начинается сbegins with

    адрес содержит "@"
    телефон начинается с "+7"

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

Числа, сравнения, литералы — арифметика и шесть сравнений. Карточек: 3.

• Арифметика: плюс, минус, умножить на, делить на, остаток от

  плюсplus минусminus умножить наtimes делить наdivided by остаток отmodulo

    товары плюс доставка
    внесено минус цена
    (сумма минус (сумма остаток от 100)) делить на 100
    цена умножить на количество

  Числа — IEEE-754 double, как в ядре FTS: расхождение по арифметике с уже напечатанным кодом недопустимо. Деление на ноль даёт бесконечность, а не ошибку, — печать в JavaScript обязана давать то же самое значение.

• Сравнения: шесть и только шесть

  равенequals не равенis not equal to большеis greater than меньшеis less than не большеis at most не меньшеis at least

      дано значение равно 100
      дано граница равно 100
      дано значение равно 120
      дано граница равно 100
      дано значение равно 20

  Сравнений в языке ровно шесть: равен, не равен, больше, меньше, не больше, не меньше. Седьмого нет, и придумать его нельзя — компилятор откажет с номером строки. Равенство скаляров — Object.is, списки и записи сравниваются структурно.

• Литералы: да, нет, ничто

  даtrue нетfalse ничтоnull

      дано юрлицо равно да
      ожидается да
      дано юрлицо равно нет
      ожидается нет
    возвращает ничто

  Признак записывается словами «да» и «нет», пустое значение — «ничто». В английской записи это true/false/null и yes/no, и обе поверхности дают один и тот же AST: файл на русском и файл на английском компилируются в одно.

Модель FTS — категория, утилита, правило, свойство. Карточек: 6.

• Категория: предметная область и её объекты

  категорияcategory являетсяis

  категория «Продажи»
      сумма является деньгами
      «постоянный клиент» является признаком

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

• Вложенный объект: вложен объект «…»

  вложен объектnested object

      вложен объект Адрес

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

• Свойство: постусловие обо всех входах

  свойствоproperty результатresult

      свойство «Скидка ограничена»
        результат не больше 15000
        ожидается результат равен 2000
        ожидается результат равен 15000

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

• Правило: условие и одно действие

  правилоrule процентовpercent

      правило «Большая покупка»
        то добавить 10 процентов от поля сумма
      правило «Постоянный клиент»
        то добавить 5 процентов от поля сумма

  Срабатывают ВСЕ правила, чьи условия истинны, и складываются: это не цепочка if / else if. Условия соединяются словом «и». Проценты считаются от поля: «10 процентов от поля сумма» — дословно та же формула, что уедет в напечатанный код.

• Типы полей: строка, число, деньги, дата, признак, состояние

  строкаstring числоnumber деньгиmoney датаdate признакboolean иногда являетсяmay be

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

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

• Утилита: вход, тип результата и стартовое значение

  утилитаutility начинает сstarts with

    утилита «Стоимость доставки»
      начинает с 200

  Три строки обязательны: что принимает, что возвращает и с чего начинает. Ноль в «начинает с» пишет автор модели, а не подставляет рантайм — без этой строки компилятор откажет с FTS_UTILITY_INITIAL. Утилита — это будущая функция: `flang emit` печатает её в восемь языков.

Категории и морфизмы — стрелки, теоремы, функторы. Карточек: 8.

• Бифунктор: перевод, у которого два входа

  бифункторbifunctor объектыobjects морфизмыmorphisms

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

  Функтор переводит одну категорию в другую, бифунктор — две сразу: ключ отображения не имя, а ПАРА имён. Так описывают всё, что берёт две вещи и делает третью: пару значений, «либо одно, либо другое», словарь ключей и значений. Законы проверяются тем же способом, что у функтора, и это важнее самой формы: морфизм в языке — ОБЪЯВЛЕНИЕ, домен и кодомен известны до запуска, поэтому «образ композиции есть композиция образов» решается сличением имён — без сетки входов, без вычислений, без решателя.

• Композиция: после, цепочка, единица

  послеafter цепочкаchain сначалаfirst затемnext единицаidentity

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

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

• Функтор: отображение одной категории в другую

  функторfunctor отображается вmaps to отображается в полеmaps to field отображается в морфизмmaps to morphism

  функтор «Запрос страницы в условие выборки» из «Запрос списка» в «Хранилище»
    объект «Запрос страницы» отображается в «Условие выборки»
      поле «номер страницы» отображается в поле «смещение»
      поле «размер страницы» отображается в поле «предел»
    морфизм «нормализовать» отображается в морфизм «ограничить»

  Функтор переводит объекты в объекты, поля в поля и морфизмы в морфизмы — целиком, а не «примерно». Именно поэтому переход между двумя моделями (запрос списка и хранилище, скидки и подписки) можно проверить, а не пересказать в комментарии.

• Изоморфизм: два представления одного и того же

  изоморфизмisomorphism прямой морфизмforward morphism обратный морфизмinverse morphism

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

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

• Моноид и группа: закон вместо соглашения

  моноидmonoid носительcarrier операцияoperation обратный элементinverse element

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

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

• Морфизм-стрелка: морфизм «…» из «…» в «…»

  морфизмmorphism

  морфизм «отгрузить» из «Заказ» в «Отгрузка»

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

• Утверждение: фигурная поверхность и свидетельство в данных

  утверждениеproposition

    proposition witness TaskRow.status {

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

• Теорема: утверждение о данных, которое проверяется

  теоремаtheorem имеетhas в данныхin data найти гдеfind where по морфизмуby morphism следовательноtherefore по законуunder law

      по закону «Отгружаем только подтверждённое складом»
    теорема «Заказ ЗК-7781 можно отгрузить»
      дано Заказ имеет «готов к отгрузке» равное да
      в данных заказы найти где номер равен «ЗК-7781»
      по морфизму «Готовый заказ можно отгрузить»

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

Процессы — состояние, надзор, прогон. Карточек: 5.

• Запас витков: с запасом … витков

  с запасомwith budget

    обрабатывает «разобрать пакет» с запасом 2000 витков

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

• План: продолжение, записанное значением

  планplan

  план «Сходить по ссылке»

  План — это программа, которая ЖДЁТ: читает файл, ходит в сеть, пишет ответ. Ни одна строка ниже ничего из этого не делает. Каждая строит ЗНАЧЕНИЕ, описывающее следующий ход, а исполняет его хозяин — среда, в которую модуль напечатан. Отсюда свойство, которое обычно теряется вместе с чистотой: функции плана ТОТАЛЬНЫ. Программа, ходящая в сеть, доказано завершается — потому что сеть в неё не входит. Завершается описание; ждёт хозяин. И потому же каждый ход проверяется обычным примером, без файлов и сокетов. Замыканий в языке нет, поэтому продолжение не спрятано, а названо: варианты «Хода» — это точки, в которых программа ждёт.

• Процесс: состояние, начальное значение, сообщения, обработчик

  процессprocess обрабатываетhandles состояниеstate

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

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

• Прогон: семя, входящие сообщения, ожидаемое состояние

  прогонrun семяseed

  прогон «два прибавления»
    семя 4172
  прогон «то же самое на другом семени»
    семя 99

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

• Надзор: стратегия на процесс и порог отказов

  надзорsupervision стратегияstrategy порог отказовfailure threshold

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

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