Законы годятся указателем, а не выводом — но в стандартной библиотеке их объявлено ноль

Из замысла владельца про теоркат («выводить пакет по теоркату из библиотеки Борхеса») выполнима не та половина, что кажется. Вывести модуль из законов нельзя: законы не порождают код, они его отсеивают — это уже записано в category-theory-transports-truth («теоркат не пишет код»). Зато отсев — ровно то, чего не хватает поиску: подпись называет класс из двенадцати (a-signature-does-not-determine-a-function), и сузить его нечем.

Машинка для отсева в дереве уже есть, и она дешёвая. flang/src/monoid.mjs — 245 строк: ассоциативность, нейтральность, обратимость проверяются на конечной сетке значений, не больше 12 (ПРЕДЕЛ_СЕТКИ), а значения берутся из примеров самого автора, не из генератора. Законы функтора проверяются сличением объявлений (FLANG_FUNCTOR_SQUARE с контрпримером — module-links-need-a-named-data-translation), словарь между спеками — flang/src/compat.mjs, 560 строк (the-dictionary-between-specs-was-mute). Пять объявляемых свойств (flang/cat/ZAKONY.md) — идемпотентность, коммутативность, дистрибутивность, монотонность, частичный порядок — заведены каждое ради конкретного разрешения, а не ради полноты списка.

То есть спросить «дай модуль, у которого операция ассоциативна и есть единица» можно уже сегодня, механизмом проверки, который написан и работает.

И спрашивать не у кого. Вот число. Верхнеуровневых объявлений законов во всём дереве — 28: 6 моноидов, 6 категорий, 4 функтора, 12 свойств. Все 28 лежат в examples/ (в cat/ — 11, в cat/moduli/ — 4, в money/ и paths/ — по 1 из семи файлов). В flang/stdlib/ их ноль:

