Система типов и то, чего в ней нет
Проверка типов flang написана на самом flang: flang/self/types.flang в
репозитории языка, 7638 строк в выпуске 0.7.29. Вход — разобранная
программа, выход — диагностики с кодом, файлом, строкой и столбцом. Все примеры
ниже прогнаны командой flang check (и flang test, где есть примеры) на
flang 0.7.29.
Почему здесь нет Хиндли — Милнера
Язык функциональный по духу, но классического вывода типов с унификацией в нём
нет. Причина практическая: у каждой функции тип объявлен — принимает и
возвращает пишутся в заголовке. Неизвестен тип только у локального пусть,
элемента списка, накопителя свёртки и пустого списка. Для этих мест хватает
двунаправленной проверки: ожидаемый тип течёт сверху вниз и решает
единственный по-настоящему неоднозначный случай — пустой список. пустой список в контексте список числа получает тип список числа:
модуль «Пустой список»
тотальная функция «Пустой список без контекста»
принимает н: число
возвращает список числа
пример «Пусто»
дано н равно 1
ожидается пустой список
пустой списокОбъявленный возвращаемый тип и есть тот контекст, которого не хватало. Выигрыш от отказа от унификации — в сообщениях: вместо «t7 против t12» flang говорит словами, что не сошлось. Ветви разного типа:
модуль «Ветви»
тотальная функция «Ветви»
принимает н: число
возвращает число
если н больше 0 то 1 иначе "строка"$ flang check ветви.flang
FLANG_TYPE в файле ветви.flang, строка 6, столбец 3: ветви «если» разных типов: неотрицательное и строка
Литерал 1 получил самый узкий числовой тип, неотрицательное (о числовых
типах ниже).
Какие типы есть
Грамматика типа из docs/flang/SPEC.md, раздел 3:
Тип := строка | число | признак | ничто
| неотрицательное | целое | вес | сотых | тысячных уточнения числа
| точное целое | точное дробное точные числа без округления
| деньги | дата поверхность наследия: сводятся к числу и строке
| список Тип
| «Имя объекта» запись
| «Имя типа» сумма
| «Имя типа» от Тип и Тип применение параметрического типа
| «Имя параметра» параметр типа внутри своего объявления
| ( Тип ) скобки
| функция из Тип и Тип в Тип тип функции (она же — значение)
| Тип → Тип он же, стрелочной записью
деньги и дата остались от ранней поверхности: параметр а: деньги
принимает число, д: дата — строку.
Числа
Числовых типов несколько, и выбор меняет то, что компилятор докажет
(таблица законов по каждому — docs/number-kinds.md в репозитории языка):
| тип | что это |
|---|---|
число |
IEEE-754 double |
неотрицательное |
целое из [0, 2⁵³−1] |
целое |
целое из [−(2⁵³−1), 2⁵³−1] |
сотых, тысячных |
целое число сотых или тысячных долей, не меньше нуля |
точное целое |
неотрицательное целое без потолка 2⁵³: список разрядов по основанию 2²², младший первым |
точное дробное |
неотрицательная дробь: пара точных целых, всегда сокращённая |
Уточнения числа (неотрицательное, целое, сотых) сужают то, что функция
принимает: пример с 0.1 для параметра типа сотых отвергается — «0.1 не
целое, а тип сотых — целый». Арифметика над ними даёт обычное число: функция,
которая принимает а: сотых, б: сотых и считает а плюс б, обязана объявить
возвращает число.
Точные типы — отдельные виды значений. Сумма 0.1 + 0.2 + 0.3 над double
зависит от расстановки скобок, над точное дробное — нет:
модуль «Точные числа»
тотальная функция «Сумма»
принимает а: точное дробное, б: точное дробное
возвращает точное дробное
а плюс б
тотальная функция «Слева направо»
возвращает точное дробное
пример «над double здесь 0.6000000000000001»
ожидается [[3], [5]]
«Сумма» от («Сумма» от [[1], [10]] и [[1], [5]]) и [[3], [10]]
тотальная функция «Справа налево»
возвращает точное дробное
пример «над double здесь 0.6»
ожидается [[3], [5]]
«Сумма» от [[1], [10]] и («Сумма» от [[1], [5]] и [[3], [10]])
тотальная функция «Сумма точных»
принимает а: точное целое, б: точное целое
возвращает точное целое
пример «2⁵³ + 1 плюс 1 равно 2⁵³ + 2»
дано а равно [1, 0, 512]
дано б равно [1]
ожидается [2, 0, 512]
а плюс бflang test даёт «примеров 3, прошло 3». Литерал [[1], [10]] — одна
десятая; дробью его делает ожидаемый тип. Точные типы не смешиваются ни с
число, ни друг с другом без явного перевода (FLANG_TYPE), и знака у них нет:
[1] минус [2] останавливает вычисление сообщением «точное целое ниже нуля
значений не имеет: [1] минус [2]; молчаливый ноль запрещён». Длинные целые и
дроби со знаком есть в библиотеке — модули «Bignum» и «Rationals».
Исчерпывающность разбора
Проверяется, и это одна из самых полезных вещей в языке:
модуль «Цвета»
тип «Цвет»
вариант «Красный»
вариант «Зелёный»
вариант «Синий»
тотальная функция «Код цвета»
принимает цвет: «Цвет»
возвращает число
разбор цвет
случай «Красный»
то 1
случай «Зелёный»
то 2$ flang check цвет.flang
FLANG_MATCH_NOT_EXHAUSTIVE в файле цвет.flang, строка 11, столбец 3: разбор «Цвет» не покрывает «Синий»
Сообщение называет конкретный непокрытый вариант, а не факт неполноты. Есть и
парный код FLANG_MATCH_UNREACHABLE — на недостижимый случай.
Функции как значения
Функция — значение: тип функция из числа в число (или число → число),
значение функция «Удвоить», применение ф от х. Программа из главы про
синтаксис — «Применить дважды», принимающая ф: функция из числа в число, —
проходит check, и все три её функции остаются тотальными.
Замыканий при этом нет. Значение-функция — это тег, имя объявленной
функции, а перед выводом кода компилятор одним проходом заменяет каждое
применение вызовом диспетчера применить(тег, аргумент) — снятие
функций-значений (Рейнольдс, 1972; flang/self/defunc.flang). Код на выходе
остаётся первого порядка. Вот диспетчер из C, который выводит
flang emit … --target c для этой программы:
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);
}
}
Собранная программа (make в каталоге вывода) отвечает:
$ echo '{"fn":"Применить дважды","args":[{"v":"Удвоить","f":[]},{"n":"5"}]}' | ./flang_cli
{"ok":true,"value":{"n":"20"}}
Почему это не сломало доказательство завершения
При настоящем высшем порядке «кто кого зовёт» неразрешимо: значение-функция,
пришедшее неизвестно откуда, делает граф вызовов неизвестным, и анализ
убывания перестаёт работать. После снятия функций-значений граф конечен и
известен целиком: тег строится только формой функция «Имя», и программа видна
вся. Применение разворачивается в столько обычных рёбер графа вызовов, сколько
тегов может в него прийти.
Цена названа в спецификации: снятию нужна вся программа, раздельной компиляции у языка нет. Отсюда и правило при запуске — применить можно только тег, который программа где-то строит. Чужой тег отвергается:
$ echo '{"fn":"Применить дважды","args":[{"v":"Чужой","f":[]},{"n":"5"}]}' | ./flang_cli
{"ok":false,"code":"FLANG_MATCH_NOT_EXHAUSTIVE","message":"разбор не покрывает значение Чужой"}
Чего у функций-значений нет
Лямбд, каррирования и частичного применения. Арность — свойство функции, и
«Применить» от («Сложить» от 1) и х при двухместной «Сложить» не собирается:
$ flang check карри.flang
FLANG_TYPE в файле карри.flang, строка 16, столбец 19: функция «Сложить» принимает 2 арг. («а», «б»), а вызвана с 1
FLANG_TYPE в файле карри.flang, строка 16, столбец 19: аргумент «ф» функции «Применить»: ожидался функция из числа в число, получен число
Полиморфная функция значением не становится:
FLANG_TYPE_PARAM в файле обернуть.flang, строка 20, столбец 18: функция «Обернуть» объявлена от 1 параметра и значением стать не может: у значения тип один, а у неё их столько, сколько подстановок
Встроенные формы отобразить / отфильтровать / свёртка принимают тело,
а не функцию, и остаются основным способом обхода:
отфильтровать элементы где эл → эл не равен значениеДля тех, кому нужна функция аргументом, в библиотеке есть модуль «Higher order»: «Свернуть», «Отобразить», «Отфильтровать», «Сортировать по», «Составить».
Параметрический полиморфизм
тип «Возможно» от «А»
вариант «Есть» содержит значение: «А»
вариант «Нет»Это начало модуля «Optional» из библиотеки. Одно объявление обслуживает и
«Возможно» от числа, и «Возможно» от строки, и «Возможно» от («Возможно» от числа) — это тот же тип, а не второй, написанный руками.
Аргументы типа при вызове выводятся, а параметры при объявлении
пишутся: тотальная функция «Обернуть» от «А». Неявное правило «незнакомое
имя типа считается параметром» превратило бы опечатку в принятую программу.
Библиотека пользуется этим сама: «Длина», «Обратить» и «Приписать в начало» в
«Lists» объявлены от «А», «Результат» в «Result» — сумма от двух параметров.
Код на выходе от полиморфизма не толстеет: типы при выводе стираются (в C все
значения — fl_value, как в диспетчере выше), и одно объявление даёт один
конструктор на вариант, а не копию на каждую подстановку.
Псевдонимы типов
модуль «Псевдоним»
тип «Строка счёта» это список числа
тотальная функция «Сколько»
принимает позиции: «Строка счёта»
возвращает число
пример «Три позиции»
дано позиции равно [1, 2, 3]
ожидается 3
разбор позиции
случай пусто
то 0
случай голова и хвост
то 1 плюс «Сколько» от хвостаcheck подтверждает завершение, test даёт «примеров 1, прошло 1».
Чего в системе типов нет
Порядка на строках у операторов
больше и меньше для строк отвергаются на check:
модуль «Строки»
тотальная функция «Раньше»
принимает а: строка, б: строка
возвращает признак
а больше б$ flang check строки.flang
FLANG_TYPE в файле строки.flang, строка 6, столбец 3: левый операнд сравнения «gt» имеет тип строка: сравнения порядка допустимы только для чисел
FLANG_TYPE в файле строки.flang, строка 6, столбец 12: правый операнд сравнения «gt» имеет тип строка: сравнения порядка допустимы только для чисел
Сравнивать строки можно функцией: «Строка раньше» из модуля «Tree map»
библиотеки сравнивает их по кодам символов (код символа).
Исключений
Исключений и перехвата в языке нет, и спецификация обещает, что не будет:
перехват — это прыжок по стеку, а в выведенном C прыгать нечем. Отказ
встроенной формы (к числу от "abc", голова от пустого списка)
останавливает вычисление целиком. Функция «Число из текста» с телом
к числу текст:
$ flang run отказ.flang --function "«Число из текста»" --args '{"текст":"abc"}'
доказано: утверждений 0
FLANG_BUILTIN_ARGS: «к числу»: строка "abc" не является числом
Вместо этого у языка три средства, и все они видны в типах.
Отказ значением. У самой частой опасной формы есть двойник, который отказать
не может: к числу или беда возвращает вариант «Разобрано» или «Не разобрано»:
модуль «Ошибки»
тотальная функция «Число или ноль»
принимает текст: строка
возвращает число
пример «Число»
дано текст равно "12"
ожидается 12
пример «Не число»
дано текст равно "abc"
ожидается 0
разбор (к числу или беда текст)
случай вариант «Разобрано» с значение как н
то н
случай вариант «Не разобрано» с код как код и сообщение как весть
то 0Предусловие. Функция объявляет, что ей нужно, словом требует, и каждый
вызов проверяется при компиляции:
модуль «Предусловие»
тотальная функция «Делить»
принимает а: число, б: число
требует «делитель не ноль» б больше 0
возвращает число
а делить на б
тотальная функция «Половина»
принимает а: число
возвращает число
пример «Четыре пополам»
дано а равно 4
ожидается 2
«Делить» от а и 2Замените 2 на 0 в последней строке — и программа не соберётся:
$ flang check предусловие.flang
FLANG_PRECONDITION_CALL в файле предусловие.flang, строка 15, столбец 3: вызов «Делить» в функции «Половина» не снимает предусловие «делитель не ноль»: вычисление замкнутой цели не проходит: … Цель ЛОЖНА — доказывать нечего, надо чинить вызов или требование. …
Снимать предусловия компилятор умеет не для всякого условия: в 0.7.29 у него
десять правил («не меньше 0», «больше терма», «равно», «содержит» и другие —
отказ перечисляет все). б не равен 0 среди них нет, поэтому здесь написано
б больше 0.
Сумма типов. Модуль «Result» библиотеки:
тип «Результат» от «Значение» и «Беда»
вариант «Успех» содержит значение: «Значение»
вариант «Ошибка» содержит сообщение: «Беда»Как к этому относиться
Система типов здесь скромная по возможностям и внятная по сообщениям. Типы объявляются, сообщения говорят словами, разбор обязан быть полным, а то, что функция требует от аргумента, проверяется на месте вызова. Цена — в многословии: нет вывода типов функций, нет лямбд, нет перехвата, и каждое опасное место автор закрывает сам — предусловием, отказом значением или суммой типов.
Дальше — глава «Тотальность», про самую нестандартную часть проверок.
