Система типов Хиндли – Милнера

Хиндли -Милнера ( HM ) Система типов — это классическая система типов для лямбда-исчисления с параметрическим полиморфизмом . Он также известен как Дамас-Милнер или Дамас-Хиндли-Милнер . Впервые его описал Дж. Роджер Хиндли. и позже вновь открыт Робином Милнером . Луис Дамас представил тщательный формальный анализ и доказательство метода в своей докторской диссертации.

Среди наиболее примечательных свойств HM — его полнота и способность определять наиболее общий тип данной программы без аннотаций типов или других подсказок, предоставляемых программистом. Алгоритм W является эффективным методом вывода типов на практике и успешно применяется на больших базах кода, хотя и имеет высокую теоретическую сложность . HM предпочтительно используется для функциональных языков . Впервые он был реализован как часть системы типов языка программирования ML . С тех пор HM расширялся различными способами, в первую очередь за счет классов типов, ограничений подобных тем, что есть в Haskell .

Введение

Основная статья: Вывод типа

В качестве метода вывода типа Хиндли-Милнер может выводить типы переменных, выражений и функций из программ, написанных в совершенно нетипизированном стиле. Будучи чувствительным к области действия , он не ограничивается получением типов только из небольшой части исходного кода, а скорее из целых программ или модулей. Способность работать с параметрическими типами также является основой систем типов многих функциональных языков программирования . Впервые он был применен таким образом в языке программирования ML .

Происхождением является алгоритм вывода типа для просто типизированного лямбда-исчисления , который был разработан Хаскеллом Карри и Робертом Фейсом в 1958 году. В 1969 году Дж. Роджер Хиндли расширил эту работу и доказал, что их алгоритм всегда выводит наиболее общий тип. В 1978 году Робин Милнер независимо от работы Хиндли предоставил эквивалентный алгоритм, алгоритм W. в 1982 году. Луис Дамас наконец доказал, что алгоритм Милнера является полным, и расширил его для поддержки систем с полиморфными ссылками.

Мономорфизм против полиморфизма

Основная статья: параметрический полиморфизм

В просто типизированном лямбда-исчислении типы T являются либо константами атомарного типа, либо функциональными типами формы $T\rightarrow T$. Такие типы мономорфны . Типичными примерами являются типы, используемые в арифметических значениях:

 3       : Number
 add 3 4 : Number
 add     : Number -> Number -> Number

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

идентификатор ≡ λ Икс . х

который просто возвращает любое значение, к которому оно применено. Менее тривиальные примеры включают параметрические типы, такие как списки .

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

 cons : forall a . a -> List a -> List a
 nil  : forall a . List a
 id   : forall a . a -> a

Полиморфные типы могут стать мономорфными путем последовательной замены их переменных. Примеры мономорфных экземпляров :

id'  : String -> String
nil' : List Number

В более общем смысле, типы являются полиморфными, если они содержат переменные типа, тогда как типы без них являются мономорфными.

В отличие от систем типов, используемых, например, в Pascal (1970) или C (1972), которые поддерживают только мономорфные типы, HM разработан с упором на параметрический полиморфизм. Преемники упомянутых языков, такие как C++ (1985), сосредоточились на различных типах полиморфизма, а именно на подтипировании в связи с объектно-ориентированным программированием и перегрузке . Хотя подтипирование несовместимо с HM, вариант систематической перегрузки доступен в основанной на HM системе типов Haskell.

Let-полиморфизм

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

 (λ id .  ... (id 3) ... (id "text") ... ) (λ x . x)

К сожалению, вывод типа в полиморфном лямбда-исчислении неразрешим. Вместо этого HM предоставляет let-полиморфизм формы

 let id = λ x . x
  in ... (id 3) ... (id "text") ...

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

Обзор

Оставшаяся часть этой статьи продолжается следующим образом:

• Определена система типов HM. Это делается путем описания системы вывода, которая точно определяет, какие выражения имеют какой тип, если таковые имеются.
• Далее он работает над реализацией метода вывода типа. После введения синтаксически-ориентированного варианта вышеупомянутой дедуктивной системы приводится набросок эффективной реализации (алгоритма J), апеллирующей главным образом к металогической интуиции читателя.
• Поскольку остается открытым вопрос, действительно ли алгоритм J реализует исходную систему вывода, вводится менее эффективная реализация (алгоритм W) и намекается на ее использование в доказательстве.
• Наконец, обсуждаются дополнительные темы, связанные с алгоритмом.

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

Система типов Хиндли – Милнера

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

Синтаксис

Выражения

${\begin{array}{lrll}\\e&=&x&{\textrm {variable}}\\&\vert &e_{1}\ e_{2}&{\textrm {application}}\\&\vert &\lambda \ x\ .\ e&{\textrm {abstraction}}\\&\vert &{\mathtt {let}}\ x=e_{1}\ {\mathtt {in}}\ e_{2}&\\\\\end{array}}$

Типы

${\begin{array}{llrll}\\{\textrm {mono}}&\tau &=&\alpha &\ {\textrm {variable}}\\&&\vert &C\ \tau \dots \tau &\ {\textrm {application}}\\{\textrm {poly}}&\sigma &=&\tau \\&&\vert &\forall \ \alpha \ .\ \sigma &\ {\textrm {quantifier}}\\\\\end{array}}$

Контекст и типизация

${\begin{array}{llrl}\\{\text{Context}}&\Gamma &=&\epsilon \ {\mathtt {(empty)}}\\&&\vert &\Gamma ,\ x:\sigma \\{\text{Typing}}&&=&\Gamma \vdash e:\sigma \\\\\end{array}}$

Переменные свободного типа

${\begin{array}{ll}\\{\text{free}}(\ \alpha \ )&=\ \left\{\alpha \right\}\\{\text{free}}(\ C\ \tau _{1}\dots \tau _{n}\ )&=\ \bigcup \limits _{i=1}^{n}{{\text{free}}(\ \tau _{i}\ )}\\{\text{free}}(\ \Gamma \ )&=\ \bigcup \limits _{x:\sigma \in \Gamma }{\text{free}}(\ \sigma \ )\\\\{\text{free}}(\ \forall \ \alpha \ .\ \sigma \ )&=\ {\text{free}}(\ \sigma \ )\ -\ \left\{\alpha \right\}\\{\text{free}}(\ \Gamma \vdash e:\sigma \ )&=\ {\text{free}}(\ \sigma \ )\ -\ {\text{free}}(\ \Gamma \ )\\\\\end{array}}$

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

