2010 → Выпуск 5

Модель типизации Хиндли — Милнера и пример её реализации на языке Haskell

Роман Душкин

Аннотация: Статья описывает алгоритм Хиндли — Милнера, используемый для автоматического вывода типов выражений. Рассматриваются дополнения данного алгоритма, используемые в функциональном языке программирования Haskell в связи с наличием в этом языке ограниченного полиморфизма. Приводится пример реализации функции для автоматического вывода типов, реализованной на языке Haskell, для чего, в том числе, даются полезные примеры применения библиотеки синтаксического анализа.

The article describes the Hindley–Milner type inference algorithm. Extended version capable of handling bounded polymorphism is shown. Implementation of algorithm in Haskell is provided, complete with a small parser for lambda-calculus and a top-level for exploration of the type inference.

Обсуждение статьи ведётся в LiveJournal.

1 Введение

Настоящая статья продолжает цикл публикаций, посвящённый типизации в функциональном программировании и в языке программирования Haskell в частности. Предыдущие статьи данного цикла были опубликованы в номерах 2–4 журнала [11, 13, 12].

В перечисленных статьях упоминалось, что для некоторых видов полиморфизма проблема вывода типов неразрешима. В настоящей статье рассматривается механизм автоматического вывода типов, основанный на алгоритме Хиндли — Милнера (иногда в специальной литературе называемый алгоритмом Дамаса — Милнера или алгоритмом Хиндли — Милнера — Дамаса), который позволяет вывести тип в рамках большого числа формальных систем типов, в том числе и для полиморфных типов ранга 2 (определение и о способах применения параметрического полиморфизма высших рангов см. [13, 12]).

Если разработчик не указал явно тип выражений, используемых им в исходных кодах, алгоритм Хиндли — Милнера позволяет получать наиболее общие типы этих выражений. Наиболее общим типом называется такой тип заданного выражения, к которому можно привести любой другой тип, который может быть приписан этому выражению. Настоящая статья как раз описывает один из способов получения наиболее общего типа, а также процедуру приведения к нему — унификацию. В следующем разделе будет дано формальное определение наиболее общего типа.

Особенностью и положительным эффектом от использования алгоритма является то, что он позволяет разработчику программных средств не задумываться о типизации выражений в статически типизированных языках программирования — механизм вывода типов автоматически построит все недостающие определения, а компилятор языка проверит их на корректность.

Суть системы типизации Хиндли — Милнера заключается в том, что на уровне синтаксиса программы можно провести формальные преобразования таким образом, чтобы автоматически определить типы выражений, используемых в этой программе. Это избавляет разрабочика от необходимости явно указывать типы выражений, что в свою очередь влечёт за собой лаконичность и высокую степень читаемости кода программ. В таком языке программирования, как Haskell, декларации типов выражений обычно вносятся в исходные коды только для выражений самого верхнего уровня в целях документирования кода.

Алгоритм автоматического вывода типов основан на работах Хаскеля Карри и Роберта Фейса по типизированному λ-исчислению и был впервые представлен Роджером Хиндли в 1969 году. Последний доказал, что его алгоритм выводит наиболее общий тип выражения. Независимо от работы Хиндли в 1978 году Робин Милнер представил свой вариант алгоритма, который он назвал «алгоритм W» [6]. Наконец, в 1982 году Луис Дамас доказал, что алгоритм Милнера полон и позволяет выводить типы в полиморфных системах [2]. Алгоритмы, разработанные Р. Милнером и Р. Хиндли в свою очередь опираются на принцип резолюции, который был впервые предложен Дж. А. Робинзоном [8].

Независимо от этих исследователей алгоритм унификации и типизации были предложены Дж. Моррисом (1968 год), К. Мередитом (в 1950-х годах) и, предположительно, А. Тарским (вообще в 1920-х годах). По этому поводу Роджер Хиндли заметил: «Вероятно, кому-то не помешало бы научиться читать, или кому-то другому — писать» [15].

В алгоритме используются следующие обозначения и понятия:

Типами τ являются базовые типы из некоторого зафиксированного множества B, типовые переменные с идентификаторами из другого множества V, а также типы, полученные при помощи применения конструктора типов →:
τ ::= T ∣ v ∣ τ → τ

здесь T ∈ B — типы из зафиксированного множества базовых типов, v ∈ V — типовые переменные, идентификаторы которых берутся из некоторого множества V.
Базовые типы представляют собой обычные для разработчиков программного обеспечения конструкции — такие типы как Int, Bool и т. д. Теория λ-исчисления требует только наличия некоторого зафиксированного множества B, а состав этого множества не регламентируется.
В качестве идентификаторов типовых переменных обычно используются строчные буквы греческого алфавита с его начала: α, β, γ и т. д. В качестве соглашения, принимаемого для упрощения дальнейшего изложения, будет считаться, что строчные греческие буквы с начала алфавита — это типовые переменные. Буквы σ и τ (возможно, с индексами) — это обозначение типов вообще.
Конструктор типов -> является правоассоциативным, так что можно опускать скобки следующим образом: τ₁ → τ₂ → τ₃ ≡ τ₁ → (τ₂ → τ₃). Тип может быть представлен в виде двоичного дерева, в узлах которого находятся конструкторы типов, а в листьевых вершинах — базовые типы.
Выражениями e являются константы из некоторого зафиксированного множества C, переменные, абстракции и аппликации (применения):
e ::= c ∣ x ∣ λ x : τ.e ∣ (e e)