grep -c '^моноид\|^свойство\|^категория\|^функтор' flang/stdlib/*.flang
   → ни одного ненулевого

Указатель по законам, построенный сегодня, содержал бы 28 записей на 234 файла и 208 функций библиотеки — и ни одной записи о том, что кто-нибудь захочет искать. Для сравнения: теорем в дереве 80, то есть доказывать про функции у нас привыкли, а называть их свойства — нет.

Узкое место переехало, и это его третье место в проекте. Не «указателя нет» и не «проверять нечем» — проверять есть чем и указатель строится поверх готового. Не хватает входных данных: законов никто не пишет. Работа, которая даёт указатель, — это не индексатор, а 208 строк свойство/моноид в стандартной библиотеке.

И даже тогда отсев слабее, чем хочется. Самый естественный закон для класса строка → строка — идемпотентность. Разбор двенадцати функций класса по их собственным примерам: идемпотентны девять («В верхний регистр», «В нижний регистр», «Обрезать пробелы», «Обрезать слева», «Обрезать справа», «Заглавная буква», «Строчная буква», «Первый символ», «Последний символ»), не идемпотентны три — «Обратить строку» (ф(ф(х)) = х, другой закон), «Заглавная точка» ("раз" → "раз.", второй проход даёт "раз..") и «Ошибка разбора» ("3" → "", а "" → "это не цифра").

Значит ответ «идемпотентна» сужает класс с двенадцати до девяти — это 0,4 бита при нужных log₂ 12 ≈ 3,6 битах. Одним законом класс не разрешается; чтобы из двенадцати остался один, нужно около девяти таких вопросов. Словарь языка (5 свойств + моноид + функтор) даёт максимум семь, и то не все применимы к одноместной функции над строкой. Указатель по законам, стало быть, честно называется сужением, а не поиском: он превращает двенадцать кандидатов в девять, и последний выбор всё равно за человеком.

Снаружи это пробовали дважды, и оба раза остановились там же. Довод к указателю по законам придуман не нами: Заремски и Винг (FSE 1995) начинают ровно с нашего числа — «in the C math library nearly two-thirds of the functions (31 out of 47) have signature double → double» (pdf). Наши 36,5 % — то же наблюдение на своей библиотеке. Дальше у них случилось поучительное: работа про сопоставление подписей прижилась и разошлась, а работа про сопоставление спецификаций осталась шестью запросами на стеке и очереди, и в ней написано, что «some of the proofs require user assistance». Диагноз поставлен позже, в Yogo (PLDI 2020): «Rollins and Wing assume a world in which every function comes equipped with a logical specification» (pdf). Мира такого нет — и у нас его нет тоже, ровно на ноль объявлений в stdlib.

Вторая половина, добыча законов, тоже упирается в стену, и рано: QuickSpec называет свою область работы прямо — «a good starting point seems to be a signature consisting of up to 10 functions», размер терма 7–9 (pdf); 33 функции над списками при размере 7 — 42 минуты, 398 законов, 50 000 термов, 874 000 проверок; при размере 8 — нехватка памяти и срыв двухчасового предела. Сами авторы советуют «up to 10 functions» и признают, что на 33 функциях выходит мусор вроде zip (map f xs ++ ys) xs = zip (map f xs) xs. SPYRO (OOPSLA 2023) выводит наиболее точную алгебраическую спеку для модулей в 1–14 функций (самый большой — 140 строк), решая 41 задачу из 45, и тратит на это от минут до получаса — по упрощённым реализациям, а не по настоящим.

Указателя пакетов по законам не построил никто и никогда. Даже в Mathlib — 1,9 миллиона строк формализованных законов, единственный корпус, где законы действительно написаны, — работающий поиск (Loogle, exact?) остаётся сопоставлением образцов по дереву различения, а не поиском по законам.

И одно наблюдение, которое стоит знать прежде, чем строить такой указатель. В опросе 151 программиста на Haskell 121 из 121 пользователей Hoogle назвали поиск по типу тем, ради чего они им пользуются. Когда тем же людям дали Hoogle+ и посадили за задачи, из 115 запросов по типу были только 22 — «across the board, users searched by type the least» (pdf). Заявленная нужда и настоящая — разные величины.

Чем подтверждено. Счёт на /srv/flang-rabota/packages, ветка work/packages-research, 2026-08-18: grep -rh '^моноид' flang --include='*.flang' и то же для свойство, категория, функтор, теорема дают 6, 12, 6, 4, 80; grep -rl по тем же образцам даёт только пути внутри examples/. Размеры проверяльщиков — wc -l flang/src/monoid.mjs flang/src/compat.mjs = 245 и 560. Предел сетки — константа ПРЕДЕЛ_СЕТКИ = 12 в flang/src/monoid.mjs.

Чем ограничено.

• Отсев по закону — опровержение, а не подтверждение. Сетка конечна и собрана из примеров автора; «прошло сетку» не значит «закон держится». Указатель по законам поэтому даёт кандидатов, а не ответ, и это его природа, а не недоделка. Тот же предел уже записан в module-links-need-a-named-data-translation: вырожденная сетка подтверждает саму себя.
• Разбор «девять к трём» сделан по примерам в исходнике, а не прогоном. Первый счёт был неверен — вышло «одиннадцать к одному», потому что «Заглавная точка» и «Ошибка разбора» посчитались идемпотентными не глядя. Проверка примеров это сняла, и ошибка записана, а не стёрта: закон надо прогонять, а не угадывать. Настоящий замер — отдельная работа: объявить свойство «идемпотентность» у функций strings.flang и дать проверить компилятору.
• Указателя по законам нет ни строки. Здесь измерено только то, что для него готово и чего не хватает.
• Внешние числа взяты из чужих работ, а не проверены здесь. Отрицательное утверждение «указателя по законам не построил никто» — это «не нашли» при исчерпанном бюджете поиска, а не доказанное отсутствие.
• Два числа держатся на одном источнике каждое, и это надо знать. «31 из 47 подписей double → double» и опыт с Hoogle+ (121 из 121 против 22 из 115) добыты одним разбором; второй, независимый, до них не дошёл и потому их не подтверждает и не опровергает. Цена SPYRO разошлась между двумя разборами (900 против 1732 секунд на самой тяжёлой задаче), поэтому здесь она названа вилкой, а не числом.

Связано: a-signature-does-not-determine-a-function, category-theory-transports-truth, module-links-need-a-named-data-translation, the-dictionary-between-specs-was-mute, the-bottleneck-is-rule-strength, code-cannot-be-derived-from-its-hash, derivation-works-where-the-domain-was-narrowed-on-purpose, synthesis-from-a-spec-hits-75-tree-nodes