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

http://www.codecommit.com/blog/scala/what-is-hindley-milner-and-why-is-it-cool
  • Перевод

Введение


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 для примеров кода
Поделиться публикацией
Комментарии 12
    +6
    О да, вывод типов в окамле — это то, что меня всегда радовало.
      0
      Работает алгоритм действительно потрясающе.

      Даже нет особого желания разбираться с тем, как он работает.
        +1
        А существуют случаи, когда алгоритм не может вывести тип и пользователю придется править код самостоятельно?
          +3
          Только если такого типа нет. Во всех остальных случаях алгоритм выводит наиболее общий тип выражения. Другое дело, что иногда требуется определить для выражения более конкретный тип (если более общий не подходит семантически). Тогда его задают вручную.
            +4
            Подробно алгоритм описан в статье Р.Душкина «Модель типизации Хиндли — Милнера и пример её реализации на языке Haskell» в 5-м выпуске журнала «Практика функционального программирования»
              +1
              Угу. Хорошая статья. Практически «на пальцах» объясняется. :) Мне на русском языке ничего лучше не попадалось.
            +1
            Спасибо за хороший перевод хорошей статьи.

            Когда я впервые заинтересовался этим алгоритмом, статья Даниэля Спивака мне очень помогла понять основы, и облегчила понимание более формального описания алгоритма.
              0
              Не раскрыта тема наследования. По крайней мере F# при коде насыщенном иерархиями наследования/коваринатностью ведет себя очень глухо (http://www.rsdn.ru/forum/decl/3789317.1.aspx)

              В Nemerle ситуация лучше, вот о его алгоритме было бы интереснее почитать.
                +1
                >> множество ограничей
                Опечатка?
                • НЛО прилетело и опубликовало эту надпись здесь
                  +5
                  Мой друг без аккаунта на Хабре попросил запостить следующее (надеюсь, что это не является нарушением правил, поскольку песочницы для комментариев нет):

                  Алгоритм вывода для систем типов Хиндли-Милнера был придуман Дамасом и Милнером. Он подходит для некоторого ряда систем типов, которые обладают общими свойствами. Оригинальная система типов, с которой работали Хиндли и Милнер была простое типизированное лямбда-исчисление. Современные алгоритмы вывода типов в языках Haskell, Ocaml, Standard ML хоть и предназначены для работы с более мощными системами типов, в основе содержат тот же алгоритм.

                  Язык Scala же, напротив, имеет систему типов, для которой вывод типов по этому алгоритму невозможен. Поэтому она использует другой алгоритм, он придуман Пирсом (local type inference) и улучшен Одерским (colored local type inference). Поэтому иллюстрировать текст про алгоритм Хиндли-Милнера примерами на Скале нехорошо. Спиваку об этом, кстати, несколько раз написали в комментариях к исходному посту. Он ответил, что да, он это сейчас понимает, но на момент написания текста (2008-й год) он этого не знал и текст уже переделывать не станет.
                    0
                    Спасибо, это хороший комментарий. Добавил ссылку на него в топик.

                  Только полноправные пользователи могут оставлять комментарии. Войдите, пожалуйста.

                  Самое читаемое