здесь c ∈ C — константы, имеющие базовые типы. Константами, являются конкретные значения из базовых типов. Например, True, False ∈ Bool, 0, 1 ∈ Int и т. д.
Запись λ x : τ.e обозначает типизированную абстракцию — связанная переменная x имеет тип τ.
Контексты типизации обозначаются полужирными заглавными буквами греческого алфавита: Γ, Δ и т. д. и представляют собой множества предположений о типизации вида x : τ, то есть предположений, что «переменная x имеет тип τ»:
Γ = { x_i : τ_i }_i = 1ⁿ
Отношение типизации, обозначаемое как Γ ⊢ e : τ, обозначает, что выражение e имеет тип τ в контексте Γ и, таким образом, корректно типизировано. Конкретизации отношений типизации называются суждениями о типизации.
Корректность суждений о типизации должна быть подтверждена при помощи правил вывода типов, которых имеется четыре:
1. Константы корректно типизированы и имеют либо определённый базовый тип, либо тип, представляющий собой типовую переменную:
  
  c : (T ∈ B) ∈ C
  
  Γ ⊢ c : T
  
  ∨
  c : (v ∈ V) ∈ C
  
  Γ ⊢ c : v
  
  (1)
  
  Типовые переменные используются для обобщения типовых выражений. При непосредственном использовании выражения, в типе которого имеются типовые переменные, все они должны быть конкретизированны либо базовыми типами, либо «стрелками»¹, в вершинах которых находятся базовые типы (речь, конечно, идёт о параметрическом полиморфизма первого ранга).
2. Если переменная x имеет тип τ в некотором контексте, то x^τ есть отношение типизации в этом контексте и x корректно типизирована.
  
  x : τ ∈ Γ
  
  Γ ⊢ x : τ
  
  (2)
3. Если в определённом контексте Γ вместе с предположением x : τ корректно типизировано выражение e типа σ, то в том же самом контексте без предположений о типе переменной x можно корректно типизировать абстракцию λ x : τ.e:
  
  Γ ⋃ { x : τ } ⊢ e : σ
  
  Γ ⊢ (λ x : τ.e) : τ → σ
  
  (3)
4. Если в некотором контексте выражение e₁ корректно типизировано типом τ → σ, а выражение e₂ корректно типизировано типом τ, то в этом же контексте можно корректно типизировать аппликацию (e₁ e₂):
  
  Γ ⊢ e₁ : τ → σ, e₂ : τ
  
  Γ ⊢ (e₁ e₂) : σ
  
  (4)

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

Теперь всё готово для рассмотрения самого алгоритма. Далее в статье в разделе 1 рассматривается сам алгоритм Хиндли — Милнера в «классической постановке». В разделе 2 описывается адаптация этого алгоритма для языка программирования Haskell. В разделе 3 приводятся определения функций на языке Haskell, реализующие алгоритм. В качестве дополнительной литературы по проблеме автоматического вывода типов можно порекомендовать [14, 7].

2 Описание алгоритма Хиндли — Милнера

Алгоритм автоматического вывода типов строит систему уравнений, неизвестными в которой являются типы, после чего решает эту систему, находя неизвестные значения. Базовый вариант алгоритма достаточно прост, поэтому он неоднократно переоткрывался независимо друг от друга различными исследователями в области информатики и прикладной математики, как уже было показано во введении. Базовый вариант оперирует только теми сущностями, которые используются в простом типизированном λ-исчислении — хотя непосредственно в процессе вывода используются типовые переменные, в результате работы алгоритма для λ-термов получаются только базовые типы из известного множества.

2.1 Построение системы уравнений

Чтобы построить систему уравнений вывода типов (типовых уравнений), необходимо последовательно применить два процесса, а именно:

На основании правил вывода типов породить систему предположений о типах для самого обрабатываемого λ-выражения и всех его подвыражений вплоть до переменных и констант. Правила вывода применяются без проверки предусловий, и это — особенность алгоритма Хиндли — Милнера.
Для предположений о типах всех подвыражений построить равенства вида τ₁ = τ₂ на основании того, что типы τ₁ и τ₂ приписаны одному и тому же λ-терму. Весь набор таких равенств и представляет собой систему типовых уравнений.

Система предположений о типах λ-выражений строится посредством применения правил вывода, указанных во введении, к каждому элементу обрабатываемого λ-терма. По сути предположения о типах представляют собой выражения вида e : τ, а сама система предположений — это ничто иное, как несколько расширенное понимание контекста Γ. Важными отличиями от определённого ранее термина является то, что, во-первых, при построении системы предположений в неё могут включаться несколько предположений для одного и того же выражения, а во-вторых, в контекст входят лишь типизации переменных, в то время как предположения о типах строятся для каждого подвыражения.

Например, простейшая аппликация двух переменных друг к другу (x y) породит систему предположений, состоящую из пяти элементов, а именно:

x : α — применение правила вывода (2) для переменной x.
y : β — применение того же правила вывода уже для переменной y.
(x y) : γ — применение правила вывода (4) для аппликации переменных.
y : δ — применение того же правила вывода для аппликации к переменной y.
x : δ → γ — расширение типа переменной x на основании правила вывода (4) в стрелку.

На основании этой системы предположений строится система типовых уравнений, состоящая из двух элементов, а именно:

α = δ → γ;
β = δ.

Поскольку рассматриваемый случай вырожден, полученная системая вывода типов тривиальна — она сама по себе является решением.

