Связь двух модулей становится проверяемой ровно тогда, когда назван перевод данных

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

перевести и сделать = сделать и перевести

По-деловому это «отменённый заказ отменён везде». Формально — закон естественности перевода.

Чем подтверждено. Ветка work/moduli-kak-obekty, коммиты cbbd42e, 7ff6895, ca7debd. Пример examples/cat/modules/ — четыре файла, три модуля и связи между ними. Три порчи сняты прогоном, и каждая ломает сборку:

1. перевод забыл перенести поле (возвращён равным 0 вместо возвращён равным заказ.отменён) — FLANG_FUNCTOR_SQUARE с контрпримером: на {"сумма":500,"отменён":0} один путь дал возвращён 0, другой — 1;
2. в модуль добавлена стрелка, а связи про неё не сказали — FLANG_FUNCTOR_NOT_TOTAL у обеих связей сразу;
3. минус 100 вместо минус 10000 — единицы забыты один раз, опять квадрат.

Во всех трёх случаях каждая функция по отдельности тотальна, типы сходятся, свои примеры зелёные. Ни одна другая проверка дерева этого не видит.

Записи для этого хватило старой: объект «А» отображается в «Б» даёт «Ф». Новых слов ноль — форма прежде отвергалась разбором, и заняла она то, что было ошибкой. Тот же приём, каким категория получила список своих стрелок.

Побочная находка, и она важнее, чем кажется. Проверка полноты связи существовала и работала — но только внутри одного файла. Связывание модулей не переносило categories, и те же строки, разложенные по трём модулям через использует, давали valid: true при нуле диагностик. То есть проверка не работала ровно там, где она и нужна. Это второй случай того же класса: теоремы через импорт тоже не переезжают. Отсюда правило: проверка, зелёная в одном файле, не считается работающей, пока её не прогнали через границу модуля.

Чем ограничено. Слой проверяет структурную согласованность, а не деловую правильность. Он скажет «новое требование противоречит существующему переводу»; он не скажет «требование плохое». Кроме того:

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

Связано: category-theory-transports-truth, natural-transformation-catches-what-nothing-else-does, proven-is-not-correct, checks-that-stopped-comparing, a-removal-must-turn-a-test-red, names-not-hashes