GrabDuck

Просто о Хиндли-Милнере

:

Введение


Robert MilnerЕсли вы когда-нибудь интересовались не слишком популярными языками, то должно быть слышали о «Хиндли-Милнере». Этот алгоритм вывода типов используются в F# и Haskell и OCaml, как и в их предшественнике ML. Некоторые исследователи даже пытаются использовать ХМ для оптимизации динамических языков вроде Ruby, JavaScript и Clojure.

И не смотря на его распространенность, до сих пор не было простого и понятного объяснения, что же это такое. Как же эта магия работает? Всегда ли выводимые типы будут верными? Или чем Хиндли-Милнер лучше, скажем, Java? И пока те, кто действительно знает что такое ХМ будут восстанавливаться от очередного умственного перенапряжения, мы попробуем разобраться в этом сами.

Первый шаг


По-существу, Хиндли-Милнер (или «Дамас-Милнер») это алгоритм для вывода типов значений на основании того, как они используются. Буквально, он формализует интуитивное представление о том, что тип может быть выведен из поддерживаемых им операций. Рассмотрим следующий код на псевдо-Scala [4]:
def foo(s: String) = s.length
 
// заметьте: без указания типов
def bar(x, y) = foo(x) + y

Просто посмотрев на определение функции bar, мы можем сказать, что ее тип должен быть (String, Int)=>Int. Это не сложно вывести. Мы просто смотрим на тело функции и видим два способоа использовать параметры x и y. x передается в foo, который ожидает String. Следовательно x должен иметь тип String для того, чтобы этот код скомпилировался. Более того, foo возвращает значение типа Int. Метод + класса Int ожидает параметр, также Int, следовательно y должен быть типа Int. Наконец, мы знаем, что + возвращает Int, а значит это и есть тип, возвращаемый bar.

И этот именно то, что делает Хиндли-Милнер: просматривая определение функции он вычисляет множество ограничений, накладываемых тем, как значение используется. И именно это мы и делали, когда заметили, что foo принимает параметр типа String. Как только создано множество ограничений, алгоритм завершает восстановление типов при помощи унификации этих ограничений. Если выражение хорошо типизировано, то в итоге ограничения приведут к недвусмысленному типу. Иначе одно (или несколько) ограничений будут взаимоисключающими или неразрешимыми с данным набором типов.

Неформальный алгоритм


Простой пример

Для того, чтобы было проще понять алгоритм, выполним каждый его шаг вручную. Во-первых, нужно вывести множество ограничений. Начнем с присваивания каждой переменной ( x и y) нового типа (т.е. «не существующего»). Если бы мы записали bar с этими типами, то вышло бы что-нибудь вроде [1]:
def bar(x: X, y: Y) = foo(x) + y

Не важно, как называются типы, главное, что они никак не пересекаются с «реальными» типами. Они нужны для того, чтобы алгоритм мог недвусмысленно ссылаться на еще не известный тип каждого значения. Без чего невозможно создать множество ограничений.

Далее, мы погружаемся в тело функции в поиске операций, которые налагают некоторые ограничения на тип. И так, первой операцией является вызов метода foo. [2] Мы знаем, что тип foo это String=>Int и это позволяет нам записать ограничение:

X ↦ String

Следующей операцией будет +, связанной со значением y. Scala представляет все операторы как вызов метода, т.о. это выражение в действительности значит " foo(x).+(y)". Мы уже знаем, что foo(x) это выражение типа Int (из типа возвращаемого foo), как и то, что + определен как метод класса Int с типом Int=>Int (конечно, это не совсем корректно использовать магию присущую только Scala). Что позволяет добавить в наше множество еще одно ограничение:

X ↦ String
Y ↦ Int

Последний шаг восстановления типов — это унификация всех этих ограничений для того, чтобы получить реальные типы, которые мы подставим вместо переменных X и Y. Унификация, буквально, — это процесс прохода через все ограничения в попытке найти единственный тип, который удовлетворяет им всем. Например, представьте, что вам дали следующие факты:

  • Маша высокая
  • Вася высокий
  • Маша любит красный
  • Вася любит синий
Теперь, посмотрите на эти ограничения:
  • Некто высок
  • Некто любит красный
