Теоркат, шаг 2: функтор перестал быть словом без гарантии

Объявление функтора в языке было и раньше: `функтор «Ф» из «A» в «B»` с блоком
отображений разбирался и укладывался в дерево. Проверки за ним не стояло
никакой — можно было написать это слово и получить ровно ничего, кроме слова.
Курс, кстати, на эту ловушку и наткнулся: файл с функтором проходил `check` с
ответом valid, и это легко принять за реализацию.

Теперь проверяются три закона, и все три ДОКАЗЫВАЮТСЯ, а не проверяются на
сетке:

  1. согласование стрелки с объектами: если «ф» ведёт из «A» в «B», её образ
     обязан вести из образа «A» в образ «B»;
  2. сохранение композиции: образ композиции обязан быть композицией образов в
     том же порядке — и обязан быть объявлен именно композицией, а не стрелкой
     с теми же концами;
  3. сохранение единиц: образ тождественного морфизма объекта — тождественный
     морфизм его образа.

Плюс однозначность отображения объектов: второй образ у того же объекта — это
ошибка, а не победа последней строки.

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

ЗАКОНЫ НЕ ВКЛЮЧАЮТСЯ ПО ЖЕЛАНИЮ. В контракте стояла строка `сохраняет
композицию` — отдельное разрешение на проверку. Не сделана намеренно:
отображение, не сохраняющее композицию, функтором не является, и позволить
написать это слово без закона значило бы продать имя вместо содержания.

Граница честности закреплена тестом: имена категорий («из «Продажи» в
«Биллинг»») остаются пометкой для читателя. Категория отдельной сущностью не
объявляется, и утверждать, что объект принадлежит именно ей, не на чем. Тест
с выдуманными категориями обязан проходить — если когда-нибудь перестанет,
значит появилась проверка, и обещание в документации надо переписать.

Проверено: 10 тестов законов функтора, 1434 теста языка целиком, 0 падений.

Author: Marat Zimnurov

flang/src/types.mjs

@@ -113,6 +113,7 @@ export function checkTypes(program) {
   }
 
   checkMorphisms(program, ctx)
+  checkFunctors(program, ctx)
 
   return { ok: diagnostics.length === 0, diagnostics, types: ctx.signatures }
 }
@@ -207,6 +208,170 @@ function checkMorphisms(program, ctx) {
   ctx.morphisms = стрелки
 }
 