Типы синтаксически делятся на две группы: монотипии и политипы.

Монотипии

Монотипии всегда обозначают определенный тип. Монотипии $\tau$ синтаксически представлены в виде терминов .

Примеры монотипий включают константы типа, такие как ${\mathtt {int}}$ или ${\mathtt {string}}$и параметрические типы, такие как ${\mathtt {Map\ (Set\ string)\ int}}$. Последние типы являются примерами применения , функций типа например, из множества $\{{\mathtt {Map^{2},\ Set^{1},\ string^{0},\ int^{0}}},\ \rightarrow ^{2}\}$, где верхний индекс указывает количество параметров типа. Полный набор типовых функций $C$ произвольно в HM, за исключением того, что он должен содержать как минимум $\rightarrow ^{2}$, тип функции. Для удобства его часто записывают в инфиксной записи. Например, функция, отображающая целые числа в строки, имеет тип ${\mathtt {int}}\rightarrow {\mathtt {string}}$. Опять же, круглые скобки могут использоваться для устранения неоднозначности выражения типа. Приложение привязывается сильнее, чем инфиксная стрелка, которая привязывается вправо.

Переменные типа допускаются как монотипы. Монотипии не следует путать с мономорфными типами, которые исключают переменные и допускают только основные термины.

Две монотипии равны, если у них одинаковые термины.

Политипы

Политипы (или схемы типов ) — это типы, содержащие переменные, связанные нулем или более кванторами для всех, например $\forall \alpha .\alpha \rightarrow \alpha$.

Функция с политипом $\forall \alpha .\alpha \rightarrow \alpha$ может сопоставить любое значение того же типа с самим собой, и функция идентификации является значением для этого типа.

В качестве другого примера: $\forall \alpha .({\mathtt {Set}}\ \alpha )\rightarrow {\mathtt {int}}$ — это тип функции, отображающей все конечные множества в целые числа. Функция, возвращающая мощность набора, будет значением этого типа.

Квантификаторы могут отображаться только на верхнем уровне. Например, тип $\forall \alpha .\alpha \rightarrow \forall \alpha .\alpha$ исключается синтаксисом типов. Также в состав политипов входят монотипии, при этом тип имеет общий вид. $\forall \alpha _{1}\dots \forall \alpha _{n}.\tau ,n\geq 0$, где $\tau$ является монотипией.

Равенство политипов сводится к изменению порядка количественной оценки и переименованию количественных переменных ( $\alpha$-конверсия). Кроме того, количественные переменные, не встречающиеся в монотипе, могут быть опущены.

Контекст и типизация

Чтобы осмысленно объединить все еще разрозненные части (синтаксические выражения и типы), необходима третья часть: контекст. Синтаксически контекст представляет собой список пар $x:\sigma$, называемые присваиваниями , предположениями или привязками , каждая пара указывает это значение переменной $x_{i}$имеет тип $\sigma _{i}.$ Все три части вместе дают типичную оценку формы. $\Gamma \ \vdash \ e:\sigma$, заявив, что при предположениях $\Gamma$, выражение $e$ имеет тип $\sigma$.

Переменные свободного типа

В типе $\forall \alpha _{1}\dots \forall \alpha _{n}.\tau$, символ $\forall$ является квантором, связывающим переменные типа $\alpha _{i}$ в монотипии $\tau$. Переменные $\alpha _{i}$ называются количественными , и любое появление переменной количественного типа в $\tau$ называется связанным , а все переменные несвязанного типа в $\tau$ называются бесплатными . Дополнительно к количественной оценке $\forall$ в политипах переменные типа также могут быть связаны, встречаясь в контексте, но с обратным эффектом в правой части $\vdash$. Такие переменные тогда ведут себя там как константы типа. Наконец, переменная типа может легально встречаться несвязанной при типизации, и в этом случае они неявно всеквантифицируются.

Наличие как связанных, так и несвязанных переменных типов довольно редко встречается в языках программирования. Часто все переменные типа неявно рассматриваются как всеквантованные. нет предложений со свободными переменными Например, в Прологе . Аналогично в Хаскеле где все переменные типа неявно имеют количественную оценку, т.е. тип Haskell. a -> a означает $\forall \alpha .\alpha \rightarrow \alpha$ здесь. Связанным с этим, но также очень редким, является связывающий эффект правой части. $\sigma$ из заданий.

Обычно смесь связанных и несвязанных переменных типа возникает из-за использования свободных переменных в выражении. Постоянная функция K = $\lambda x.\lambda y.x$ приводит пример. Имеет монотипию $\alpha \rightarrow \beta \rightarrow \alpha$. Можно вызвать полиморфизм с помощью $\mathbf {let} \ k=\lambda x.(\mathbf {let} \ f=\lambda y.x\ \mathbf {in} \ f)\ \mathbf {in} \ k$. Здесь, $f$ имеет тип $\forall \gamma .\gamma \rightarrow \alpha$. Свободная переменная монотипии $\alpha$ происходит от типа переменной $x$ связанный с окружающей областью. $k$ имеет тип $\forall \alpha \forall \beta .\alpha \rightarrow \beta \rightarrow \alpha$. Можно представить себе переменную свободного типа $\alpha$ в типе $f$ быть связанным $\forall \alpha$ в типе $k$. Но такое масштабирование не может быть выражено в HM. Скорее, привязка реализуется контекстом.

Тип заказа

Основная статья: Унификация (информатика) § Замена

Полиморфизм означает, что одно и то же выражение может иметь (возможно, бесконечно) множество типов. Но в этой системе типов эти типы не совсем не связаны друг с другом, а скорее управляются параметрическим полиморфизмом.