Если дополнить рассмотренную аппликацию абстракцией одной из переменных (к примеру, x), то система предположений о типах, а за ней и система типовых уравнений дополнятся. Соответственно, система предположений для λ-терма λ x.(xy) будет дополнена следующими предположениями:

x : ε;
(λ x.(xy)) : ε → η;
(xy) : η.

ну а система типовых уравнений будет преобразована к следующему виду (здесь первое уравнение записано в таком виде, чтобы не записывать три уравнения попарного равенства):

α = δ → γ = ε;
β = δ;
η = γ.

В процессе построения системы типовых уравнений на основе предположений о типах можно сразу проводить оптимизацию, не строя уравнения вида α → β, то есть уравнения, с каждой стороны которой стоит просто типовая переменная. Если для какого-то λ-терма в контексте Γ уже назначен тип в виде типовой переменной, то второе назначение типовой переменной не осуществляется. Если применить такой оптимизирующий подход, то три вышеприведённых уравнения «схлопнутся» в одно: α = β → γ.

2.2 Унификация

Для решения построенной системы уравнений применяется процедура унификации. Её суть заключается в сравнении типов и попытках сопоставить типы друг с другом.

Как указано во введении, тип представляет собой либо какой-то базовый тип из известного множества, либо типовую переменную, либо стрелку. Понятие типовой переменной вводится для упрощения процедуры вывода типов. В итоге есть три класса типовых сущностей: константа, переменная и стрелка, по обеим сторонам которой могут находиться эти же самые типовые сущности.

Для осуществления унификации необходимо понятие подстановки типов. Подстановкой типов называется отображение S из множества типов в него же, такое что вместо заданного типа τ подставляется некоторый другой тип σ. Базовые типы могут подставляться только сами в себя, а вместо типовой переменной можно подставить любой другой тип, который не включает в себя эту типовую переменную. Подстановка для стрелки осуществляется по схеме: S(σ → τ) = S(σ) → S(τ).

Если S(σ) = τ, то тип τ называется примером типа σ. Соответственно, если для некоторого λ-терма M имеет место, что ⊢ M : τ, и при этом любой другой тип терма M является примером типа τ, то тип τ называется наиболее общим типом (или главным типом).

Унификация производится на паре типов, таким образом имеется 3²=9 комбинаций для унификации. Также необходимо отметить, что операция унификации некоммутативна. Этот процесс односторонен — результат приведения первого типа ко второму в общем случае не равен результату приведения второго типа к первому. Пример: константу невозможно унифицировать переменной, а переменная унифицируется константой, принимая в качестве конкретного значения её саму.

Из-за чего возникает односторонность операции унификации? Дело в том, что в процессе вывода типа некоторого λ-выражения алгоритм должен пройтись по всем его подвыражениям и занести в контекст предположения о типах этих подвыражений. Подвыражения могут повторяться, а потому новый тип, выводимый для повторного проявления подвыражения должен унифицироваться с тем типом, который уже имеется в контексте.

C
v
→

C Унифицируется только в случае, если унифицируемые базовые типы совпадают. В противном случае имеет место ошибка несоответствия базовых типов. Предположение о типовой переменной отвергается, из контекста берётся базовый тип. Осуществляется проверка совместимости этого базового типа с использованием исследуемого выражения. Унифицируется только в случае, если базовый тип является функциональным типом, и обе стороны применения стрелки также могут быть унифицированы друг с другом.

v Типовая переменная в контексте принимает конкретное значение в виде унифицируемого базового типа. В контексте для исследуемого подвыражения оставляется только один идентификатор типовой переменной с обязательной заменой вхождений удаляемого идентификатора. Типовая переменная в контексте заменяется на стрелку (с подстановкой во всех типах в составе контекста).

→ Унифицируется только в случае, если унифицируемый базовый тип является функциональным типом, и обе стороны применения стрелки соответствуют друг с другу. Производится проверка на вхождение типовой переменной в состав стрелки. Если вхождение имеется, то имеет место ошибка типизации (например, как для λ-терма λ x.xx). В противном случае вместо переменной используется стрелка. Унифицируется только если друг с другом унифицируются соответствующие правые и левые операнды стрелок.

Таблица 1: Унификация типов

В таблице 1 представлены способы, при помощи которых типы унифицируются друг с другом. Строки соответствуют вариантам типов для исследуемого подвыражения, которые уже находятся в контексте (эти варианты указаны в первом, заголовочном столбце). Столбцы соответствуют вариантам типов, которые необходимо унифицировать с тем, что уже имеется в контексте (соответственно, эти варианты перечислены в заглавной строке).

В данной таблице C обозначает базовый тип из соответствующего множества базовых типов, v обозначает типовую переменную, а → обозначает стрелку.

2.3 Несколько несложных примеров

В качестве примеров, при помощи которых можно детально изучить алгоритм и закрепить его понимание, можно рассмотреть типизацию нескольких базовых комбинаторов. Например, пусть это будут композитор B, пермутатор C и дубликатор W².

Композитор B имеет комбинаторную характеристику Bxyz = x(yz). В виде λ-терма его можно представить как λ xyz.x(yz) или, записывая явно все синтаксические конструкции, — λ x.λ y.λ z.(x(yz)). Типизация первой абстракции, связывающей переменную x, даёт следующие предположения о типах подвыражений:

x : α;
(λ y.λ z.(x(yz))) : β;
(λ x.λ y.λ z.(x(yz))) : α → β.

Далее последовательно применяя правила вывода для каждого подвыражения, можно получить следующий набор предположений о типах:

