Ментальная модель: данные, правила, вывод и эффект

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

Эта глава задаёт словарь на весь курс: как читать .fts-файл, не путая четыре разных вещи, которые в обычном коде обычно свалены в один метод. Если это разделение усвоено, дальнейшие главы — просто новый синтаксис для тех же четырёх слоёв.

Минимальный пример

категория «Исполнение заказа»

  объект Заказ
    номер является строкой
    клиент является строкой
    оплачен является признаком
    «склад подтвердил» является признаком
    «готов к отгрузке» является состоянием «Готов к отгрузке»

  морфизм «Готовый заказ можно отгрузить»
    если «Готов к отгрузке»
    то «Отгрузить заказ разрешено»

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

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

Что делает компилятор

compile(source) строит один канонический FtsDocument — плоский JSON с полями category, structures, functors, proposition, utilities. validate(document) проверяет, что имена не дублируются, поля объектов существуют, а домен и кодомен каждого морфизма — реальные типы свидетельств. Дальше расходятся три пути: prove строит человекочитаемый вывод из proposition и, если дан JSON-контекст, сверяет witness с реальными данными; certify/verify делают то же самое, но с SHA-256 digest’ами для независимой проверки; testUtilities выполняет пример-блоки внутри утилита как исполняемые тесты. Ни один из этих шагов не читает файл сам — источник и контекст всегда передаются явно, аргументом.

Четыре слоя

Данные. объект и структура описывают наблюдаемую форму входа: набор именованных полей с типом. Методов, конструкторов и скрытого состояния нет — это не класс.

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

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

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

Граница эффекта проведена не потому, что в языке чего-то не хватает, а намеренно: FTS не имеет примитивов HTTP, SQL, транзакций, времени и случайности, поэтому один и тот же .fts-файл даёт одинаковый результат в браузере, в Node.js и в тесте CI. Решение о том, когда именно результат превращается в реальное действие — это архитектурное решение приложения, а не языка. FTS не знает про retry, идемпотентность или очередь сообщений; это работа кода, который получает его результат.

Морфизм и утилита — два разных вида правил

морфизм «Готовый заказ можно отгрузить»
  если «Готов к отгрузке»
  то «Отгрузить заказ разрешено»

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

Утилита отличается от обычной функции в коде тремя вещами. Во-первых, у неё обязателен явный начинает с — нет неявного undefined или null в начале вычисления. Во-вторых, правила внутри неё — это не if / else if с побочными эффектами, а именованный список: выполняются все правила, чьи условия истинны, и порядок влияет только на то, в каком порядке складываются значения. В-третьих, утилита физически не может дёрнуть сеть или файл — в её грамматике просто нет для этого конструкции. TypeScript-функция может сделать всё перечисленное, и именно поэтому она не заменяет утилиту как источник правды: скомпилированный .fts гарантирует то, что обычная функция гарантирует только дисциплиной команды.

Три уровня уверенности

• fts check доказывает только структурную и типовую корректность модели.
• fts test показывает, что исполняемые примеры утилиты совпадают с текущей семантикой.
• fts verify независимо пересчитывает сертификат и проверяет, что каждый witness разрешился в конкретном JSON-контексте.

Ни один уровень не делает внешний бизнес-закон истинным «из воздуха». Если команда объявила морфизм «успешная проверка разрешает выплату», FTS проверит его правильное применение и покажет закон явной предпосылкой в сертификате (assumptions), но основание этого закона — политика, договор или исследование, а не компилятор.

Практика в песочнице

Найдите в выводе assumptions и steps: какая строка — данные, какая — применённый морфизм, какая — итоговый вывод. Затем откройте diagram того же файла и сверьте с текстовым выводом.

Добавьте шестой пример с суммой ровно 10000 и без постоянного клиента. Посчитайте ожидаемый результат вручную по правилу «Большая покупка» и добейтесь 6/6 примеров.

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

Типичные ошибки

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

FTS_WITNESS_MISMATCH — заявленное в дано значение не совпало с реальными данными по указанному пути. Для примера выше, если у заказа «готов к отгрузке» на самом деле нет, prove вернёт: witness does not match context at заказы[номер="ЗК-7781"].готов к отгрузке: expected true, got false. Это не ошибка синтаксиса — модель корректна, но факт в контексте другой. Правка — исправить либо данные, либо условие теоремы; убедительность текста правила на это не влияет.

Чек-лист

• Я могу разложить любое правило своей системы на данные, правило, вывод и эффект — по отдельности.
• Я понимаю разницу между морфизм (допустимый переход) и правило утилиты (вычисление числа).
• Я знаю, что fts check, fts test и fts verify доказывают разные вещи и не заменяют друг друга.
• Я объясняю, почему граница эффекта — решение приложения, а не языка.

Кейсы каталога по этой теме

Дальше: установка и JSON