Хмм, кем же может быть Некто? Этот процесс комбинирования множества ограничений вместе с множеством фактов может быть математически формализован в виде унификации. В случае с восстановление типов, достаточно переименовать «типы» в «факты».

В этом примере унификация множества ограничений тривиальна. У нас было всего лишь одно ограничение для каждого значения ( x и y) и оба они отображаются в реальные типы. Единственное, что требовалось это подставить " String" вместо " X" и " Int" вместо " Y".

Сложный пример

Чтобы почувствовать силу унификации, рассмотрим пример посложнее. Допустим, у нас есть следующая функция [3]:
def baz(a, b) = a(b) :: b

Здесь объявлена функция baz, которая из параметров принимает функцию и что-то еще, вызывая функцию от переданного ей второго параметра и затем присоединяя результат к нему же самому. Легко вывести множество ограничений для этой функции. Как и до этого, мы начнем с создания новых типов для каждого значения.
Заметьте, что в этом случае мы аннотируем не только параметры, но и возвращаемое значение.
def baz(a: X, b: Y): Z = a(b) :: b

Первое ограничение, которые мы выведем, будет тем, что параметр a должен быть функцией, что принимает значение типа Y и возвращает значение нового типа Y'. Более того, мы знаем, что :: это функция над классом List[A], которая принимает новый элемент A и возвращает новый список List[A]. Таким образом мы знаем, что Y и Z должны быть типа List[Y']. Ограничения, записанные в формальном виде:

X ↦ (Y=>Y')
Y ↦ List[Y']
Z ↦ List[Y']

Теперь унификация не на столько тривиальна. Важно, что переменная X зависит от Y, то есть потребуется как минимум еще один дополнительный шаг:

X ↦ (List[Y']=>Y')
Y ↦ List[Y']
Z ↦ List[Y']

Это то же множество ограничений, только на этот раз мы подставили известное отображение для Yв отображение для X. С помощью этой подстановки мы избавились от X, Y и Z из выведенных нами типов, получив следующую, типизированную функцию baz:

def baz(a: List[Y`]=>Y`, b: List[Y`]): List[Y`] = a(b) :: b

Конечно, это все еще не конечный результат. Даже если бы имя типа Y' было бы синтаксически верно, то ошибкой являлось бы отсутствие такого типа. Это случается, достаточно часто, при работе с алгоритмом восстановления типов Хиндли-Милнера. Каким-то образом, после вывода всех ограничений и унификации мы имеем «остатки» типов переменных, для которых больше нет ограничений.
Решением можно считать неограниченные переменные вроде параметров типа. В конце-концов, если параметр ничем не ограничен, то мы можем просто подставить любой тип, включая дженерик. И так, окончательная версия функции baz, куда мы добавили неограниченный параметр типа " A" и заменили им все вхождения Y' в выведенных типах:
def baz[A](a: List[A]=>A, b: List[A]): List[A] = a(b) :: b

Вывод


И… это всё! Хиндли-Милнер не сложнее, чем то, что мы здесь описали. Просто представить, как этот алгоритм может быть использован для восстановления типов выражений значительно более сложных, чем мы рассмотрели.

Надеюсь, эта статья помогла вам лучше понять, как же работает алгоритм Хиндли-Милнера. Этот тип вывода типов может быть очень полезен, сокращая количество кода, нужное для статической типизации до необходимого минимума. Пример " bar" был специально приведен в похожем на Ruby синтаксисе, чтобы показать, что этой информации все еще достаточно для проверки типов. Это может быть полезно следующий раз, когда кто-то скажет, что все статически типизированные языки слишком не выразительны.

Сноски и комментарии


  1. Тип возвращаемого значения опущен для простоты чтения. Технически, типы всегда выводятся для выражения в целом.
  2. Это поиск в глубину по АСД, что значит, что мы в первую очередь смотрим на операции с высоким приоритетом. Хотя технически не важен порядок обхода, но таким образом проще думать об алгоритме.
  3. "::" — это так называемый cons-оператор в Scala. Он отвечает за присоединение левого элемента к правому списку.
  4. О корректности использования Scala для примеров кода