y : γ;
(λ z.(x(yz))) : δ;
(λ y.λ z.(x(yz))) : γ → δ;
z : ε;
(x(yz)) : η;
(λ z.(x(yz))) : ε → η;
x : θ → ι;
(yz) : θ;
(x(yz)) : ι;
y : κ → µ;
z : κ;
(yz) : µ.

Сопоставляя подвыражения исходного λ-терма для композитора B, выстраивается система типовых уравнений:

α = θ → ι;
β = γ → δ;
γ = κ → µ;
δ = ε → η;
ε = κ;
η = ι;
θ = µ.

Наконец, собирается общий тип исходного λ-терма, который в контексте выглядит как α → β:

	α → β
⇒	(θ → ι) → (γ → δ)
⇒	(θ → ι) → ((κ → µ) → (ε → η))
⇒	(θ → η) → ((ε → θ) → (ε → η))
⇒	(θ → η) → (ε → θ) → ε → η
⇒^α	(β → γ) → (α → β) → α → γ

На последнем шаге вывода типов была произведена α-конверсия идентификаторов типовых переменных в целях приведения сигнатуры к более традиционному виду. В итоге получается корректно типизированный λ-терм: B : (β → γ) → (α → β) → α → γ. Если вспомнить, что в языке Haskell композитор B соответствует операции композиции функций ., то можно сравнить их типы (с помощью интерпретатора GHCi, использовав команду :t):

> :t (.) (.) :: (b -> c) -> (a -> b) -> a -> c

Так же типизируется пермутатор C, который в виде полного λ-терма записывается как λ x.λ y. λ z.((xz)y). Система уравнений для этого λ-терма выглядит следующим образом (для упрощения изложения перечисленные ниже выражения составлены из предположений о типах и типовых уравний, в связи с чем должны читаться как «для такого-то λ-терма в контексте имеются следующие подлежащие унификации типы», для этого использован символ двойного двоеточия):

x :: α	=	κ → µ.
y :: γ	=	θ.
z :: ε	=	κ.
λ y.λ z.((xz)y) :: β	=	γ → δ.
λ z.((xz)y) :: δ	=	ε → η.
((xz)y) :: η	=	ι.
(xz) :: θ → ι	=	µ.

Унификация этих типовых уравнений выглядит примерно так:

	α → β
⇒	(κ → µ) → (γ → δ)
⇒	(κ → µ) → (γ → (ε → η))
⇒	(κ → µ) → (θ → (κ → ι))
⇒	(κ → θ → ι) → θ → κ → ι
⇒^α	(α → β → γ) → β → α → γ

Полученное выражение типизации C: (α → β → γ) → β → α → γ опять же полностью соответствует типу функции flip в языке Haskell, которая переставляет аргументы для заданной функции:

> :t flip flip :: (a -> b -> c) -> b -> a -> c

Для дубликатора W процесс вывода типа абсолютно такой же. Читатель может самостоятельно составить набор предположений, на основании него вывести систему типовых уравнений, после чего провести процесс унификации. Результат можно сравнить со следующей цепочкой унификации:

	α → β
⇒	(θ → ι) → (γ → δ)
⇒	(θ → (ε → η)) → (γ → δ)
⇒	(θ → θ → η) → θ → η
⇒^α	(α → α → β) → α → β

Результат типизации W: (α → α → β) → α → β можно проверить в GHCi:

> :t (\x y -> x y y) (\x y -> x y y) :: (a -> a -> b) -> a -> b

Хорошее краткое описание алгоритма, дополнительные примеры, а также объяснение дополнительных правил вывода дано в презентации Р. Чепляки [15].

3 Адаптация алгоритма для языка Haskell

Любой прикладной язык программирования отличается от простого типизированного λ-исчисления наличием дополнительных синтаксических конструкций, ограничений и прочих вещей, которые не выражаются в терминах оного λ-исчисления. Например, комбинаторы неподвижной точки не типизируются в системе Хиндли — Милнера [9], а потому либо должны быть внедрены в ядро языка, либо для вывода типов должна использоваться иная система типизации (например, система Жирара-Рейнольдса, известная как «Система F»).

В языках программирования семейства ML (к которому можно отнести и язык Haskell) используются дополнительные синтаксические конструкции, которые позволяют определять функции (в том числе и рекурсивные). Общей методикой доработки алгоритма типизации является включение в состав базовых типов и правил вывода дополнительных сущностей, которые отражают особенности языка программирования [1].

В качестве примера можно рассмотреть некоторые особенности алгоритма типизации в Haskell. Несмотря на то, что алгоритм для этого языка базируется на системе Жирара-Рейнольдса, в её основе в любом случае лежит первоначальный алгоритм W и система типизации Хиндли — Милнера. Отметим следующие особенности, которые нужно учесть не только при изучении этого языка, но и других функциональных языков программирования:

Все типы в языке Haskell имеют в своём составе специальное значение ⊥, которое используется для обозначения незавершающихся или ошибочных вычислений. Обработка этого значения заложена в системе типизации языка Haskell.
Разработчик может определять свои алгебраические типы данных [11] и изоморфные типы, которые должны динамически вноситься в множество базовых типов и использоваться в процессе вывода типов.
Система классов типов, используемых в языке Haskell для описания функциональных интерфейсов и ограничений, налагаемых на используемые типы, дополняет алгоритм типизации необходимостью обрабатывать такие ограничения. Возможность использования нескольких ограничений, а также своеобразное «наследование» классов накладывает дополнительные требования на алгоритм типизации.
Расширения языка Haskell, связанные с системой типизации, а именно полиморфизм высших рангов [13], экзистенциальные типы [12], многопараметрические классы, классы с зависимыми параметрами и т. д., также дополняют и усложняют алгоритм вывода типов.