Например, тождество $\lambda x.x$ может иметь $\forall \alpha .\alpha \rightarrow \alpha$ как его тип, так и ${\texttt {string}}\rightarrow {\texttt {string}}$ или ${\texttt {int}}\rightarrow {\texttt {int}}$ и многие другие, но не ${\texttt {int}}\rightarrow {\texttt {string}}$. Самый общий тип этой функции: $\forall \alpha .\alpha \rightarrow \alpha$, в то время как другие более конкретны и могут быть выведены из общего путем последовательного замена другого типа параметра типа , т. е. количественного переменная $\alpha$. Контрпример неверен, поскольку замена не соответствует.

Непротиворечивую замену можно сделать формальной, применив замену $S=\left\{\ a_{i}\mapsto \tau _{i},\ \dots \ \right\}$ к термину типа $\tau$, написано $S\tau$. Как следует из примера, замена тесно связана не только с порядком, который выражает, что тип является более или менее особенным, но также и с все-количественной оценкой, которая позволяет применить замену.

Правило специализации

$\displaystyle {\frac {\tau '=\left\{\alpha _{i}\mapsto \tau _{i}\right\}\tau \quad \beta _{i}\not \in {\textrm {free}}(\forall \alpha _{1}...\forall \alpha _{n}.\tau )}{\forall \alpha _{1}...\forall \alpha _{n}.\tau \sqsubseteq \forall \beta _{1}...\forall \beta _{m}.\tau '}}$

Формально в HM тип $\sigma '$ является более общим, чем $\sigma$, формально $\sigma '\sqsubseteq \sigma$, если некоторая количественная переменная в $\sigma '$ последовательно заменяется так, что получается $\sigma$ как показано на боковой панели. Этот порядок является частью определения типа системы типов.

В нашем предыдущем примере, применяя замену $S=\left\{\alpha \mapsto {\texttt {string}}\right\}$ приведет к $\forall \alpha .\alpha \rightarrow \alpha \sqsubseteq {\texttt {string}}\rightarrow {\texttt {string}}$.

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

Альтернативно, рассмотрите эквивалентное обозначение для политипов без кванторы, в которых количественные переменные представлены различным набором символы. В таких обозначениях специализация сводится к простому согласованному замена таких переменных.

Отношение $\sqsubseteq$ это частичный заказ и $\forall \alpha .\alpha$ является его наименьшим элементом.

Основной тип

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

Подстановка в типизациях

Определенный выше порядок типов можно распространить на типизации, поскольку подразумеваемая всеколичественная оценка типизаций обеспечивает последовательную замену:

$\Gamma \vdash e:\sigma \quad \Longrightarrow \quad S\Gamma \vdash e:S\sigma$

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

В этой статье будут обсуждаться четыре различных набора правил:

1. $\vdash _{D}$ декларативная система
2. $\vdash _{S}$ синтаксическая система
3. $\vdash _{J}$ алгоритм J
4. $\vdash _{W}$ алгоритм W

Дедуктивная система

Синтаксис правил

