Система типов и то, чего в ней нет

Проверка типов живёт в flang/src/types.mjs — 2779 строк. Вход — AST из раздела 5 спецификации, выход — диагностики в формате ядра FTS и таблица сигнатур. Читать этот файл приятно: почти каждое решение объяснено вместе с отвергнутой альтернативой.

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

Почему здесь нет Хиндли — Милнера

Вопрос напрашивается: язык функциональный по духу, почему не классический вывод типов с унификацией? Ответ записан в шапке модуля, и обратите внимание на вставку в середине — её дописали, когда функции стали значениями:

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

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

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

Проверить легко:

тотальная функция «Пустой список без контекста»
  принимает н: число
  возвращает список числа
  пример «Пусто»
    дано н равно 1
    ожидается пустой список
  пустой список

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

Сообщения действительно получились человеческие. Ветви разного типа:

$ … если н больше 0 то 1 иначе "строка"
{"code":"FLANG_TYPE","message":"ветви «если» разных типов: число и строка"}

Какие типы есть

Тип := строка | число | признак | ничто
     | список Тип
     | «Имя объекта»          запись
     | «Имя типа»             сумма
     | «Имя типа» от Тип и Тип        параметрический тип
     | функция из Тип и Тип в Тип     тип функции

Последние две строки — новые, и о каждой ниже отдельный раздел. Скобки в позиции типа завёл полиморфизм («Возможно» от («Возможно» от числа)), и цена им оказалась нулевая: ( в позиции типа до того всегда было ошибкой разбора.

Скалярные псевдонимы нормализуются в одном месте — таблица SCALAR_ALIASES в types.mjs. Это нужно, потому что имена приходят из трёх источников: русской поверхности (число, строка, признак, ничто), английской (number, string, boolean, null) и моста из FTS (Число, Деньги, Строка, Дата, Признак). Деньги — это число, Дата — строка.

Есть и четвёртый случай, который стоит отметить отдельно, потому что он объясняет, зачем в системе типов вообще нужен джокер. FTS умеет описывать поля именами состояний — «Скоринг пройден». Это маркеры доказательств, а не значения; ядро FTS их не проверяет. Мост переводит их в unknown с сохранённым именем, и тайпчекер обязан их пропускать — иначе он отверг бы существующие модели, что запрещено обещанием совместимости.

Исчерпывающность разбора

Проверяется, и это одна из самых полезных вещей в языке:

тип «Цвет»
  вариант «Красный»
  вариант «Зелёный»
  вариант «Синий»

тотальная функция «Код цвета»
  принимает цвет: «Цвет»
  возвращает число
  разбор цвет
    случай «Красный»
      то 1
    случай «Зелёный»
      то 2

{"code":"FLANG_MATCH_NOT_EXHAUSTIVE","message":"разбор «Цвет» не покрывает «Синий»",
 "span":{"line":11,"column":5}}

Сообщение называет конкретный непокрытый вариант, а не факт неполноты. Есть и парный код FLANG_MATCH_UNREACHABLE — на недостижимый случай.

Главное решение развернулось: функции стали значениями

Здесь стояла самая уверенная формулировка всего трека:

Функции не являются значениями первого класса. Это осознанное ограничение, а не недоделка: без экспоненциалов остаётся выразимой генерация в языки без замыканий, а анализ завершаемости остаётся простым и предсказуемым.

За сутки это перестало быть правдой, и перестало не потому, что решение пересмотрели, а потому, что обе его причины удалось снять, не тронув ни одну из защищаемых ими вещей. Способ известен с 1972 года и называется дефункционализацией (Рейнольдс).

Идея простая. В языке функция становится значением, а компилятор перед печатью заменяет каждое такое значение тегом и одним диспетчером применить(тег, аргумент). Напечатанный код остаётся первопорядковым: в C это структура и switch, а не указатель на функцию с окружением.

Проверить можно за минуту. Программа из главы про синтаксис — «Применить дважды», принимающая ф: функция из числа в число, — печатается в C и собирается под -Werror -pedantic. Вот диспетчер из напечатанного файла, дословно:

fl_status vysshiy_poryadok_primenit_1(fl_ctx *ctx, fl_value teg, fl_value a1,
                                      fl_value *result, fl_error *error) {
  if (fl_variant_is(teg, "Удвоить")) {
    return vysshiy_poryadok_udvoit(ctx, a1, result, error);
  } else {
    return fl_match_fail(ctx, teg, error);
  }
}

Никаких замыканий, никакого боксинга окружений. Собранный бинарник отвечает:

$ echo '{"fn":"Применить дважды","args":[{"v":"Удвоить","f":[]},{"n":"5"}]}' | ./flang_cli
{"ok":true,"value":{"n":"20"}}

Почему это не сломало доказуемость завершения — главный пункт

Второй довод исходной формулировки был сильнее первого, и его стоит разобрать медленно.

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

Дефункционализация снимает ровно это: после неё граф вызовов конечен и известен целиком, потому что тег строится ровно одной формой и программа видна вся. Отсюда формулировка, которая стоит в flang/cat/HOF.md заголовком раздела и которую стоит запомнить: анализ не изменился ни на строку — изменилось то, чем он питается. Применение разворачивается в столько обычных рёбер f → g, сколько тегов может в это применение прийти.

Цена уплачена заранее и названа: дефункционализация требует видеть всю программу, а раздельной компиляции у языка нет и не планируется.

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

$ echo '{"fn":"Применить дважды","args":[{"v":"Чужой","f":[]},{"n":"5"}]}' | ./flang_cli
{"ok":false,"code":"FLANG_MATCH_NOT_EXHAUSTIVE","message":"разбор не покрывает значение Чужой"}

Список тегов у вычислителя и у анализа один и тот же — одно определение на оба слоя, flang/src/tags.mjs, 91 строка.

Чего у функций-значений всё-таки нет

Каррирования и частичного применения. Арность в flang — свойство функции, а не сахар над цепочкой одноместных, и это записано как решение «чего решено не делать никогда». Значит экспоненциал «Б»^«А» в языке появился как объект, но не как сопряжение, и декартово замкнутой категорией flang от этого не стал — контракт запрещает утверждать обратное.

Полиморфная функция значением не становится, и это отказ, а не пропуск:

{"code":"FLANG_TYPE_PARAM",
 "message":"функция «Обернуть» объявлена от 1 параметра и значением стать не может:
            у значения тип один, а у неё их столько, сколько подстановок"}

Встроенные формы отобразить / отфильтровать / свёртка, принимающие тело, а не функцию, при этом никуда не делись и остаются основным способом обхода:

отфильтровать элементы где эл → эл не равен значение

Параметрический полиморфизм: фаза первая

Второй разворот той же силы. Здесь стояло «самое дорогое из отсутствующего» — теперь это есть, и признание переписано в самом репозитории. Шапка flang/stdlib/optional.flang сегодня начинается так:

Здесь стояло: «типы не параметрические, «Есть» с полем любого типа записать нельзя». Про ЯЗЫК это больше не правда — проверено запуском.

тип «Возможно» от «А»
  вариант «Есть» содержит значение: «А»
  вариант «Ничего»

Одно объявление обслуживает и «Возможно» от числа, и «Возможно» от строки, и — что важнее всего — «Возможно» от («Возможно» от числа), то есть тот же тип, а не второй, написанный руками. Именно это делало монаду невыразимой: имена вариантов уникальны на модуль, поэтому без параметров M(M) был отдельным типом с другими конструкторами, а законы монады трогают M³.

Аргументы типа при вызове выводятся, а параметры при объявлении пишутся — и второе тоже решение: неявное правило «незнакомое имя типа считается параметром» превратило бы опечатку в принятую программу.

Полиморфизм не стоил печати ничего — и это измерение опрокинуло решение

Вот место, ради которого стоит читать flang/PLAN.md. Там стояло: полиморфизм печатается мономорфизацией, «Возможно» от «А» разворачивается в отдельный тип на каждое применение, потому что у C генериков нет.

Измерение это опровергло. Все восемь бэкендов типы уже стирают: сигнатуры везде fl_value / rt.Value / Value, а единственная функция в каждом бэкенде, которая вообще читает объявленный тип, печатает комментарий:

lines.push(` * @param ${idents[index]} — «${param.name}»${typeNote(param.type)}`)

Фабрика печатается одна на запись и одна на вариант, по имени, а не по подстановке. Значит «Возможно» от числа и «Возможно» от строки — это одна фабрика, а не две, и мономорфизация не нужна вовсе.

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

Урок автор формулирует сам, и он общий: «решение о печати принималось из общего соображения „у C нет генериков“, а надо было посмотреть, что бэкенды делают на самом деле».

Чего у полиморфизма ещё нет

Фаза первая — это разбор, типы, подстановка, вывод аргументов. Не сделано: примеры на полиморфных функциях, теоркат на параметрических типах и — главное — самоприменение. Правило до конца работы жёсткое и записано прямым текстом: ни одна программа репозитория, включая stdlib, не вправе использовать полиморфизм, пока self/ его не понимает.

Выяснилось это дорого: файл-пример с полиморфизмом уронил три теста неподвижной точки, причём расходились не flang₁ и flang₂, а эталон и flang₁ — на входе, которого раньше не было. То же правило и та же цена у функций-значений: модуль с ними, положенный в flang/stdlib/, роняет пять тестов.

Чего в системе типов нет

Раздел заметно похудел, и один пункт стоит проводить отдельно, потому что он ушёл тихо. Здесь стояло: псевдонимов типов нет — конструкция разбирается, но types.mjs раскладывает объявления только на суммы и записи, и псевдоним становится записью без полей. Проверяем:

тип «Строка счёта» это список числа

тотальная функция «Сколько»
  принимает позиции: «Строка счёта»
  возвращает число
  пример «Три позиции»
    дано позиции равно [1, 2, 3]
    ожидается 3
  разбор позиции
    случай пусто
      то 0
    случай голова и хвост
      то 1 плюс «Сколько» от хвоста

check даёт valid: true и total: true, test — 1 из 1. Работает. Причём псевдоним тоже параметрический и разворачивается с подстановкой.

Порядка на строках

больше и меньше для строк отвергаются на check:

{"code":"FLANG_TYPE","message":"левый операнд сравнения «gt» имеет тип строка:
 сравнения порядка допустимы только для чисел"}

Это делает невыразимой сортировку строк, и в списке невыразимых задач LeetCode так и записано (задача 179, Largest Number).

Отметим для точности: в index.json этот пункт описан иначе — как расхождение слоёв, где «types.mjs разрешает „больше“/„меньше“ для строк, а interpret.mjs на них бросает FLANG_TYPE», то есть программа проходит проверку и падает при запуске. На момент нашей проверки расхождения нет: отказ приходит на check, до запуска. Похоже, долг закрыли; сам пункт в index.json обновить не успели.

Обработки ошибок в типах

Тип не умеет сказать «эта функция может не справиться». Исключений в языке нет, отказ встроенной формы (к числу от "abc", голова от пустого списка) прекращает вычисление целиком и не перехватывается. Единственный способ — вернуть сумму типов вручную; так устроен flang/stdlib/result.flang:

тип «Результат числа»
  вариант «Успех» содержит значение: число
  вариант «Ошибка» содержит сообщение: строка

С важной оговоркой из шапки того же файла: «Проверка должна идти ДО опасной встроенной формы, а не после: обработать её отказ уже нельзя».

Как к этому относиться

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

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

И здесь стоит сказать вещь, которая важнее любого из двух разворотов выше. Полиморфизм и функции-значения в языке есть, а в библиотеке их по-прежнему нет — и разрыв этот не временное неудобство, а измеренное следствие устройства. Дублирование посчитано, а не оценено: девять функций stdlib отличаются друг от друга ровно одним подставленным предикатом или операцией, а ещё 55 функций из 202 в stdlib, examples/leetcode и examples/rosetta — побайтовые копии друг друга. Замена написана целиком: 36 функций, все тотальные, 55 примеров, печать во все восемь целей. Положить её на место нельзя — уронит самоприменение. Разбор — в главе «Стандартная библиотека».

Насколько это терпимо на большом объёме, стало понятнее с тех пор, как на flang написали восемнадцать тысяч строк: ядро FTS в flang/core/ (4573 строки) и компилятор самого языка в flang/self/ (13 640) (глава «Ядро FTS на flang»). Ответ оказался не «невыносимо», но и не «незаметно», и виден он в решении, которое там приняли: AST в этих файлах не типизирован. Узел дерева — это обобщённое «Значение» из core/json.flang, сумма «скаляр | список | запись», а не свой тип на каждый вид узла.

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

Дальше — глава «Тотальность», про самую нестандартную часть проверок.