Также опубликовано на aleksandra.codes.
Если вы увлекаетесь функциональным программированием, возможно, вы слышали о Хиндли-Милнер. В противном случае это система типов, которая является основой для большинства статически типизированных функциональных языков, таких как Haskell, OCaml, SML или F #. Здесь вы можете прочитать об этом подробнее, потому что в этой статье я не буду вдаваться в подробности самого H-M; Я сосредоточусь на алгоритме вывода типов для систем типов на основе HM.
Тем не менее, было бы жаль, если бы я упустил свой шанс, рассказав вам о своем взгляде на его наиболее убедительные аспекты.
Одно из них - его полнота. Это означает, что вам будет нелегко, если вы попытаетесь обойти это. Ничего не скажешь: заткнись, я действительно хочу сделать это приведение типов. Он орал бы, сломал вашу программу во время компиляции и заставил бы вас держаться подальше от нее. Но то, что вас не убивает, делает вас сильнее. Вы можете обрести уверенность - если ваша программа наконец-то компилируется, вероятно, она сработает. (Это то, что я говорил себе, когда писал код на Haskell). Это не только позволяет раньше обнаруживать ошибки, но и часто предотвращает их.
Еще одна замечательная функция - это возможность определять тип выражения без явных объявлений. Об этом и будет эта статья. Я сделаю небольшой обзор того, как вывод типов работает для систем типов Хиндли Милнера. Некоторые примеры будут на Haskell, но они достаточно просты и не требуют предварительного знания Haskell. Я стремлюсь объяснить, как алгоритм вывода типов для систем типов на основе Хиндли-Милнера работает под капотом, не углубляясь в подробности и формальные определения.
Несколько слов о функциях
Как я уже сказал, некоторые примеры в статье взяты на Haskell, так что здесь мы подходим к заключению о функциях Haskell.
В Haskell функции являются первоклассными гражданами, а это означает, что они не обращают внимания на другие типы данных. В них нет ничего особенного. Мы относимся к ним так же, как и к другим типам данных.
Все функции в Haskell принимают один аргумент. Более конкретно - они принимают один аргумент за раз. Давайте посмотрим на, возможно, наиболее распространенный пример:
add :: Integer -> Integer -> Integer
add x y = x + y
Как читать на хаскелльском?
Добавить - это функция, которая принимает целое число и возвращает функцию, которая принимает целое число и возвращает целое число.
Для большей читабельности поставим скобки.
Добавить - это функция, которая принимает целое число и возвращает (функция, которая принимает целое число и возвращает целое число).
add :: Integer -> (Integer -> Integer)
Как и все функции в Haskell, Добавить каррировано.
Каррирование преобразует функцию, которая принимает n аргументов, в n функций, каждая из которых принимает по одному аргументу.
Поскольку все функции в Haskell принимают ровно один аргумент, вы можете рассматривать fun a b c = ...
как синтаксический сахар для привязки лямбда-функций к fun: fun = \a -> \b -> \c -> ...
.
Вывод типа
Вывод типа означает, что типы в программе могут быть выведены без явных аннотаций типов. Идея состоит в том, что некоторая информация может быть не указана, но алгоритм вывода типов может заполнить пробелы, определяя типы на основе их использования.
Вывод типов был впервые изобретен Хаскеллом Карри и Робертом Фейсом (для некоторых вещей, связанных с лямбда-исчислением). Затем Дж. Роджер Хиндли расширил этот алгоритм, а пару лет спустя Робин Милнер независимо разработал эквивалентный алгоритм - для языков программирования ML. Хотя практический вывод типов был разработан для машинного обучения, он применим и к другим языкам.
Существует широкий спектр того, в какой степени язык может выводить типы, и на практике почти ни один язык не поддерживает вывод полного типа. Core ML очень близок, но у него есть некоторые ограничения, когда речь идет о типах более высокого ранга.
Вывод типа поддерживает полиморфизм. Алгоритм использует переменные типа в качестве заполнителя для неизвестных типов. Иногда алгоритм вывода типов может разрешить все переменные типа и определить, что они должны быть равны определенным типам. Тем не менее, в других случаях тип функции может не ограничиваться способом определения функции. В этих случаях функция может применяться к любым аргументам, типы которых соответствуют форме, заданной выражением типа, содержащим переменную типа.
Идея вывода типов
Допустим, у нас есть простая функция:
inc x = x + 1
Мы знаем, что тип (+) - Int - ›Int -› Int. Кроме того, мы также знаем, что 1 имеет тип Int. Обладая этими знаниями, мы можем сделать вывод, что тип x должен быть Int. Это означает, что тип inc - Int - ›Int.
Теперь давайте посмотрим на другой пример и следующие рассуждения:
f (g, h) = g(h(0))
- h применяется к 0 :: Int
- На основе ☝️ мы можем вывести тип h: h :: Int - ›a, где a - некоторый неизвестный тип (тип переменная).
- g - это функция, которая принимает то, что возвращает h, и возвращает другую вещь неизвестного типа: g :: a - ›b.
- Собирая все вместе, первый аргумент f будет равен a - ›b, а второй - Int -› a.
- Следовательно, функция f принимает пару (f, g) возвращает тот же тип, что и функция g, что приводит нас к ее окончательному типу:
f :: (a -> b, Int -> a) -> b
Вывод типа vs проверка типа
Эти термины иногда путают, поэтому я хотел бы пояснить, в чем разница, прежде чем мы продолжим.
Проверка стандартного типа
int f(int x) { return x * x }
int g(int x) { return x * f(x) }
Средство проверки типов проверяет тело каждой функции, а затем использует объявленные типы программистом на предмет их совпадения. Взгляните на приведенный выше пример. Он будет проходить через каждое использование функций f и g и проверять две вещи:
- Если параметр всегда имеет целочисленный тип,
- Если функции возвращают целые числа.
Вывод типа
i̶n̶t̶ f(i̶n̶t̶ x) { return x * x }
i̶n̶t̶ g(i̶n̶t̶ x) { return x * f(x) }
Алгоритм вывода типа отличается. Он просматривает программу, исследует код без информации о типе и пытается вывести наиболее общие типы, которые могли быть объявлены.
Алгоритм вывода типа
Алгоритм состоит из трех шагов:
- Присвойте тип или переменную типа выражению и каждому подвыражению. Для известных выражений, таких как +, - и т. Д., Используйте типы, известные для этих выражений. В противном случае используйте переменные типа - заполнители для неизвестных типов.
- Сгенерируйте набор ограничений для типов, используя дерево синтаксического анализа выражения. Эти ограничения выглядят примерно так: если функция применяется к целому числу, то тип ее аргумента - целое число.
- Решите эти ограничения путем унификации - алгоритма решения уравнений, основанного на подстановках.
Теперь давайте посмотрим на этот алгоритм в действии 🚀
Примеры
#1
Мы начнем с простого примера, аналогичного тому, что у нас был раньше. Ниже представлено дерево синтаксического анализа выражения.
Корень указывает, что здесь у нас есть объявление функции. Потомки - это выражение, привязанное к родителю. В этом случае у нас есть добавить и x. Оператор плюса рассматривается как префиксный, а не инфиксный. Узлы @ обозначают функциональные приложения.
(+) 2 x эквивалентно x + 2. В Haskell заключение оператора в скобки преобразует его в префиксную функцию.
1. На первом этапе мы назначаем переменные типа каждому выражению. Каждое вхождение связанной переменной должно иметь один и тот же тип; в нашем случае переменная x имеет тот же тип (t1), что и узел привязки.
2. Теперь мы создаем набор ограничений для типов.
Давайте соберем все ограничения, которые у нас могут быть на данный момент.
- t3 = Int, поскольку 2 имеет тип Int.
- t2 = Int - ›Int -› Int, потому что алгоритм знает типы элементарных функций, такие как (+).
- Узлы переменных не вводят никаких ограничений, потому что алгоритм не знает ничего, кроме значений, которые они представляют, например: x остается как t1.
- @ узлы. Если у нас есть такое выражение, как веселье x, то мы говорим, что веселье применяется к x, а веселье - к тип функции. Более того, тип всего выражения fun x должен совпадать с типом возвращаемого значения fun. В нашем дереве синтаксического анализа @ означает развлечение.
3. Последний шаг - решение ограничений путем объединения.
Следующий список ограничений - это то, что мы получили на втором этапе.
1° t0 = t1 -> t6
2° t4 = t1 -> t6
3° t2 = t3 -> t4
4° t2 = Int -> (Int -> Int)
5° t3 = Int
Теперь из 4 ° и 5 ° мы можем вывести следующее уравнение:
6° t4 = Int -> Int (from 3° and 4°)
У нас все еще остаются нерешенными t1 и t6, но благодаря новому уравнению 6 ° и 2 ° мы можем подразумевать:
8° t1 = Int (from 2° and 7°)
9° t6 = Int (from 2° and 7°)
Ура! У нас все это решено 🎉
t0 = Int -> Int
t1 = Int
t2 = Int -> Int -> Int
t3 = Int
t4 = Int -> Int
t6 = Int
#2
На этот раз полиморфные функции. Я не буду вдаваться в подробности, надеюсь, вы уловили идею после первого примера.
1. Назначение переменных типа каждому выражению.
2. Создание набора ограничений для типов.
3. Решение ограничений путем объединения.
Вот что у нас есть на старте:
1° t1 = t2 -> t6
2° t0 = t3 -> t6
3° t3 = (t1, t2)
Благодаря уравнению 3 ° мы можем подставить t3 в уравнение 1 °:
4° t0 = (t1, t2) -> t6
Затем используйте 1 °, чтобы заменить t1 на 4 °:
5° t0 = (t2 -> t6, t2) -> t6
И это означает тип нашей полиморфной функции! 🎉
Сложность
Доказано, что временная сложность этого алгоритма экспоненциальна. Однако на практике это в основном линейно, но экспоненциально по глубине полиморфных объявлений.
Резюме
Как я писал в начале, это должно было быть очень краткое объяснение алгоритма вывода. Я надеюсь, что кому-то это пригодится.
Спасибо за Ваше внимание! Не стесняйтесь поправлять меня, если я что-то не так