+/**
+ * Функтор: отображение объектов и стрелок, обязанное сохранять устройство.
+ *
+ * Объявление функтора в языке было и раньше — `функтор «Ф» из «A» в «B»` с
+ * блоком `объект … отображается в …` и `морфизм … отображается в морфизм …`.
+ * Не было проверки: слово «функтор» стояло, а гарантии за ним не стояло
+ * никакой. Здесь появляется гарантия.
+ *
+ * ЗАКОНЫ НЕ ВКЛЮЧАЮТСЯ ПО ЖЕЛАНИЮ. В контракте была строка `сохраняет
+ * композицию` — отдельное разрешение на проверку. Она не сделана намеренно:
+ * отображение, не сохраняющее композицию, функтором не является, и дать
+ * написать это слово без закона значило бы продать имя вместо содержания.
+ *
+ * ЧТО ИМЕННО ДОКАЗЫВАЕТСЯ, а не проверяется на примерах. Всё нижеследующее —
+ * утверждения обо всех входах, и берутся они из одних объявлений, без сетки и
+ * без решателя. Это возможно ровно потому, что морфизм здесь объявление, а не
+ * значение: у функций первого класса такой проверки не бывает.
+ *
+ *   1. согласование стрелки с объектами: если «ф» ведёт из «A» в «B», то её
+ *      образ обязан вести из образа «A» в образ «B». Ровно та же стыковка, что
+ *      у композиции, только через отображение;
+ *   2. сохранение композиции: образ композиции обязан быть композицией образов
+ *      в том же порядке;
+ *   3. сохранение единиц: образ тождественного морфизма объекта обязан быть
+ *      тождественным морфизмом его образа;
+ *   4. отображение объектов однозначно — иначе это не функция.
+ *
+ * Чего проверка НЕ делает и делать не может: имена категорий («из «Продажи» в
+ * «Биллинг»») остаются пометкой для читателя. Категория в языке не объявляется
+ * отдельной сущностью, и утверждать, что объект принадлежит именно этой
+ * категории, не на чем.
+ */
+function checkFunctors(program, ctx) {
+  const наследие = Array.isArray(program?.legacy) ? program.legacy : []
+  const функторы = наследие.filter((узел) => узел?.construct === "functorFile")
+  if (функторы.length === 0) return
+
+  const стрелки = ctx.morphisms instanceof Map ? ctx.morphisms : new Map()
+  const морфизмы = Array.isArray(program?.morphisms) ? program.morphisms : []
+  /* Композиции берутся из исходных узлов, а не из `стрелки`: там от композиции
+     остались только домен и кодомен, а закону нужны имена сомножителей. */
+  const композиции = new Map()
+  for (const узел of морфизмы) {
+    if (узел?.kind === "composition") композиции.set(узел.name, узел)
+  }
+  const единицы = new Map()
+  for (const узел of морфизмы) {
+    if (узел?.kind === "morphism" && узел.identity === true) единицы.set(узел.name, узел.domain)
+  }
+
+  for (const { value: функтор, span } of функторы) {
+    const узел = { span }
+    const образОбъекта = new Map()
+    for (const пара of функтор.objects ?? []) {
+      if (образОбъекта.has(пара.from)) {
+        ctx.report(
+          "FLANG_FUNCTOR_OBJECT_TWICE",
+          `функтор «${функтор.name}»: объект «${пара.from}» отображается дважды — ` +
+            `в «${образОбъекта.get(пара.from)}» и в «${пара.to}»; отображение объектов обязано быть однозначным`,
+          узел,
+        )
+        continue
+      }
+      образОбъекта.set(пара.from, пара.to)
+    }
+
+    const образМорфизма = new Map()
+    for (const пара of функтор.morphisms ?? []) образМорфизма.set(пара.from, пара.to)
+
+    /* Закон 1: стрелка согласована с объектами. */
+    for (const пара of функтор.morphisms ?? []) {
+      const исходная = стрелки.get(пара.from)
+      const образ = стрелки.get(пара.to)
+      if (исходная === undefined) {
+        ctx.report(
+          "FLANG_UNKNOWN_NAME",
+          `функтор «${функтор.name}» отображает «${пара.from}», но такого морфизма нет`,
+          узел,
+        )
+        continue
+      }
+      if (образ === undefined) {
+        ctx.report(
+          "FLANG_UNKNOWN_NAME",
+          `функтор «${функтор.name}» отображает «${пара.from}» в «${пара.to}», но морфизма «${пара.to}» нет`,
+          узел,
+        )
+        continue
+      }
+      for (const [роль, конец] of [["домен", "domain"], ["кодомен", "codomain"]]) {
+        const объект = исходная[конец]
+        if (!образОбъекта.has(объект)) {
+          ctx.report(
+            "FLANG_FUNCTOR_OBJECT_MISSING",
+            `функтор «${функтор.name}» отображает морфизм «${пара.from}», но не отображает его ${роль} ` +
+              `«${объект}»: без образа объекта образ стрелки не с чем согласовать`,
+            узел,
+          )
+          continue
+        }
+        const ожидается = образОбъекта.get(объект)
+        if (образ[конец] !== ожидается) {
+          ctx.report(
+            "FLANG_FUNCTOR_ARROW_MISMATCH",
+            `функтор «${функтор.name}»: «${пара.from}» имеет ${роль} «${объект}», его образ — «${ожидается}», ` +
+              `но «${пара.to}» имеет ${роль} «${образ[конец]}»`,
+            узел,
+          )
+        }
+      }
+    }
+
+    /* Закон 2: образ композиции — композиция образов, в том же порядке. */
+    for (const [имя, композиция] of композиции) {
+      if (!образМорфизма.has(имя)) continue
+      const образЛевой = образМорфизма.get(композиция.left)
+      const образПравой = образМорфизма.get(композиция.right)
+      if (образЛевой === undefined || образПравой === undefined) {
+        const без = образЛевой === undefined ? композиция.left : композиция.right
+        ctx.report(
+          "FLANG_FUNCTOR_COMPOSITION",
+          `функтор «${функтор.name}» отображает композицию «${имя}», но не отображает «${без}», ` +
+            `из которой она собрана: закон сохранения композиции проверить не на чем`,
+          узел,
+        )
+        continue
+      }
+      const образКомпозиции = композиции.get(образМорфизма.get(имя))
+      if (образКомпозиции === undefined) {
+        ctx.report(
+          "FLANG_FUNCTOR_COMPOSITION",
+          `функтор «${функтор.name}»: образ композиции «${имя}» — «${образМорфизма.get(имя)}» — сам композицией не объявлен, ` +
+            `а обязан быть «${образЛевой}» после «${образПравой}»`,
+          узел,
+        )
+        continue
+      }
+      if (образКомпозиции.left !== образЛевой || образКомпозиции.right !== образПравой) {
+        ctx.report(
+          "FLANG_FUNCTOR_COMPOSITION",
+          `функтор «${функтор.name}» не сохраняет композицию: образ «${имя}» обязан быть ` +
+            `«${образЛевой}» после «${образПравой}», а объявлен как «${образКомпозиции.left}» после «${образКомпозиции.right}»`,
+          узел,
+        )
+      }
+    }
+
+    /* Закон 3: образ единицы — единица образа. */
+    for (const [имя, объект] of единицы) {
+      if (!образМорфизма.has(имя)) continue
+      if (!образОбъекта.has(объект)) continue
+      const ожидается = `единица ${образОбъекта.get(объект)}`
+      if (образМорфизма.get(имя) !== ожидается) {
+        ctx.report(
+          "FLANG_FUNCTOR_IDENTITY",
+          `функтор «${функтор.name}» не сохраняет единицы: образ «${имя}» обязан быть «${ожидается}», ` +
+            `а объявлен «${образМорфизма.get(имя)}»`,
+          узел,
+        )
+      }
+    }
+  }
+}
+
 /* ------------------------------------------------------------------ */
 /* Объявления                                                          */
 /* ------------------------------------------------------------------ */