Дополнительно о типизации в языке Haskell и способах реализации алгоритма можно ознакомиться в статье [4].

4 Пример реализации функций для автоматического вывода типов

Чтобы закрепить полученные сведения об алгоритме вывода типов, имеет смысл реализовать простой вариант данного алгоритма. Пусть в качестве языка программирования выступает язык Haskell, а в качестве формальной системы, для которой будет реализовываться алгоритм типизации, выступает простое типизированное λ-исчисление. Дополнительно вводится ограничение, что в качестве константного типа выступает тип *, так что все функциональные типы имеют вид (* → *), (* → * → *), ((* → *) → *) и т. д.

Далее в данном разделе описываются типы для представления сущностей предметной области, специализированные функции для облегчения работы с разрабатываемой программой, а также основной алгоритм вывода типов по Хиндли — Милнеру.

4.1 Типы и связанные с ними определения

Для внутреннего представления структур данных, описывающих λ-термы и их типы, необходимо определить соответствующие типы языка Haskell. Эти типы определяются в полном соответствии с формулами, данными во введении.

Тип Expr описывает одно λ-выражение (англ. expression), которое может быть переменной (конструктор Var), применением терма к другому терму или аппликацией (конструктор App) или λ-абстракцией, то есть связыванием переменной с λ-термом (конструктор Abs):

data Expr = Var String | App Expr Expr | Abs String Expr deriving (Eq, Ord)

Тип Type описывает типы, которые могут быть сопоставлены λ-термам. Тип может быть константным (конструктор Const), типовой переменной (конструктор TyVar) и функциональным типом или стрелкой (конструктор Arrow):

data Type = Const | TyVar String | Arrow Type Type deriving Eq

Для того чтобы отображать значения двух вышеприведённых типов, имеет смысл специальным образом реализовать для них экземпляры класса Show, а не полагаться на автоматически построенные определения. Это делается тривиально:

instance Show Expr where show (Var name) = name show (App exp1@(Abs _ _) exp2) = "(" ++ show exp1 ++ ")" ++ show exp2 show (App expr (Var name)) = show expr ++ name show (App exp1 exp2) = show exp1 ++ "(" ++ show exp2 ++ ")" show (Abs name expr) = "\\" ++ name ++ "." ++ show expr

instance Show Type where show Const = "*" show (TyVar name) = name show (Arrow Const typ2) = "* -> " ++ show typ2 show (Arrow (TyVar name) typ2) = name ++ " -> " ++ show typ2 show (Arrow typ1 typ2) = "(" ++ show typ1 ++ ") -> " ++ show typ2

Данные экземпляры позволят выводить на экран значения типов Expr и Type соответственно в «традиционном» виде, учитывая соглашения об опускании скобок.

Так, например, комбинатор K ≡ λ xy.x, который во внутреннем представлении имеет вид «Abs "x" (Abs "y" (Var "x"))» (и в примерно таком же виде это представление выводилось бы на экран в случае использования автоматически сгенерированного экземпляра класса Show), будет преобразован в строку «\x.\y.x».

А тип комбинатора S ≡ λ xyz.xz(yz), который в принятых ограничениях может быть представлен как (* → * → *) → (* → *) → * → * и имеющий следующее внутреннее представление:

Arrow (Arrow Const (Arrow Const Const)) (Arrow (Arrow Const Const) (Arrow Const Const))

будет преобразован в строку «(* → * → *) → (* → *) → * → *».

4.2 Вспомогательные функции

Для того чтобы не утруждать пользователя разрабатываемой программы вводом описаний простых λ-выражений во внутреннем представлении, имеет смысл реализовать синтаксический анализатор, который будет переводить вводимую строку во внутреннее представление. Это также поможет при разработке цикла интерактивного взаимодействия, когда у пользователя просто не будет возможности вводить данные во внутреннем представлении в строке интерпретатора.

Синтаксический анализатор имеет смысл реализовывать только для простых λ-выражений, поскольку типы пользователь вводить не будет, они будут автоматически выводиться программой. Синтаксический анализатор, по сути, должен преобразовывать строку, сгенерированную при помощи экземпляра класса Show, обратно во внутреннее представление. Другими словами, для синтаксического анализатора parse должны выполняться следующие правила:

parse . show ≡ id :: Expr -> Expr
show . parse ≡ id :: String -> String

Для реализации синтаксического анализатора проще всего воспользоваться готовой библиотекой комбинаторов синтаксического анализа, например библиотекой Parsec, которая была разработана Д. Лейеном [5]. При помощи этой библиотеки формальная грамматика языка представления простых λ-выражений практически без изменений (с точностью до синтаксиса) записывается на языке Haskell.

Формальная грамматика для описания простых λ-выражений изоморфна определению оных (см. введение):

Expr ::= Var | App | Abs Var ::= <Id> App ::= '(' Expr Expr ')' Abs ::= '\' <Id> '.' Expr

В список задач настоящей статьи не входит обучение читателя основам синтаксического анализа и разработки функций для него. Заинтересованного читателя можно отослать к специализированной литературе на эту тему. Определения же функций для анализа простых типизированных λ-термов имеются в исходных кодах, которые можно получить с сайта журнала. Корневой функцией для анализа является функция parseExpr в модуле TIParser.