${\begin{array}{lrl}{\text{Predicate}}&=&\sigma \sqsubseteq \sigma '\\&\vert \ &\alpha \not \in free(\Gamma )\\&\vert \ &x:\alpha \in \Gamma \\\\{\text{Judgment}}&=&{\text{Typing}}\\{\text{Premise}}&=&{\text{Judgment}}\ \vert \ {\text{Predicate}}\\{\text{Conclusion}}&=&{\text{Judgment}}\\\\{\text{Rule}}&=&\displaystyle {\frac {{\textrm {Premise}}\ \dots }{\textrm {Conclusion}}}\quad [{\mathtt {Name}}]\end{array}}$

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

Доказательство с использованием правил — это последовательность суждений, в которой все предпосылки перечисляются перед заключением. В примерах ниже показан возможный формат доказательств. Слева направо в каждой строке показано заключение, $[{\mathtt {Name}}]$ применяемого правила и посылок, либо путем ссылки на более раннюю строку (номер), если посылка является суждением, либо путем явного определения предиката.

Правила набора текста

См. также Правила набора текста.

Декларативная система правил

${\begin{array}{cl}\displaystyle {\frac {x:\sigma \in \Gamma }{\Gamma \vdash _{D}x:\sigma }}&[{\mathtt {Var}}]\\\\\displaystyle {\frac {\Gamma \vdash _{D}e_{0}:\tau \rightarrow \tau '\quad \quad \Gamma \vdash _{D}e_{1}:\tau }{\Gamma \vdash _{D}e_{0}\ e_{1}:\tau '}}&[{\mathtt {App}}]\\\\\displaystyle {\frac {\Gamma ,\;x:\tau \vdash _{D}e:\tau '}{\Gamma \vdash _{D}\lambda \ x\ .\ e:\tau \rightarrow \tau '}}&[{\mathtt {Abs}}]\\\\\displaystyle {\frac {\Gamma \vdash _{D}e_{0}:\sigma \quad \quad \Gamma ,\,x:\sigma \vdash _{D}e_{1}:\tau }{\Gamma \vdash _{D}{\mathtt {let}}\ x=e_{0}\ {\mathtt {in}}\ e_{1}:\tau }}&[{\mathtt {Let}}]\\\\\\\displaystyle {\frac {\Gamma \vdash _{D}e:\sigma '\quad \sigma '\sqsubseteq \sigma }{\Gamma \vdash _{D}e:\sigma }}&[{\mathtt {Inst}}]\\\\\displaystyle {\frac {\Gamma \vdash _{D}e:\sigma \quad \alpha \notin {\text{free}}(\Gamma )}{\Gamma \vdash _{D}e:\forall \ \alpha \ .\ \sigma }}&[{\mathtt {Gen}}]\\\\\end{array}}$

В боковой рамке показаны правила вычетов системы типа HM. Условно правила можно разделить на две группы:

Первые четыре правила $[{\mathtt {Var}}]$ (доступ к переменной или функции), $[{\mathtt {App}}]$ ( приложение , т.е. вызов функции с одним параметром), $[{\mathtt {Abs}}]$ ( абстракция , т.е. объявление функции) и $[{\mathtt {Let}}]$ (объявление переменной) сосредоточены вокруг синтаксиса, представляя одно правило для каждой формы выражения. Их смысл очевиден на первый взгляд, поскольку они разлагают каждое выражение, доказывают свои подвыражения и, наконец, соединяют отдельные типы, встречающиеся в посылках, с типом в заключении.

Вторую группу образуют оставшиеся два правила. $[{\mathtt {Inst}}]$ и $[{\mathtt {Gen}}]$. Они занимаются специализацией и обобщением типов. В то время как правило $[{\mathtt {Inst}}]$ должно быть ясно из раздела о специализации выше , $[{\mathtt {Gen}}]$ дополняет первое, работая в противоположном направлении. Он допускает обобщение, т.е. количественную оценку монотипных переменных, не связанных с контекстом.

Следующие два примера демонстрируют систему правил в действии. Поскольку и выражение, и тип заданы, они представляют собой использование правил для проверки типов.

Пример : Доказательство $\Gamma \vdash _{D}id(n):int$ где $\Gamma =id:\forall \alpha .\alpha \rightarrow \alpha ,\ n:int$, можно было бы написать

${\begin{array}{llll}1:&\Gamma \vdash _{D}id:\forall \alpha .\alpha \rightarrow \alpha &[{\mathtt {Var}}]&(id:\forall \alpha .\alpha \rightarrow \alpha \in \Gamma )\\2:&\Gamma \vdash _{D}id:int\rightarrow int&[{\mathtt {Inst}}]&(1),\ (\forall \alpha .\alpha \rightarrow \alpha \sqsubseteq int\rightarrow int)\\3:&\Gamma \vdash _{D}n:int&[{\mathtt {Var}}]&(n:int\in \Gamma )\\4:&\Gamma \vdash _{D}id(n):int&[{\mathtt {App}}]&(2),\ (3)\\\end{array}}$

Пример : Чтобы продемонстрировать обобщение, $\vdash _{D}\ {\textbf {let}}\,id=\lambda x.x\ {\textbf {in}}\ id\,:\,\forall \alpha .\alpha \rightarrow \alpha$ показано ниже:

${\begin{array}{llll}1:&x:\alpha \vdash _{D}x:\alpha &[{\mathtt {Var}}]&(x:\alpha \in \left\{x:\alpha \right\})\\2:&\vdash _{D}\lambda x.x:\alpha \rightarrow \alpha &[{\mathtt {Abs}}]&(1)\\3:&id:\alpha \rightarrow \alpha \vdash _{D}id:\alpha \rightarrow \alpha &[{\mathtt {Var}}]&(id:\alpha \rightarrow \alpha \in \left\{id:\alpha \rightarrow \alpha \right\})\\4:&\vdash _{D}{\textbf {let}}\,id=\lambda x.x\ {\textbf {in}}\ id\,:\,\alpha \rightarrow \alpha &[{\mathtt {Let}}]&(2),\ (3)\\5:&\vdash _{D}{\textbf {let}}\,id=\lambda x.x\ {\textbf {in}}\ id\,:\,\forall \alpha .\alpha \rightarrow \alpha &[{\mathtt {Gen}}]&(4),\ (\alpha \not \in free(\epsilon ))\\\end{array}}$

Let-полиморфизм

Не видимый сразу набор правил кодирует положение, при котором тип может быть обобщен или нет путем незначительного изменения использования моно- и политипов в правилах. $[{\mathtt {Abs}}]$ и $[{\mathtt {Let}}]$. Помните, что $\sigma$ и $\tau$ обозначают поли- и монотипии соответственно.

В правиле $[{\mathtt {Abs}}]$, переменная значения параметра функции $\lambda x.e$ добавляется в контекст с мономорфным типом через посылку $\Gamma ,\ x:\tau \vdash _{D}e:\tau '$, в то время как в правиле $[{\mathtt {Let}}]$, переменная попадает в среду в полиморфном виде $\Gamma ,\ x:\sigma \vdash _{D}e_{1}:\tau$. Хотя в обоих случаях наличие $x$ в контексте запрещает использование правила обобщения для любой свободной переменной в присваивании, это правило принудительно определяет тип параметра $x$ в $\lambda$-выражение останется мономорфным, в то время как в let-выражении переменная может быть введена полиморфной, что делает возможной специализацию.

В результате этого регулирования $\lambda f.(f\,{\textrm {true}},f\,{\textrm {0}})$ невозможно напечатать, поскольку параметр $f$ находится в мономорфном положении, а ${\textbf {let}}\ f=\lambda x.x\,{\textbf {in}}\,(f\,{\textrm {true}},f\,{\textrm {0}})$ имеет тип $(bool,int)$, потому что $f$ был введен в let-выражение и поэтому считается полиморфным.

Правило обобщения

Правило обобщения также заслуживает более пристального внимания. Здесь всеколичественная оценка, подразумеваемая в предпосылке $\Gamma \vdash _{D}e:\sigma$ просто перемещается в правую часть $\vdash _{D}$ в заключении, связанном явным квантором универсальности. Это возможно, поскольку $\alpha$ не встречается свободно в контексте. Опять же, хотя это и делает правило обобщения правдоподобным, на самом деле оно не является его следствием. Напротив, правило обобщения является частью определения системы типов HM, а неявная всеквантификация является следствием.

Алгоритм вывода

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

Степени свободы выбора правил

Выделение точек в доказательстве, где решение вообще невозможно, первая группа правил, основанная на синтаксисе, не оставляет выбора, поскольку каждому синтаксическому правилу соответствует уникальное правило типизации, определяющее часть доказательства, тогда как между выводом и посылками этих фиксированные части цепей $[{\mathtt {Inst}}]$ и $[{\mathtt {Gen}}]$ могло произойти. Такая цепочка могла существовать и между заключением доказательство и правило высшего выражения. Все доказательства должны иметь такая нарисованная форма.

Поскольку единственным выбором в доказательстве в отношении выбора правил является $[{\mathtt {Inst}}]$ и $[{\mathtt {Gen}}]$ цепи, Форма доказательства наводит на вопрос, можно ли его уточнить, где эти цепи могут быть не нужны. На самом деле это возможно и приводит к вариант системы правил без таких правил.

Система правил, управляемая синтаксисом

Синтаксическая система правил

${\begin{array}{cl}\displaystyle {\frac {x:\sigma \in \Gamma \quad \sigma \sqsubseteq \tau }{\Gamma \vdash _{S}x:\tau }}&[{\mathtt {Var}}]\\\\\displaystyle {\frac {\Gamma \vdash _{S}e_{0}:\tau \rightarrow \tau '\quad \quad \Gamma \vdash _{S}e_{1}:\tau }{\Gamma \vdash _{S}e_{0}\ e_{1}:\tau '}}&[{\mathtt {App}}]\\\\\displaystyle {\frac {\Gamma ,\;x:\tau \vdash _{S}e:\tau '}{\Gamma \vdash _{S}\lambda \ x\ .\ e:\tau \rightarrow \tau '}}&[{\mathtt {Abs}}]\\\\\displaystyle {\frac {\Gamma \vdash _{S}e_{0}:\tau \quad \quad \Gamma ,\,x:{\bar {\Gamma }}(\tau )\vdash _{S}e_{1}:\tau '}{\Gamma \vdash _{S}{\mathtt {let}}\ x=e_{0}\ {\mathtt {in}}\ e_{1}:\tau '}}&[{\mathtt {Let}}]\end{array}}$

Обобщение

${\bar {\Gamma }}(\tau )=\forall \ {\hat {\alpha }}\ .\ \tau \quad \quad {\hat {\alpha }}={\textrm {free}}(\tau )-{\textrm {free}}(\Gamma )$

Современная трактовка HM использует чисто синтаксическую систему правил из-за Клемент как промежуточный этап. В этой системе специализация располагается сразу после исходной. $[{\mathtt {Var}}]$ правило и сливается с ним, а обобщение становится частью $[{\mathtt {Let}}]$ правило. Там такое обобщение также решил всегда создавать наиболее общий тип, вводя функцию ${\bar {\Gamma }}(\tau )$, что количественно определяет все переменные монотипа, не связанные в $\Gamma$.

Формально, чтобы подтвердить, что эта новая система правил $\vdash _{S}$ эквивалентно оригиналу $\vdash _{D}$, у одного есть чтобы показать это $\Gamma \vdash _{D}\ e:\sigma \Leftrightarrow \Gamma \vdash _{S}\ e:\sigma$, которое распадается на два поддоказательства:

• $\Gamma \vdash _{D}\ e:\sigma \Leftarrow \Gamma \vdash _{S}\ e:\sigma$ ( Последовательность )
• $\Gamma \vdash _{D}\ e:\sigma \Rightarrow \Gamma \vdash _{S}\ e:\sigma$ ( Полнота )

Хотя последовательность можно увидеть, разложив правила $[{\mathtt {Let}}]$ и $[{\mathtt {Var}}]$ из $\vdash _{S}$ в доказательства в $\vdash _{D}$, вероятно, видно, что $\vdash _{S}$ является неполным, так как нельзя показать $\lambda \ x.x:\forall \alpha .\alpha \rightarrow \alpha$ в $\vdash _{S}$например, но только $\lambda \ x.x:\alpha \rightarrow \alpha$. Доказуема лишь немного более слабая версия полноты. хотя, а именно

• $\Gamma \vdash _{D}\ e:\sigma \Rightarrow \Gamma \vdash _{S}\ e:\tau \wedge {\bar {\Gamma }}(\tau )\sqsubseteq \sigma$

подразумевая, что можно получить основной тип выражения в $\vdash _{S}$ что позволяет нам в конечном итоге обобщить доказательство.

Сравнивая $\vdash _{D}$ и $\vdash _{S}$, сейчас в суждениях всех правил фигурируют только монотипии. Кроме того, форма любого возможного доказательства с помощью системы вывода теперь идентична форме выражения (оба рассматриваются как деревья ). Таким образом, выражение полностью определяет форму доказательства. В $\vdash _{D}$ форма, вероятно, будет определена с учетом всех правил, кроме $[{\mathtt {Inst}}]$ и $[{\mathtt {Gen}}]$, которые позволяют строить сколь угодно длинные ветки (цепочки) между остальными узлами.

Степени свободы, реализующие правила

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

Здесь вступает в силу порядок замещения (специализации). Хотя на первый взгляд невозможно определить типы локально, есть надежда, что их можно будет уточнить с помощью порядка при обходе дерева доказательства, дополнительно предполагая, поскольку полученный алгоритм должен стать методом вывода, что Тип любого помещения будет определен как наилучший. И действительно, можно, глядя на правила $\vdash _{S}$ предлагает:

• [ Abs ] : Критическим выбором является τ . ничего не известно На данный момент о τ , поэтому можно лишь предположить наиболее общий тип, а именно: $\forall \alpha .\alpha$. План состоит в том, чтобы специализировать этот тип, если в этом возникнет необходимость. К сожалению, политип в этом месте не разрешен, поэтому некоторого α на данный момент достаточно . Чтобы избежать нежелательного захвата, безопасным выбором будет переменная типа, которая еще не проверена. Кроме того, следует иметь в виду, что эта монотипия еще не фиксирована и может быть уточнена.
• [ Var ] : Выбор в том, как уточнить σ . Поскольку любой выбор типа τ здесь зависит от использования переменной, которая не известна локально, самым безопасным вариантом является наиболее общий. Используя тот же метод, что и выше, можно создать экземпляры всех количественных переменных в σ с новыми переменными монотипа, снова оставляя их открытыми для дальнейшего уточнения.
• [ Let ] : Правило не оставляет выбора. Сделанный.
• [ Приложение ] : Только правило приложения может привести к уточнению переменных, «открытых» на данный момент, как того требуют обе предпосылки.
  1. Первая посылка заставляет результат вывода иметь форму $\tau \rightarrow \tau '$.
     • Если это так, то хорошо. Позже можно выбрать его τ' для результата.
     • Если нет, то это может быть открытая переменная. Затем это можно уточнить до требуемой формы с двумя новыми переменными, как и раньше.
     • В противном случае проверка типа не удалась, поскольку первая предпосылка вывела тип, который не является и не может быть преобразован в тип функции.
  2. Вторая посылка требует, чтобы выведенный тип был равен τ первой посылки. Теперь есть два, возможно, разных типа, возможно, с переменными открытого типа, которые можно сравнить и приравнять, если это возможно. Если да, то обнаруживается уточнение, а если нет, то снова обнаруживается ошибка типа. Известен эффективный метод «приведения двух членов равными» заменой — Робинсона Унификация в сочетании с так называемым алгоритмом Union-Find .

Кратко суммируя алгоритм поиска объединения, учитывая множество всех типов в доказательстве, он позволяет группировать их в классы эквивалентности с помощью союз процедуры и выбрать представителя для каждого такого класса, используя найти процедуру. Подчеркивая слово процедура в смысле побочного эффекта , мы явно выходим из области логики, чтобы подготовить эффективный алгоритм. Представитель а. ${\mathtt {union}}(a,b)$ определяется так, что, если и a, и b являются переменными типа, то представителем произвольно является один из них, но при объединении переменной и термина представитель становится представителем. Предполагая реализацию Union-Find под рукой, можно сформулировать объединение двух монотипий следующим образом:

unify(ta, tb):
    ta = find(ta)
    tb = find(tb)
    if both ta,tb are terms of the form D p1..pn with identical D,n then
        unify(ta[i], tb[i]) for each corresponding ith parameter
    else
    if at least one of ta,tb is a type variable then
        union(ta, tb)
    else
        error 'types do not match'

Теперь, имея под рукой набросок алгоритма вывода, в следующем разделе будет дано более формальное представление. Это описано у Милнера. стр. 370 и далее. как алгоритм Дж.

Алгоритм J

Алгоритм J

${\begin{array}{cl}\displaystyle {\frac {x:\sigma \in \Gamma \quad \tau ={\mathit {inst}}(\sigma )}{\Gamma \vdash _{J}x:\tau }}&[{\mathtt {Var}}]\\\\\displaystyle {\frac {\Gamma \vdash _{J}e_{0}:\tau _{0}\quad \Gamma \vdash _{J}e_{1}:\tau _{1}\quad \tau '={\mathit {newvar}}\quad {\mathit {unify}}(\tau _{0},\ \tau _{1}\rightarrow \tau ')}{\Gamma \vdash _{J}e_{0}\ e_{1}:\tau '}}&[{\mathtt {App}}]\\\\\displaystyle {\frac {\tau ={\mathit {newvar}}\quad \Gamma ,\;x:\tau \vdash _{J}e:\tau '}{\Gamma \vdash _{J}\lambda \ x\ .\ e:\tau \rightarrow \tau '}}&[{\mathtt {Abs}}]\\\\\displaystyle {\frac {\Gamma \vdash _{J}e_{0}:\tau \quad \quad \Gamma ,\,x:{\bar {\Gamma }}(\tau )\vdash _{J}e_{1}:\tau '}{\Gamma \vdash _{J}{\mathtt {let}}\ x=e_{0}\ {\mathtt {in}}\ e_{1}:\tau '}}&[{\mathtt {Let}}]\end{array}}$

Представление алгоритма J представляет собой неправильное использование обозначений логических правил, поскольку оно включает в себя побочные эффекты, но допускает прямое сравнение с $\vdash _{S}$ одновременно выражая эффективную реализацию. В правилах теперь указана процедура с параметрами $\Gamma ,e$ уступчивость $\tau$ в заключении, где исполнение посылок идет слева направо.

Процедура $inst(\sigma )$ специализируется на политипе $\sigma$ путем копирования термина и последовательной замены переменных связанного типа новыми переменными монотипа. ' $newvar$' создает новую переменную монотипа. Вероятный, ${\bar {\Gamma }}(\tau )$ должен скопировать тип, вводя новые переменные для количественного анализа, чтобы избежать нежелательного захвата. В целом, алгоритм теперь всегда делает наиболее общий выбор, оставляя специализацию унификации, которая сама по себе дает наиболее общий результат. Как уже отмечалось выше , окончательный результат $\tau$ должен быть обобщен до ${\bar {\Gamma }}(\tau )$ в конце концов, чтобы получить наиболее общий тип для данного выражения.

Поскольку стоимость процедур, используемых в алгоритме, составляет около O(1), общая стоимость алгоритма близка к линейной зависимости от размера выражения, для которого необходимо определить тип. Это резко контрастирует со многими другими попытками разработать алгоритмы вывода типа, которые часто оказывались NP-трудными , если не неразрешимыми в отношении завершения. Таким образом, HM работает так же хорошо, как и лучшие полностью информированные алгоритмы проверки типов. Проверка типов здесь означает, что алгоритму не нужно находить доказательство, а только проверять заданное.

Эффективность немного снижается, поскольку необходимо поддерживать привязку переменных типа в контексте, чтобы обеспечить возможность вычисления ${\bar {\Gamma }}(\tau )$ и включите проверку возникновения , чтобы предотвратить построение рекурсивных типов во время ${\mathit {unify}}(\alpha ,\tau )$. Примером такого случая является $\lambda \ x.(x\ x)$, для которого тип не может быть получен с помощью HM. На практике типы представляют собой лишь небольшие термины и не образуют расширяющихся структур. Таким образом, при анализе сложности их сравнение можно рассматривать как константу, сохраняя затраты O(1).

Доказательство алгоритма

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

Наиболее важным моментом в приведенной выше аргументации является уточнение монотипии. переменные, связанные контекстом. Например, алгоритм смело меняет контекст при выводе, например $\lambda f.(f\ 1)$, потому что переменная монотипии добавлена ​​в контекст для параметра $f$ позже надо доработать к $int\rightarrow \beta$ при работе с приложением. Проблема в том, что правила вычета не допускают такого уточнения. Утверждая, что уточненный тип мог быть добавлен раньше вместо монотипная переменная в лучшем случае является целесообразным.

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

$\Gamma \vdash _{S}e:\tau \quad \Longrightarrow \quad S\Gamma \vdash _{S}e:S\tau$

Таким образом, уточнение свободных переменных означает уточнение всей типизации.

Алгоритм W

Алгоритм W

${\begin{array}{cl}\displaystyle {\frac {x:\sigma \in \Gamma \quad \tau ={\mathit {inst}}(\sigma )}{\Gamma \vdash _{W}x:\tau ,\emptyset }}&[{\mathtt {Var}}]\\\\\displaystyle {\frac {\begin{array}{ll}\Gamma \vdash _{W}e_{0}:\tau _{0},S_{0}&S_{0}\Gamma \vdash _{W}e_{1}:\tau _{1},S_{1}\\\tau '={\mathit {newvar}}&S_{2}={\mathsf {mgu}}(S_{1}\tau _{0},\ \tau _{1}\rightarrow \tau ')\end{array}}{\Gamma \vdash _{W}e_{0}\ e_{1}:S_{2}\tau ',S_{2}S_{1}S_{0}}}&[{\mathtt {App}}]\\\\\displaystyle {\frac {\tau ={\mathit {newvar}}\quad \Gamma ,\;x:\tau \vdash _{W}e:\tau ',S}{\Gamma \vdash _{W}\lambda \ x\ .\ e:S\tau \rightarrow \tau ',S}}&[{\mathtt {Abs}}]\\\\\displaystyle {\frac {\Gamma \vdash _{W}e_{0}:\tau ,S_{0}\quad S_{0}\Gamma ,\,x:{\overline {S_{0}\Gamma }}(\tau )\vdash _{W}e_{1}:\tau ',S_{1}}{\Gamma \vdash _{W}{\mathtt {let}}\ x=e_{0}\ {\mathtt {in}}\ e_{1}:\tau ',S_{1}S_{0}}}&[{\mathtt {Let}}]\end{array}}$

Отсюда доказательство алгоритма J приводит к алгоритму W, который делает только побочные эффекты, вызванные процедурой ${\textit {union}}$ явный по выражая его серийный состав посредством замен $S_{i}$. Представление алгоритма W на боковой панели по-прежнему использует побочные эффекты. в операциях, выделенных курсивом, но теперь они ограничиваются генерацией свежие символы. Форма судебного решения – это $\Gamma \vdash e:\tau ,S$, обозначая функцию с контекстом и выражением в качестве параметра, производящую монотипию вместе с замена. ${\textsf {mgu}}$ это версия без побочных эффектов из ${\textit {union}}$ производя замену, которая является наиболее общим объединителем .

Хотя алгоритм W обычно считается алгоритмом HM и часто представленный непосредственно после системы правил в литературе, его цель состоит в том, чтобы описано Милнером на стр. 369 следующим образом:

В нынешнем виде W вряд ли можно назвать эффективным алгоритмом; замены применяются слишком часто. Он был сформулирован для того, чтобы помочь доказать надежность. Теперь мы представляем более простой алгоритм J, который моделирует W в точном смысле.

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

Обязательства по доказательству

Прежде чем сформулировать обязательства по доказательству, необходимо подчеркнуть отклонение между системами правил D и S и представленными алгоритмами.

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

Наличие контекста $1:int,\ f:\alpha$, выражение $f\ 1$ тоже нельзя вводить $\vdash _{D}$ или $\vdash _{S}$, но алгоритмы придумывают тип $\beta$, где W дополнительно доставляет замену $\left\{\alpha \mapsto int\rightarrow \beta \right\}$, это означает, что алгоритм не может обнаружить все ошибки типов. Это упущение можно легко исправить, если более тщательно разграничить доказательства. переменные и переменные-монотипы.

Авторы прекрасно знали о проблеме, но решили не исправлять ее. Можно предположить, что за этим стоит прагматическая причина. Хотя более правильная реализация вывода типа позволила бы алгоритму работать с абстрактными монотипиями, они не были необходимы для предполагаемого применения, где ни один из элементов в ранее существовавшем контексте не имел свободных переменные. В этом свете ненужное усложнение было отброшено в пользу более простого алгоритма. Остающийся недостаток заключается в том, что доказательство алгоритма в отношении системы правил менее общее и может быть выполнено только для контекстов с $free(\Gamma )=\emptyset$ как побочное условие.

${\begin{array}{lll}{\text{(Correctness)}}&\Gamma \vdash _{W}e:\tau ,S&\quad \Longrightarrow \quad \Gamma \vdash _{S}e:\tau \\{\text{(Completeness)}}&\Gamma \vdash _{S}e:\tau &\quad \Longrightarrow \quad \Gamma \vdash _{W}e:\tau ',S\quad \quad {\text{forall}}\ \tau \ {\text{where}}\ {\overline {\emptyset }}(\tau ')\sqsubseteq \tau \end{array}}$

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

Чтобы правильно доказать обязательства, необходимо сначала их усилить, чтобы можно было активировать лемму о замене, пронизывающую замену. $S$ через $\vdash _{S}$ и $\vdash _{W}$. Отсюда доказательства проводятся индукцией по выражению.

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

Расширения

Рекурсивные определения

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

Правило ввода

Оригинальная бумага показывает, что рекурсия может быть реализована с помощью комбинатора ${\mathit {fix}}:\forall \alpha .(\alpha \rightarrow \alpha )\rightarrow \alpha$. Таким образом, возможное рекурсивное определение можно сформулировать как ${\mathtt {rec}}\ v=e_{1}\ {\mathtt {in}}\ e_{2}\ ::={\mathtt {let}}\ v={\mathit {fix}}(\lambda v.e_{1})\ {\mathtt {in}}\ e_{2}$.

В качестве альтернативы возможно расширение синтаксиса выражения и дополнительное правило типизации:

$\displaystyle {\frac {\Gamma ,\Gamma '\vdash e_{1}:\tau _{1}\quad \dots \quad \Gamma ,\Gamma '\vdash e_{n}:\tau _{n}\quad \Gamma ,\Gamma ''\vdash e:\tau }{\Gamma \ \vdash \ {\mathtt {rec}}\ v_{1}=e_{1}\ {\mathtt {and}}\ \dots \ {\mathtt {and}}\ v_{n}=e_{n}\ {\mathtt {in}}\ e:\tau }}\quad [{\mathtt {Rec}}]$

где

• $\Gamma '=v_{1}:\tau _{1},\ \dots ,\ v_{n}:\tau _{n}$
• $\Gamma ''=v_{1}:{\bar {\Gamma }}(\ \tau _{1}\ ),\ \dots ,\ v_{n}:{\bar {\Gamma }}(\ \tau _{n}\ )$

в основном слияние $[{\mathtt {Abs}}]$ и $[{\mathtt {Let}}]$ включая рекурсивно определенное переменные в позициях монотипии, где они встречаются слева от ${\mathtt {in}}$ а как политипы справа от него.

Последствия

Несмотря на то, что вышеизложенное очевидно, за это приходится платить.

Теория типов связывает лямбда-исчисление с вычислениями и логикой. Простая модификация, описанная выше, влияет на оба:

• Свойство сильной нормализации становится недействительным, поскольку можно сформулировать незавершающие термины.
• Логика терпит крах, потому что тип $\forall a.a$ становится обитаемым .

Перегрузка

Основная статья: Типовой класс

Перегрузка означает, что разные функции могут быть определены и использованы с одним и тем же именем. Большинство языков программирования, по крайней мере, обеспечивают перегрузку встроенными арифметическими операциями (+, < и т. д.), чтобы позволить программисту писать арифметические выражения в одной и той же форме, даже для разных числовых типов, таких как int или real. Поскольку сочетание этих разных типов в одном и том же выражении также требует неявного преобразования, перегрузка специально для этих операций часто встроена в сам язык программирования. В некоторых языках эта функция обобщена и доступна пользователю, например, в C++.

Хотя специальной перегрузки, поскольку затраты на вычисления как при проверке типов, так и при выводе в функциональном программировании удалось избежать было введено средство систематизации перегрузки, которое по форме и названию напоминает объектно-ориентированное программирование, но работает на уровень выше. «Экземпляры» в этой систематике являются не объектами (т.е. на уровне значений), а скорее типами. Пример быстрой сортировки, упомянутый во введении, использует перегрузку в заказах, имеющую следующую аннотацию типа в Haskell:

quickSort :: Ord a => [a] -> [a]

Здесь тип a не только полиморфен, но и ограничен экземпляром некоторого класса типов. Ord, который предоставляет предикаты порядка < и >= используется в теле функции. Правильные реализации этих предикатов затем передаются в функции быстрой сортировки в качестве дополнительных параметров, как только быстрая сортировка используется для более конкретных типов, обеспечивая единую реализацию перегруженной функции быстрой сортировки.

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

Типы высшего порядка

Основная статья: Вид (теория типов)

См. также: Класс типов § Полиморфизм высшего рода.

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

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

Haskell представляет еще один более высокий уровень под названием kind . В стандартном Haskell виды выводятся и используются не более чем для описания арности конструкторов типов. например, конструктор типа списка рассматривается как сопоставление типа (типа его элементов) с другим типом (типом списка, содержащего указанные элементы); условно это выражается как $*\to *$. Доступны языковые расширения, расширяющие виды для эмуляции функций зависимой системы типов .

Подтипирование

Основная статья: Подтипирование

Попытки объединить подтипирование и вывод типа вызвали немалое разочарование. Ограничения подтипирования легко накапливать и распространять (в отличие от ограничений равенства типов), делая результирующие ограничения частью выведенных схем типизации. например $\forall \alpha .\ (\alpha \leq T)\Rightarrow \alpha \rightarrow \alpha$, где $\alpha \leq T$ является ограничением переменной типа $\alpha$. Однако, поскольку в этом подходе переменные типов больше не унифицированы, он имеет тенденцию создавать большие и громоздкие схемы типизации, содержащие множество бесполезных переменных типов и ограничений, что затрудняет их чтение и понимание. Поэтому значительные усилия были приложены к упрощению таких схем типизации и их ограничений. использование методов, аналогичных методам недетерминированного конечного автоматного упрощения (NFA) (полезно при наличии выведенных рекурсивных типов). Совсем недавно Долан и Майкрофт формализовал связь между упрощением схемы типизации и упрощением NFA и показал, что алгебраический подход к формализации подтипирования позволяет генерировать компактные основные схемы типизации для ML-подобного языка (называемого MLsub). Примечательно, что предложенная ими схема типизации использовала ограниченную форму типов объединения и пересечения вместо явных ограничений. Позже Парро заявил что эта алгебраическая формулировка эквивалентна относительно простому алгоритму, напоминающему алгоритм W, и что использование типов объединения и пересечения не является обязательным.

С другой стороны, вывод типов оказался более сложным в контексте объектно-ориентированных языков программирования. потому что методы объекта, как правило, требуют первоклассного полиморфизма в стиле Системы F (где вывод типа неразрешим) и из-за таких особенностей, как F-ограниченный полиморфизм . обеспечивающие объектно-ориентированное программирование, такие как Карделли система Следовательно, системы типов с подтипами , $F_{<:}$, не поддерживают вывод типа в стиле HM.

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

Ссылки

• Майрсон, Гарри Г. (1990). «Решение о типизации ML завершено для детерминированного экспоненциального времени». Материалы 17-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования - POPL '90 . АКМ. стр. 382–401. дои : 10.1145/96709.96748 . ISBN  978-0-89791-343-0 . S2CID   75336 .
• Кфури, Эй Джей; Тюрин Дж.; Уржичин, П. (1990). «Типируемость ML завершена с учетом времени dexptime». Каап '90 . Конспекты лекций по информатике. Том. 431. С. 206–220. дои : 10.1007/3-540-52590-4_50 . ISBN  978-3-540-52590-5 .

Внешние ссылки

• Грамотная реализация Алгоритма W на Haskell вместе с его исходным кодом на GitHub .
• Простая реализация алгоритма Хиндли-Милнера на Python .