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

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

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

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

Функции в flang не являются значениями первого класса (SPEC, раздел 3), поэтому единственные места, где тип действительно неизвестен, — это локальное пусть, элемент списка, накопитель свёртки и пустой список. Всё остальное задано объявленной сигнатурой. Унификация с переменными типов дала бы ту же силу вывода, но сообщения об ошибках стали бы говорить о «t7 против t12» вместо «ветви „если“ разных типов» — для языка, где типы объявляются, это чистый проигрыш.

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

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

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

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

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

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

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

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

Это раздел 3 спецификации, за вычетом строки Тип → Тип, о которой ниже.

Скалярные псевдонимы нормализуются в одном месте — таблица 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 — на недостижимый случай.

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

В таблице типов спецификации есть строка Тип → Тип, и рядом с ней — уточнение: «функция (только как объявление, не значение)». Дальше идёт формулировка, которую стоит привести целиком:

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

Два следствия названы прямо, и оба подтверждаются кодом.

Кодогенерация. Печать в C — это flang/src/emit/c.mjs, C99 без замыканий. Если бы функция была значением, пришлось бы печатать окружения, боксинг и управление их временем жизни. Без экспоненциалов вызов печатается вызовом.

Анализ завершаемости. flang/src/totality.mjs отслеживает происхождение каждого значения — «частью какого параметра оно является и насколько глубоко разобранной частью». Функция-значение сделала бы это отслеживание межпроцедурным и, скорее всего, неразрешимым на практике.

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

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

Работает, читается неплохо. Но: собственную функцию высшего порядка вы не напишете, а значит и не абстрагируете повторяющийся обход.

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

Параметрического полиморфизма

Это самое дорогое из отсутствующего. Признание — прямо в шапке flang/stdlib/lists.flang:

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

Практически это значит, что «Обратить» для список числа и для список строки — две функции с одинаковым телом. И хуже: опциональное значение приходится заводить отдельно под каждый тип, потому что имена вариантов обязаны быть уникальны в модуле. flang/stdlib/optional.flang устроен как «Число или ничто» именно поэтому, и в комментарии написано: «Для строк пришлось бы завести второй тип с другими именами вариантов».

Псевдонимов типов

Спецификация показывает тип «Строка счёта» это список «Позиция», и лексер знает ключевое слово alias: ["это"]. Но в списке недостающего (flang/examples/leetcode/index.json) записано, что конструкция разбирается в узел alias, а types.mjs раскладывает объявления только на суммы и записи — и псевдоним становится записью без полей. Пользоваться псевдонимами нельзя. В корпусе .flang-файлов их и нет ни одного.

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

больше и меньше для строк отвергаются на 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, это разумный размен: чем меньше в типах выразительности, тем меньше мест, где два слоя могут разойтись.

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

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