Проверка работоспособности этих функций осуществляется при помощи следующего определения (в нём также показан вариант использования функции parseExpr):

test :: String -> String test l = case parse parseExpr "" $ filter (not . isSpace) l of Left msg -> show msg Right rs -> show rs

Если в передаваемой на вход анализатору строке имеется синтаксическая ошибка, парсер вернёт значение Left, в котором содержится сообщение об ошибке. Если же синтаксический анализ прошёл успешно, в значении Right будет возвращён результат анализа, в рассматриваемом случае — λ-выражение во внутреннем представлении типа Expr.

4.3 Алгоритм типизации по Хиндли — Милнеру

Всё готово для того, чтобы реализовать функцию вывода типов для простого типизированного λ-исчисления. Правила вывода типов полностью совпадают с теми, что описаны во введении. Это позволяет непосредственно реализовать данные правила на языке Haskell. Поскольку констант в языке простого типизированного λ-исчисления нет, функция для вывода типов состоит из трёх клозов.

Имеет смысл рассмотреть тип функции inferType, предназначенной для вывода типов. Он таков:

inferType :: Expr -> [String] -> Environment -> Either String (Environment, [String])

Первый аргумент представляет собой выражение, тип которого необходимо вычислить. Второй аргумент — это список доступных для использования идентификаторов типовых переменных. Третий аргумент является окружением, в котором хранятся пары вида (Выражение, Тип). Это может быть простой список типа [(Expr, Type)], однако в целях оптимизации этот тип определён как отображение:

type Environment = Map Expr Type

Результатом выполнения функции inferType является пара, первый элемент которой представляет собой новое состояние окружения, в которое включён тип для обработанного выражения (заданного первым аргументом), а второй элемент — это обновлённый перечень доступных для использования идентификаторов типовых переменных. Как видно, результат функции inferType обёрнут в монаду Either String для обработки ошибочных ситуаций. Кроме того, можно было бы «спрятать» явную передачу окружения и перечня доступных для использования идентификаторов типовых переменных в монаду State, однако этого не сделано потому, что одновременное использование для иллюстрации алгоритма нескольких идиом языка Haskell не позволит за ними увидеть суть алгоритма.

Использование типовых переменных в данном случае обусловлено тем, что в процессе вывода необходимо проводить унификацию типов, что крайне затруднительно делать, если в качестве типов непосредственно подставлять принятый константный тип *. Реализованный алгоритм вывода типов возвращает общий тип с типовыми переменными, который легко конкретизируется константным типом просто при помощи подстановки в качестве каждой типовой переменной константного типа *. Эта функциональность подразумевается, и не будет реализована в рамках данной статьи.

Первый клоз функции inferType соответствует схеме типизации переменной. Если переменная уже присутствет в окружении, то ничего менять не надо. Если же переменной ещё в окружении нет, то необходимо добавить в окружение новую пару, взяв в качестве идентификатора типовой переменной первый свободный элемент списка. Таким образом, переменная типа Expr (Var n) связывается с типом TyVar tv:

inferType e@(Var n) t@(tv:tvs) env = case Map.lookup e env of Nothing -> return (Map.insert e (TyVar tv) env, tvs) Just _ -> return (env, t)

Следующий клоз функции inferType предназначен для обработки λ-абстракций. Как показано во введении, связывание переменной типа τ с некоторым выражением типа σ даёт λ-терм типа τ → σ. Опять же, это несложно выражается на языке Haskell. В описываемом ниже клозе вводится дополнительное ограничение — нельзя использовать повторяющиеся идентификаторы связанных переменных, поскольку для демонстрации возможностей алгоритма типизации нет необходимости реализовывать α-конверсию и формализм де Брауна [3]. В связи с этим производится проверка на наличие в окружении типа для связанной переменной: если тип уже назначен, то имеет место дублирование переменной, что недопустимо.

Если же тип переменной, связываемой рассматриваемой λ-абстракцией, не назначен, то производится попытка вывести тип выражения (тела λ-абстракции). Если попытка удачна, то в новое окружение записываются три пары — тип для связываемой переменной, тип для тела λ-абстракции (запись производится неявно во время вывода типа для него) и тип для всего λ-терма. При этом надо отметить, что во время вывода типа для тела λ-абстракции уже мог быть выведен и тип связанной переменной (если она входит в тело). Итак, клоз функции inferType выглядит следующим образом:

inferType e@(Abs n e1) (tv:tvs) env = case Map.lookup (Var n) env of Nothing -> do (env', tvs') <- inferType e1 tvs env let Just tp' = Map.lookup e1 env' case Map.lookup (Var n) env' of Nothing -> do let env'' = Map.insert (Var n) (TyVar tv) env' return (Map.insert e (Arrow (TyVar tv) tp') env'', tvs') Just tp -> return (Map.insert e (Arrow tp tp') env', tvs') Just tp -> fail ("ERROR: Duplicate bound variable \"" ++ n ++ "\" in lambda-abstraction.")

Самым интересным и самым непростым является случай вывода типа для аппликации. Здесь необходимо проверять, к чему применяется выражение, поскольку для разных видов λ-термов необходимо применять различные правила вывода типов, которые являются следствием правила вывода для аппликации (опять же см. введение).

Если выражение, к которому применяется другое выражение, является простой переменной, то в зависимости от того, используется эта переменная в применяемом выражении или нет, производится либо добавление новых типов в окружение, либо попытка унификации типов с последующим обновлением окружения в случае, если унификация прошла успешно.

Для аппликации, в которой первым выражением также является аппликация, вывод типов производится при помощи унификации типов, поскольку тип первой аппликации должен быть стрелкой. Если унификация прошла успешно, в окружение записываются новые значения типов.

Наконец, если аппликация производится к λ-абстракции (то есть это просто вызов функции в терминах функционального программирования), то производится сравнение типов на «совместимость», ведь если у λ-терма тип вида τ → σ, то у прикладываемого к нему выражения должен быть тип, унифицируемый типом τ.

В итоге получается следующий достаточно громоздкий клоз определения функции inferType. Для его понимания необходимо внимательно проследить изменения окружения, которые производятся при помощи вызова функции Map.insert.

inferType e@(App e1 e2) t@(tv:tvs) env = do (env', tvs') <- inferType e2 tvs env let Just tp' = Map.lookup e2 env' case e1 of Var{} -> case Map.lookup e1 env' of Nothing -> do return (Map.insert e (TyVar tv) (Map.insert e1 (Arrow tp' (TyVar tv)) env'), tvs') Just tp -> do env'' <- unifyTypes (Arrow tp' (TyVar tv), tp) env' let Just (Arrow tp'' tp''') = Map.lookup e1 env'' return (Map.insert e tp''' env'', tvs') App{} -> do (env'', tvs'') <- inferType e1 tvs' env' let Just tp = Map.lookup e1 env'' env''' <- unifyTypes (tp, Arrow tp' (TyVar tv)) env'' let Just (Arrow tp'' tp''') = Map.lookup e1 env''' return (Map.insert e tp''' env''', tvs'') Abs{} -> do (env'', tvs'') <- inferType e1 tvs' env' let Just (Arrow tp1 tp2) = Map.lookup e1 env'' if areTypesCompatible tp1 tp' then do env''' <- unifyTypes (tp1, tp') env'' let Just (Arrow tp1' tp2') = Map.lookup e1 env''' return (Map.insert e tp2' env''', tvs'') else fail ("ERROR: Can't apply \"" ++ show e1 ++ "\" to \"" ++ show e2 ++ "\". Incompatible types.")

Теперь необходимо реализовать функцию для унификации типов unifyTypes и предикат для проверки типов на совместимость areTypesCompatible.

Первая функция получает на вход два типа — первый необходимо унифицировать вторым. Результат работы этой функции помещается непосредственно в окружение, поэтому она тоже работает в монаде Either String. Таким образом, фукнция получает на вход пару типов, текущее значение окружения, а при успешном завершении возвращает обновлённое состояние окружения. Её определение выглядит следующим образом:

unifyTypes :: (Type, Type) -> Environment -> Either String Environment unifyTypes (Const, Const) env = return env unifyTypes (TyVar n, t) env = return $ Map.map (substituteTyVar n t) env unifyTypes (Arrow t1 t2, Arrow t1' t2') env = do env' <- unifyTypes (t1, t1') env unifyTypes (t2, t2') env' unifyTypes (t1, t2) _ = fail ("ERROR: Can't unify type (" ++ show t1 ++ ") with (" ++ show t2 ++ ").")

Типовая константа унифицируется с типовой константой, при этом изменений в окружение не вносится. Типовая переменная может быть унифицирована любым типом при помощи подстановки вместо типовой переменной этого типа во всех типовых выражениях, находящихся в окружении. Две стрелки унифицируются, если унифицируются соответствующие компоненты стрелок. Другие варианты унификации типов ошибочны (например, попытка унифицировать тип α → β типом α в λ-терме λ x.xx), в связи с чем возвращается сообщение об ошибке.

Функция substituteTyVar для подстановки типа вместо типовой переменной реализуется несложно:

substituteTyVar :: String -> Type -> Type -> Type substituteTyVar _ _ Const = Const substituteTyVar n t (TyVar n') | n' == n = t | otherwise = TyVar n' substituteTyVar n t (Arrow t1 t2) = Arrow (substituteTyVar n t t1) (substituteTyVar n t t2)

Первым аргументом является идентификатор типовой переменной, вместо которой необходимо подставить тип. Вторым аргументом является тип, который подставляется вместо типовой переменной. Третий аргумент — это тип, в котором производится замена (подстановка). Функция просто обходит дерево типа и заменяет вхождения заданной типовой переменной.

Наконец, предикат areTypesCompatible возвращает значение True в случае, если типы совместимы с точки зрения процесса унификации (первый тип может быть унифицирован вторым). Определение опять говорит само за себя:

areTypesCompatible :: Type -> Type -> Bool areTypesCompatible Const _ = True areTypesCompatible TyVar{} _ = True areTypesCompatible (Arrow t1 t2) (Arrow t1' t2') = areTypesCompatible t1 t1' && areTypesCompatible t2 t2' areTypesCompatible _ _ = False

4.4 Цикл опроса пользователя

Для упрощения способа использования разработанной функции вывода типов inferType можно организовать цикл интерактивного общения с пользователем. Это достигается при помощи простых определений:

main :: IO () main = do hSetBuffering stdout NoBuffering putStrLn "Type checker for simple Lambda-calculus.\n Enter lambda-term for typing or :quit to quit.\n" runInterpreterCycle

runInterpreterCycle :: IO () runInterpreterCycle = do putStr "> " term <- getLine if (map toUpper term) `isPrefixOf` ":QUIT" then return () else do case parse parseExpr "" (filter (not . isSpace) term) of Left msg -> putStrLn (show msg ++ "\n") Right r -> case inferType r generateTyVarNames Map.empty of Left msg -> putStrLn (msg ++ "\n") Right (e, _) -> let Just t = Map.lookup r e in putStrLn (show r ++ " :: " ++ show t ++ "\n") runInterpreterCycle

Функция runInterpreterCycle выполняет один шаг цикла опроса пользователя (детали см. в [10]). Если пользователь ввёл что-то похожее на команду «:QUIT», то цикл заканчивается и программа завершается. Иначе введённая строка трактуется как λ-терм, который анализируется синтаксическим анализатором parseExpr и в случае успеха для этого терма выводится тип. Если тип также выводится успешно, он печатается на экран, а цикл опроса пользователя запускается на новый виток. Если на каком-то этапе произошла ошибка, диагностическая информация о ней также выводится на экран, после чего цикл опроса пользователя запускается снова.

Результаты работы написанной программы примерно такие:

Type checker for simple Lambda-calculus. Enter lambda-term for typing or :quit to quit. > \x.x \x.x :: b -> b > \x.\y.x \x.\y.x :: c -> b -> c > \x.\y.\z.xz(yz) \x.\y.\z.xz(yz) :: (f -> e -> d) -> (f -> e) -> f -> d

Как уже сказано ранее, здесь не производится подстановка вместо типовых переменных константы *, поскольку это тривиальная операция. Вместо этого разработанная программа позволяет изучать типы простых λ-термов в наиболее общем виде, как это доказано Р. Милнером для алгоритма типизации Хиндли — Милнера.

5 Заключение

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

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

Для углублённого изучения механизмов автоматического вывода типов можно порекомендовать уже упоминавшиеся работы [14] и [7], а также статью [1].

Список литературы

[1]: Luca Cardelli. Basic polymorphic typechecking. Science of Computer Programming, 8:147–172, 1987.
[2]: Luis Damas and Robin Milner. Principal type-schemes for functional programs. In POPL-82: Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, ACM, pages 207–212.
[3]: de Bruijn N. G. A Combinatorial Problem. page 758–764, 1946.
[4]: Mark P. Jones. Typing Haskell in Haskell. In Haskell Workshop, 1999.
[5]: Daan Leijen. Parsec, a fast combinator parser. 2001.
[6]: Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348–375, 1978.
[7]: Benjamin C. Pierce. Types and Programming Languages. The MIT Press, Cambridge, Massachusetts, 2002. По адресу http://newstar.rinet.ru/~goga/tapl/ опубликован перевод книги на русский язык.
[8]: A. J. Robinson. A machine-oriented logic based on the resolution principle. In Journal of the ACM, volume 12, 1965.
[9]: Philip Wadler. Theorems for free. In Functional Programming Languages and Computer Arcitecture, pages 347–359. ACM Press, 1989.
[10]: Душкин Р. В. Простой интерпретатор команд. Журнал «Потенциал», 8(44):46–55, 2008.
[11]: Душкин Р. В. Алгебраические типы данных и их использование в программировании. Научно-практический журнал «Практика функционального программирования», 2(2):86–105, 2009.
[12]: Душкин Р. В. Мономорфизм, полиморфизм и экзистенциальные типы. Научно-практический журнал «Практика функционального программирования», 4(4):79–88, 2009.
[13]: Душкин Р. В. Полиморфизм в языке Haskell. Научно-практический журнал «Практика функционального программирования», 3(3):67–81, 2009.
[14]: Кирпичёв Е. Р. Элементы функциональных языков. Научно-практический журнал «Практика функционального программирования», 3(3):83–197, 2009.
[15]: Чепляка Р. Вывод типов и полиморфизм, 2009. Презентация доклада на LtU@Kiev, http://ro-che.info/docs/2009-05-30-ltu-kiev-type-inference.pdf.

1: Здесь и далее термином «стрелка» будет пониматься функциональный тип вида σ → τ.
2: Традиционные наименования данных комбинаторов происходят от их комбинаторных характеристик. Композитор B представляет собой операцию композиции функций, пермутатор C переставляет аргументы функции (англ. permute — менять порядок), а дубликатор W дублирует аргумент функции.

Этот документ был получен из L^AT_EX при помощи H^EV^EA


	C	v	→

C	Унифицируется только в случае, если унифицируемые базовые типы совпадают. В противном случае имеет место ошибка несоответствия базовых типов.	Предположение о типовой переменной отвергается, из контекста берётся базовый тип. Осуществляется проверка совместимости этого базового типа с использованием исследуемого выражения.	Унифицируется только в случае, если базовый тип является функциональным типом, и обе стороны применения стрелки также могут быть унифицированы друг с другом.
v	Типовая переменная в контексте принимает конкретное значение в виде унифицируемого базового типа.	В контексте для исследуемого подвыражения оставляется только один идентификатор типовой переменной с обязательной заменой вхождений удаляемого идентификатора.	Типовая переменная в контексте заменяется на стрелку (с подстановкой во всех типах в составе контекста).
→	Унифицируется только в случае, если унифицируемый базовый тип является функциональным типом, и обе стороны применения стрелки соответствуют друг с другу.	Производится проверка на вхождение типовой переменной в состав стрелки. Если вхождение имеется, то имеет место ошибка типизации (например, как для λ-терма λ x.xx). В противном случае вместо переменной используется стрелка.	Унифицируется только если друг с другом унифицируются соответствующие правые и левые операнды стрелок.

Практика функционального программирования