Хиндли-Милнера ( НМ ) тип системы представляет собой классический тип системы для лямбда - исчисления с параметрическим полиморфизмом . Он также известен как Дамас-Милнер или Дамас-Хиндли-Милнер . Впервые он был описан Дж. Роджером Хиндли [1], а затем вновь открыт Робином Милнером . [2] Луис Дамас представил подробный формальный анализ и доказательство метода в своей докторской диссертации. [3] [4]
Среди наиболее примечательных свойств HM - его полнота и способность выводить наиболее общий тип данной программы без аннотаций типов, предоставляемых программистом, или других подсказок. Алгоритм W является эффективным методом вывода типов на практике и успешно применяется на больших базах кода, хотя имеет высокую теоретическую сложность . [примечание 1] HM предпочтительно использовать для функциональных языков . Впервые он был реализован как часть системы типов языка программирования ML . С тех пор HM был расширен различными способами, в первую очередь с помощью ограничений класса типов, подобных тем, которые есть в Haskell..
Вступление
В качестве метода вывода типа Хиндли-Милнер может выводить типы переменных, выражений и функций из программ, написанных в совершенно нетипизированном стиле. Будучи зависимым от области видимости , он не ограничивается получением типов только из небольшой части исходного кода, а скорее из полных программ или модулей. Способность работать с параметрическими типами также является ядром систем типов многих языков функционального программирования . Впервые он был применен таким образом в языке программирования ML .
Происхождение является алгоритм вывода типа для простого типизированного лямбда - исчисления , который был разработан Haskell Curry и Роберт Feys в 1958 году [ править ] В 1969 году Дж Роджер Хиндли распространил эту работу и доказали , что их алгоритм всегда выводили наиболее общий тип. В 1978 году Robin Milner , [5] независимо от работы Хиндли, при условии , эквивалентный алгоритм, алгоритм W . В 1982 году Луис Дамас [4] окончательно доказал полноту алгоритма Милнера и расширил его для поддержки систем с полиморфными ссылками.
Мономорфизм против полиморфизма
В простом типизированном лямбда-исчислении типы являются либо константами атомарного типа, либо функциональными типами формы . Такие типы мономорфны . Типичными примерами являются типы, используемые в арифметических значениях:
3: Число добавить 3 4: Число добавить: Число -> Число -> Число
В отличие от этого, нетипизированное лямбда-исчисление вообще нейтрально по отношению к типизации, и многие из его функций могут быть осмысленно применены ко всем типам аргументов. Тривиальный пример - функция идентичности
- я бы Икс . Икс
который просто возвращает то значение, к которому применяется. Менее тривиальные примеры включают параметрические типы, такие как списки .
В то время как полиморфизм в целом означает, что операции принимают значения более чем одного типа, полиморфизм, используемый здесь, является параметрическим. В литературе также встречаются обозначения схем типов , подчеркивающие параметрическую природу полиморфизма. Кроме того, константы могут быть типизированы с помощью (количественно определенных) переменных типа. Например:
минусы: для всех. a -> Список a -> Список a ноль: на все. Перечислите а. id: для всех. а -> а
Полиморфные типы могут стать мономорфными путем последовательной замены их переменных. Примеры мономорфных экземпляров :
id ': String -> Stringnil ': Номер списка
В более общем смысле типы являются полиморфными, если они содержат переменные типа, тогда как типы без них являются мономорфными.
В отличие от систем типов, используемых, например, в Pascal (1970) или C (1972), которые поддерживают только мономорфные типы, HM разработан с упором на параметрический полиморфизм. Преемники упомянутых языков, такие как C ++ (1985), сосредоточились на различных типах полиморфизма, а именно на подтипах в связи с объектно-ориентированным программированием и перегрузкой . Хотя подтипирование несовместимо с HM, вариант систематической перегрузки доступен в основанной на HM системе типов Haskell.
Let-полиморфизм
При расширении вывода типа для простого типизированного лямбда-исчисления в сторону полиморфизма необходимо определить, когда получение экземпляра значения допустимо. В идеале это было бы разрешено при любом использовании связанной переменной, например:
(λ id. ... (id 3) ... (id "текст") ...) (λ x. x)
К сожалению, вывод типа в полиморфном лямбда-исчислении не разрешим. [6] Вместо этого HM предоставляет let-полиморфизм вида
пусть id = λ x. x in ... (id 3) ... (id "текст") ...
ограничение механизма связывания в расширении синтаксиса выражения. Инстанциированию подлежат только значения, связанные в конструкции let, т. Е. Являются полиморфными, в то время как параметры в лямбда-абстракциях рассматриваются как мономорфные.
Обзор
Оставшаяся часть статьи выглядит следующим образом:
- Определена система типов HM. Это делается путем описания системы дедукции, которая уточняет, какие выражения имеют какой тип, если таковые имеются.
- Оттуда он работает в направлении реализации метода вывода типа. После введения варианта вышеупомянутой дедуктивной системы, управляемого синтаксисом, он набрасывает эффективную реализацию (алгоритм J), в основном обращаясь к металогической интуиции читателя.
- Поскольку остается открытым, действительно ли алгоритм J реализует исходную систему вывода, вводится менее эффективная реализация (алгоритм W) и намекается ее использование в доказательстве.
- Наконец, обсуждаются дальнейшие темы, связанные с алгоритмом.
Одно и то же описание системы дедукции используется повсюду, даже для двух алгоритмов, чтобы сделать различные формы, в которых представлен метод HM, напрямую сопоставимыми.
Система типа Хиндли – Милнера
Систему типов можно формально описать с помощью правил синтаксиса, которые фиксируют язык для выражений, типов и т. Д. Представление здесь такого синтаксиса не слишком формально, поскольку оно написано не для изучения поверхностной грамматики , а, скорее, для изучения глубина грамматики и оставляет некоторые синтаксические детали открытыми. Такая форма представления обычная. Основываясь на этом, правила типов используются для определения того, как связаны выражения и типы. Как и прежде, форма немного либеральна.
Синтаксис
Выражения |
Типы |
Контекст и набор текста |
Переменные произвольного типа |
Типизируемые выражения - это в точности выражения лямбда-исчисления, расширенные с помощью let-выражения, как показано в соседней таблице. Скобки можно использовать для устранения неоднозначности выражения. Приложение имеет левую привязку и связывает сильнее, чем абстракция или конструкция let-in.
Типы синтаксически делятся на две группы: монотипы и политипы. [заметка 2]
Монотипии
Монотипия всегда обозначает определенный тип. Монотипиисинтаксически представлены как термины .
Примеры монотипов включают константы типа, такие как или же , и параметрические типы, такие как . Последние типы являются примерами применения функций типа, например, из множества, где верхний индекс указывает количество параметров типа. Полный набор функций типапроизвольно в HM [примечание 3], за исключением того, что он должен содержать не менее, тип функций. Для удобства его часто пишут инфиксной нотацией. Например, функция, отображающая целые числа в строки, имеет тип. Опять же, скобки могут использоваться для устранения неоднозначности выражения типа. Приложение связывает сильнее, чем инфиксная стрелка, которая связывает вправо.
Переменные типа допускаются как монотипы. Монотипы не следует путать с мономорфными типами, которые исключают переменные и допускают только основные термины.
Два монотипа равны, если у них одинаковые термины.
Политипы
Политипы (или схемы типов) - это типы, содержащие переменные, связанные нулем или несколькими кванторами для всех, например.
Функция с политипом может отображать себе любое значение того же типа, а функция идентификации является значением для этого типа.
Другой пример: - это тип функции, отображающей все конечные множества в целые числа. Функция , которая возвращает мощность набора будет значением этого типа.
Квантификаторы могут появляться только на верхнем уровне. Например, типисключается синтаксисом типов. Также в политипы входят монотипы, поэтому тип имеет общий вид, где это монотипия.
Равенство политипов зависит от переупорядочения количественной оценки и переименования количественно определяемых переменных (-конверсия). Кроме того, количественные переменные, не встречающиеся в монотипе, могут быть опущены.
Контекст и набор текста
Чтобы осмысленно объединить все еще непересекающиеся части (синтаксические выражения и типы), необходима третья часть: контекст. Синтаксически контекст - это список пар, называемые присвоениями , предположениями или привязками , каждая пара указывает эту переменную значенияимеет тип . Все три части вместе дают оценку набора в форме, заявляя, что при предположениях , выражение имеет тип .
Переменные произвольного типа
В виде , символ квантификатор, связывающий переменные типа в монотипии . Переменныеназываются квантифицированными, и любое вхождение переменной квантифицированного типа вназывается связанными, и все переменные несвязанного типа вназываются бесплатными . Дополнительно к количественной оценке в политипах переменные типа также могут быть связаны, встречаясь в контексте, но с обратным эффектом в правой части . В этом случае такие переменные ведут себя как константы типов. Наконец, переменная типа может быть юридически несвязанной при типизации, и в этом случае все они неявно количественно определены.
Наличие как связанных, так и несвязанных переменных типа немного необычно для языков программирования. Часто все переменные типа неявно обрабатываются с количественной оценкой. Например, в Прологе нет предложений со свободными переменными . Скорее всего, в Haskell, [примечание 4], где все переменные типа неявно встречаются количественно, т.е. тип Haskell a -> a
означаетздесь. Связанный, а также очень необычный эффект связывания правой стороны заданий.
Как правило, сочетание переменных связанного и несвязанного типа происходит из-за использования в выражении свободных переменных. В функции константы K =дает пример. Имеет монотипию. Можно заставить полиморфизм. Здесь имеет тип . Бесплатная переменная монотипии происходит от типа переменной связаны в окружающей области. имеет тип . Можно представить себе переменную свободного типа в виде быть связанным в виде . Но такой объем не может быть выражен в HM. Скорее привязка реализуется контекстом.
Тип заказа
Полиморфизм означает, что одно и то же выражение может иметь (возможно, бесконечно) много типов. Но в этой системе типов эти типы не совсем не связаны между собой, а скорее управляются параметрическим полиморфизмом.
Например, личность могу иметь как его тип, а также или же и многие другие, но не . Самый общий тип этой функции -, в то время как другие более конкретны и могут быть производными от общего путем последовательной замены другого типа для параметра типа , то есть количественной переменной. Контрпример не работает, потому что замена непоследовательна.
Последовательную замену можно сделать формальной, применив замену сроку вида , написано . Как следует из примера, подстановка не только сильно связана с порядком, который выражает, что тип более или менее особенный, но также с общей количественной оценкой, которая позволяет применять замену.
Правило специализации |
Формально в HM тип более общий, чем , формально , если некоторая количественная переменная в последовательно заменяется таким образом, чтобы как показано на боковой панели. Этот порядок является частью определения типа системы типов.
В нашем предыдущем примере, применяя замену приведет к .
В то время как замена количественной переменной мономорфным (основным) типом проста, замена политипа имеет некоторые подводные камни, вызванные наличием свободных переменных. В частности, нельзя заменять несвязанные переменные. Здесь они рассматриваются как константы. Кроме того, количественная оценка может происходить только на верхнем уровне. Подставляя параметрический тип, нужно поднять его кванторы. Таблица справа уточняет правило.
В качестве альтернативы, рассмотрите эквивалентную нотацию для политипов без кванторов, в которой количественные переменные представлены другим набором символов. В таких обозначениях специализация сводится к простой последовательной замене таких переменных.
Соотношение это частичный порядок и это его самый маленький элемент.
Основной тип
Хотя специализация схемы типов является одним из видов использования порядка, она играет важную вторую роль в системе типов. Вывод типа с помощью полиморфизма сталкивается с проблемой суммирования всех возможных типов, которые может иметь выражение. Порядок гарантирует, что такое резюме существует как наиболее общий тип выражения.
Подстановка в наборах
Порядок типов, определенный выше, может быть расширен до типизации, потому что подразумеваемая полная количественная оценка типизации обеспечивает последовательную замену:
Вопреки правилу специализации, это не часть определения, а, как и неявная общая количественная оценка, скорее, следствие правил типов, определенных далее. Переменные произвольного типа в типизации служат заполнителями для возможного уточнения. Эффект привязки среды к свободным переменным типа в правой части который запрещает их замену в правиле специализации, опять же, что замена должна быть последовательной и должна включать в себя всю типизацию.
В этой статье мы обсудим четыре различных набора правил:
- декларативная система
- синтаксическая система
- алгоритм J
- алгоритм W
Дедуктивная система
Синтаксис правил |
Синтаксис HM переносится в синтаксис правил вывода, которые формируют тело формальной системы , с использованием типизации в качестве суждений . Каждое из правил определяет, какой вывод из каких посылок можно сделать. В дополнение к судебным решениям, некоторые дополнительные условия, введенные выше, также могут использоваться в качестве предпосылок.
Доказательство с использованием правил - это последовательность суждений, в которой все предпосылки перечисляются перед выводом. Примеры ниже показывают возможный формат доказательств. Слева направо каждая строка показывает вывод, применяемого правила и посылки, либо путем ссылки на более раннюю строку (номер), если посылка является суждением, либо путем явного выражения предиката.
Правила набора
Декларативная система правил |
В боковом поле показаны правила вывода системы типов HM. Условно правила можно разделить на две группы:
Первые четыре правила (доступ к переменной или функции), ( приложение , т.е. вызов функции с одним параметром),( абстракция , т.е. объявление функции) и(объявление переменной) сосредоточены вокруг синтаксиса, представляя одно правило для каждой формы выражения. Их значение очевидно с первого взгляда, поскольку они разбирают каждое выражение, доказывают свои подвыражения и, наконец, объединяют отдельные типы, найденные в предпосылках, с типом в заключении.
Вторая группа образована двумя оставшимися правилами. а также . Они обрабатывают специализацию и обобщение типов. Хотя правилодолжно быть ясно из раздела о специализации выше ,дополняет первое, работая в противоположном направлении. Это позволяет обобщать, т. Е. Количественно определять переменные монотипа, не связанные в контексте.
Следующие два примера демонстрируют систему правил в действии. Поскольку даны и выражение, и тип, они используются для проверки типов правил.
Пример : доказательство где , можно было бы написать
Пример : чтобы продемонстрировать обобщение, показано ниже:
Let-полиморфизм
Не видимый сразу, набор правил кодирует правило, при котором тип может быть обобщен или нет путем слегка изменяющегося использования моно- и политипов в правилах. а также . Помни это а также обозначают поли- и монотипы соответственно.
В правиле , переменная значения параметра функции добавляется к контексту с мономорфным типом через посылку , а в правиле , переменная входит в окружение в полиморфной форме . Хотя в обоих случаях наличие в контексте предотвращает использование правила обобщения для любой свободной переменной в присвоении, это правило заставляет тип параметра в -выражение, чтобы оставаться мономорфным, в то время как в let-выражении переменная может быть введена полиморфной, что делает возможной специализацию.
Как следствие этого правила, нельзя ввести, так как параметр находится в мономорфном положении, а имеет тип , так как был введен в let-выражение и поэтому считается полиморфным.
Правило обобщения
Правило обобщения также заслуживает внимательного изучения. Здесь всеобъемлющая количественная оценка, заложенная в предпосылку просто перемещается в правую часть по итогам. Это возможно, так какне возникает в контексте. Опять же, хотя это делает правило обобщения правдоподобным, на самом деле это не следствие. Напротив, правило обобщения является частью определения системы типов HM и следствием неявной общей количественной оценки.
Алгоритм вывода
Теперь, когда доступна система дедукции HM, можно представить алгоритм и проверить его на соответствие правилам. В качестве альтернативы можно было бы вывести его, внимательно изучив, как правила взаимодействуют и формируются доказательства. Это делается в оставшейся части этой статьи, уделяя особое внимание возможным решениям, которые можно принять при проверке типизации.
Степени свободы выбора правил
Выделяя точки в доказательстве, где решение вообще невозможно, первая группа правил, сосредоточенная вокруг синтаксиса, не оставляет выбора, поскольку каждому синтаксическому правилу соответствует уникальное правило типизации, которое определяет часть доказательства, а между заключением и помещения этих фиксированных частей цепочек а также могло произойти. Такая цепочка также могла существовать между завершением доказательства и правилом для наивысшего выражения. Все доказательства должны иметь такую набросанную форму.
Поскольку единственный выбор в доказательстве в отношении выбора правила - это а также цепочки, форма доказательства наводит на вопрос, можно ли его уточнить, где эти цепочки могут не понадобиться. На самом деле это возможно и приводит к варианту системы правил без таких правил.
Система правил, ориентированная на синтаксис
Система синтаксических правил |
Обобщение |
Современная трактовка HM использует чисто синтаксически управляемую систему правил, предложенную Клементом [7] в качестве промежуточного шага. В этой системе специализация расположена сразу после оригинальной правила и слились с ним, в то время как обобщение становится частью правило. Здесь также определяется обобщение, чтобы всегда производить наиболее общий тип путем введения функции, который позволяет количественно оценить все переменные монотипа, не связанные .
Формально, чтобы подтвердить, что эта новая система правил эквивалентен оригиналу , нужно показать, что , который распадается на два подконтрольных доказательства:
- ( Последовательность )
- ( Полнота )
Хотя согласованность можно увидеть, разложив правила а также из в доказательства в , вероятно, видно, что неполный, так как нельзя показать в , например, но только . Однако доказуема лишь немного более слабая версия полноты [8] , а именно
подразумевая, можно получить главный тип для выражения в позволяя в итоге обобщить доказательство.
Сравнение а также , теперь в суждениях всех правил фигурируют только монотипии. Кроме того, форма любого возможного доказательства с помощью системы дедукции теперь идентична форме выражения (оба они выглядят как деревья ). Таким образом, выражение полностью определяет форму доказательства. В форма, вероятно, будет определяться с соблюдением всех правил, кроме а также , которые позволяют строить произвольно длинные ответвления (цепочки) между остальными узлами.
Степени свободы, воплощающие правила
Теперь, когда форма доказательства известна, мы уже близки к формулировке алгоритма вывода типов. Поскольку любое доказательство для данного выражения должно иметь одинаковую форму, можно предположить, что монотипии в суждениях доказательства не определены, и подумать, как их определить.
Здесь играет роль порядок замещения (специализации). Хотя на первый взгляд невозможно определить типы локально, есть надежда, что их можно уточнить с помощью порядка при обходе дерева доказательства, дополнительно предполагая, поскольку результирующий алгоритм должен стать методом вывода, что Тип в любом помещении будет определен как лучший. А на самом деле можно, глядя на правила предлагает:
- : Критический выбор . На данный момент ничего не известно о, поэтому можно предположить только самый общий тип, а именно . План состоит в том, чтобы специализировать тип, если в этом возникнет необходимость. К сожалению, политип здесь не разрешен, поэтому некоторыенужно сделать на данный момент. Чтобы избежать нежелательных захватов, безопасным выбором является переменная типа, еще не прошедшая проверку. Кроме того, следует иметь в виду, что этот монотип еще не закреплен, но может быть уточнен.
- : Выбор в том, как доработать . Потому что любой выбор типаздесь, в зависимости от использования переменной, которая не известна локально, самая безопасная ставка - самая общая. Используя тот же метод, что и выше, можно создать экземпляры всех количественных переменных в со свежими переменными монотипии, снова оставляя их открытыми для дальнейшего уточнения.
- : Правило не оставляет выбора. Сделанный.
- : Только правило приложения может заставить уточнять переменные, "открытые" на данный момент.
Первая посылка заставляет результат вывода иметь форму .
- Если это так, то хорошо. Позже его можно будет выбрать за результат.
- В противном случае это может быть открытая переменная. Затем это может быть уточнено до требуемой формы с двумя новыми переменными, как и раньше.
- В противном случае проверка типа завершится неудачно, потому что первая предпосылка выявила тип, который не является и не может быть преобразован в тип функции.
Вторая посылка требует, чтобы предполагаемый тип был равен первого помещения. Теперь есть два, возможно, разных типа, возможно, с переменными открытого типа, которые можно сравнивать и приравнивать, если это возможно. Если это так, уточнение найдено, а если нет, ошибка типа обнаруживается снова. Известен эффективный метод «уравнять два члена» путем подстановки, объединение Робинсона в сочетании с так называемым алгоритмом поиска объединения .
Вкратце резюмируя алгоритм поиска объединения, учитывая набор всех типов в доказательстве, он позволяет сгруппировать их вместе в классы эквивалентности с помощью процедуры и выбрать представителя для каждого такого класса с помощью процедура. Подчеркивая слово « процедура» как « побочный эффект» , мы явно выходим из области логики, чтобы подготовить эффективный алгоритм. Представитель определяется так, что если оба а также являются переменными типа, то представитель произвольно является одним из них, но при объединении переменной и члена терм становится представителем. Предполагая, что есть реализация union-find, можно сформулировать объединение двух монотипов следующим образом:
унифицировать (ta, tb): ta = найти (ta) tb = найти (tb) если оба ta, tb являются членами формы D p1..pn с идентичными D, n, тогда унифицируйте (ta [i], tb [i]) для каждого соответствующего i- го параметра, иначе, если хотя бы один из ta, tb является введите переменную, затем союз (ta, tb) еще ошибка "типы не совпадают"
Теперь, когда имеется набросок алгоритма вывода, в следующем разделе дается более формальное представление. Это описано в Milner [2] P. 370 ff. как алгоритм J.
Алгоритм J
Алгоритм J |
Представление алгоритма J является неправильным использованием обозначения логических правил, поскольку оно включает побочные эффекты, но позволяет проводить прямое сравнение с выражая в то же время эффективную реализацию. Теперь правила определяют процедуру с параметрами. уступающий в заключении, где оформление помещения происходит слева направо.
Процедура специализируется на политипе копируя термин и последовательно заменяя переменные связанного типа новыми переменными монотипии. ''создает новую переменную монотипа. Вероятный,должен скопировать тип, вводя новые переменные для количественной оценки, чтобы избежать нежелательных захватов. В целом алгоритм теперь всегда делает наиболее общий выбор, оставляя специализацию на усмотрение унификации, которая сама по себе дает наиболее общий результат. Как отмечалось выше , окончательный результат должен быть обобщен на в конце, чтобы получить наиболее общий тип для данного выражения.
Поскольку процедуры, используемые в алгоритме, имеют стоимость около O (1), общая стоимость алгоритма близка к линейной по размеру выражения, для которого должен быть выведен тип. Это резко контрастирует со многими другими попытками вывести алгоритмы вывода типов, которые часто оказывались NP-трудными , если не неразрешимыми в отношении завершения. Таким образом, HM работает так же хорошо, как и лучшие полностью информированные алгоритмы проверки типов. Проверка типов здесь означает, что алгоритм не должен искать доказательства, а только проверять данное.
Эффективность немного снижается, потому что привязка переменных типа в контексте должна поддерживаться, чтобы позволить вычисление и включите проверку событий, чтобы предотвратить создание рекурсивных типов во время. Примером такого случая является, для которого с помощью HM нельзя получить тип. На практике типы - это небольшие сроки и не создают расширяющихся структур. Таким образом, при анализе сложности их можно рассматривать как постоянные, сохраняя затраты O (1).
Доказательство алгоритма
В предыдущем разделе при наброске алгоритма на его доказательство намекнули с помощью металогической аргументации. Хотя это приводит к эффективному алгоритму J, неясно, правильно ли алгоритм отражает системы дедукции D или S, которые служат семантической базовой линией.
Наиболее важным моментом в приведенной выше аргументации является уточнение переменных монотипа, связанных контекстом. Например, алгоритм смело изменяет контекст при выводе, например,, потому что переменная монотипа добавлена в контекст для параметра позже необходимо доработать до при обращении с приложением. Проблема в том, что правила дедукции не допускают такого уточнения. Утверждение, что уточненный тип мог быть добавлен раньше вместо переменной монотипа, в лучшем случае является уловкой.
Ключом к достижению формально удовлетворительного аргумента является правильное включение контекста в уточнение. Формально типизация совместима с заменой переменных свободного типа.
Таким образом, уточнить свободные переменные - значит уточнить всю типизацию.
Алгоритм W
Алгоритм W |
Отсюда проверка алгоритма J приводит к алгоритму W, который устраняет только побочные эффекты, налагаемые процедурой. явным, выражая его серийный состав с помощью подстановок . Представление алгоритма W на боковой панели по-прежнему использует побочные эффекты в операциях, выделенных курсивом, но теперь они ограничиваются генерацией новых символов. Форма суждения, обозначающая функцию с контекстом и выражением в качестве параметра, создающего монотипию вместе с заменой. это бесплатная версия производит замену, которая является наиболее общим объединителем .
В то время как алгоритм W , как правило , считается алгоритм НМ и часто непосредственно после того, как представлены системы правил в литературе, его цель описывается Milner [2] на P. 369 следующим образом :
- В нынешнем виде W вряд ли является эффективным алгоритмом; замены применяются слишком часто. Он был разработан, чтобы помочь доказать надежность. Теперь мы представляем более простой алгоритм J, который имитирует W в точном смысле.
Хотя он считал W более сложным и менее эффективным, он представил его в своей публикации перед J. Он имеет свои достоинства, когда побочные эффекты отсутствуют или нежелательны. Кстати, W также нужен для доказательства полноты, которая учитывается им при доказательстве правильности.
Обязательства по доказательству
Прежде чем сформулировать обязательства по доказательству, необходимо подчеркнуть отклонение между системами правил D и S и представленными алгоритмами.
В то время как описанная выше разработка неправильно использовала монотипы как «открытые» доказательные переменные, возможность того, что правильные переменные монотипа могут быть повреждены, была устранена путем введения новых переменных и надежды на лучшее. Но есть одна загвоздка: одно из обещаний заключалось в том, что эти новые переменные будут «учитываться» как таковые. Это обещание алгоритм не выполняет.
Имея контекст , выражение нельзя ввести ни или же , но алгоритмы приходят к типу , где W дополнительно доставляет замену , что означает, что алгоритм не может обнаружить все ошибки типов. Это упущение может быть легко исправлено более тщательным различением переменных доказательства и переменных монотипии.
Авторы хорошо знали о проблеме, но решили не исправлять. Можно предположить, что за этим стоит прагматическая причина. Хотя более правильная реализация вывода типов позволила бы алгоритму иметь дело с абстрактными монотипами, они не были необходимы для предполагаемого приложения, где ни один из элементов в уже существующем контексте не имеет свободных переменных. В этом свете ненужное усложнение было отброшено в пользу более простого алгоритма. Остающийся недостаток заключается в том, что доказательство алгоритма относительно системы правил менее общее и может быть выполнено только для контекстов с как побочное условие.
Дополнительное условие в обязательстве полноты касается того, как вычет может дать много типов, в то время как алгоритм всегда производит один. В то же время побочное условие требует, чтобы предполагаемый тип был самым общим.
Чтобы правильно доказать обязательства, нужно сначала усилить их, чтобы позволить активировать лемму о подстановке, распределяющую подстановку через а также . Отсюда доказательства проводятся индукцией по выражению.
Еще одно обязательство по доказательству - это сама лемма о замене, то есть замена типизации, которая, в конце концов, устанавливает все-квантификацию. Последнее невозможно формально доказать, так как такого синтаксиса нет.
Расширения
Рекурсивные определения
Чтобы сделать программирование практичным , необходимы рекурсивные функции. Центральным свойством лямбда-исчисления является то, что рекурсивные определения не доступны напрямую, но вместо этого могут быть выражены с помощью комбинатора с фиксированной точкой . Но, к сожалению, комбинатор фиксированных точек не может быть сформулирован в типизированной версии лямбда-исчисления без катастрофического воздействия на систему, как показано ниже.
Правило набора
В исходной статье [4] показано, что рекурсия может быть реализована с помощью комбинатора. Таким образом, возможное рекурсивное определение может быть сформулировано как.
В качестве альтернативы возможно расширение синтаксиса выражения и дополнительное правило ввода:
где
в основном слияние а также при включении рекурсивно определенных переменных в монотипные позиции, где они встречаются слева от но как политипы справа от него.
Последствия
Несмотря на то, что вышеизложенное является простым, за это приходится платить.
Теория типов связывает лямбда-исчисление с вычислениями и логикой. Приведенная выше простая модификация влияет на оба:
- Свойство строгой нормализации становится недействительным, потому что могут быть сформулированы неограничивающие условия.
- Логика рушится, потому что типстановится заселенным .
Перегрузка
Перегрузка означает, что разные функции по-прежнему могут определяться и использоваться с одним и тем же именем. Большинство языков программирования, по крайней мере, обеспечивают перегрузку встроенными арифметическими операциями (+, <и т. Д.), Чтобы позволить программисту писать арифметические выражения в одной и той же форме, даже для разных числовых типов, таких как int
или real
. Поскольку сочетание этих разных типов в одном выражении также требует неявного преобразования, перегрузка, особенно для этих операций, часто встроена в сам язык программирования. В некоторых языках эта функция обобщена и доступна пользователю, например, в C ++.
В то время как специальная перегрузка была предотвращена в функциональном программировании из-за затрат на вычисления как при проверке типов, так и при выводе [ необходима цитата ] , было введено средство систематизации перегрузки, которое по форме и именованию напоминает объектно-ориентированное программирование, но работает на один уровень выше. . «Экземпляры» в этой систематике - это не объекты (т. Е. На уровне значений), а скорее типы. В примере быстрой сортировки, упомянутом во введении, используется перегрузка в заказах со следующей аннотацией типа в Haskell:
quickSort :: Ord a => [ a ] -> [ a ]
Здесь тип a
не только полиморфен, но также ограничен как экземпляр некоторого класса типа Ord
, который предоставляет предикаты порядка <
и >=
используется в теле функции. Соответствующие реализации этих предикатов затем передаются в quicksorts в качестве дополнительных параметров, как только быстрая сортировка используется для более конкретных типов, обеспечивая единственную реализацию перегруженной функции quickSort.
Поскольку «классы» допускают только один тип в качестве аргумента, результирующая система типов по-прежнему может обеспечивать вывод. Кроме того, классы типов могут быть оснащены каким-либо порядком перегрузки, позволяющим организовать классы в виде решетки .
Типы высшего порядка
Параметрический полиморфизм подразумевает, что сами типы передаются как параметры, как если бы они были правильными значениями. Передается в качестве аргументов в соответствующие функции, а также в «функции типов», как в «параметрических» константах типов, приводит к вопросу о том, как более правильно типизировать сами типы. Типы высшего порядка используются для создания еще более выразительной системы типов.
К сожалению, только унификация больше не разрешима при наличии метатипов, что делает невозможным вывод типа в этой степени общности. Кроме того, предположение о типе всех типов, который включает себя в качестве типа, приводит к парадоксу, как и в случае множества всех множеств, поэтому нужно действовать поэтапно по уровням абстракции. Исследования в области лямбда-исчисления второго порядка , проведенные на один шаг вверх, показали, что вывод типов неразрешим в этой общности.
В Haskell были введены части одного дополнительного уровня под названием kind , где он используется для ввода монад . Виды остаются неявными, работая за кулисами во внутренней механике расширенной системы типов.
Подтип
Попытки совместить выделение подтипов и вывод типов вызвали некоторое разочарование. Системы типов с подтипами, обеспечивающие объектно-ориентированный стиль, например, Cardelli [9] is system , отсутствие вывода типа. В некоторой степени HM можно модифицировать для работы с записями. [10] Идея состоит в том, чтобы расширить данную запись по метке поля и ценность к новой записи с использованием синтаксиса . Затем порядок типов HM может быть применен к таким расширениям так же, как если бы они были парами, если система типов дополнительно ограничивает в этом синтаксисе быть записью.
Заметки
- ^ Вывод типа Хиндли – Милнера завершен DEXPTIME . Фактически, простое решение, является ли программа ML типизированной (без необходимости делать вывод о типе), само по себе является DEXPTIME-завершенным . Нелинейное поведение проявляется, но в основном на патологических воздействиях. Таким образом, теоретические доказательства сложности, сделанные Mairson (1990) и Kfoury, Tiuryn & Urzyczyn (1990), стали неожиданностью для исследовательского сообщества.
- ^ Политипы в оригинальной статье называются «схемами типов».
- ^ Параметрические типыне присутствовали в исходной статье о HM и не нужны для представления метода. Ни одно из приведенных ниже правил вывода не учитывает и даже не учитывает их. То же самое верно и для непараметрических «примитивных типов» в указанной статье. Все механизмы вывода полиморфных типов могут быть определены без них. Они включены сюда не только для примеров, но и потому, что суть HM заключается в параметрических типах. Это происходит от типа функции, зашитый в правилах вывода ниже, который уже имеет два параметра и представлен здесь как частный случай.
- ^ Haskell предоставляет расширение языка ScopedTypeVariables, позволяющее вводить все количественные переменные типа в область видимости.
Рекомендации
- ^ Хиндли, Дж. Роджер (1969). "Основная схема типов объекта в комбинаторной логике". Труды Американского математического общества . 146 : 29–60. DOI : 10.2307 / 1995158 . JSTOR 1995 158 .
- ^ а б в Милнер, Робин (1978). «Теория полиморфизма типов в программировании». Журнал компьютерных и системных наук . 17 (3): 348–374. CiteSeerX 10.1.1.67.5276 . DOI : 10.1016 / 0022-0000 (78) 90014-4 .
- ^ Дамас, Луис (1985). Присвоение типов в языках программирования (кандидатская диссертация). Эдинбургский университет. hdl : 1842/13555 . CST-33-85.
- ^ а б в Дамас, Луис; Милнер, Робин (1982). Основные схемы типов функциональных программ (PDF) . 9-й симпозиум по принципам языков программирования (POPL'82). ACM. С. 207–212. DOI : 10.1145 / 582153.582176 . ISBN 978-0-89791-065-1.
- ^ Милнер, Робин (1978), "Теория типа полиморфизма в программировании", журнал компьютерных и системных наук , 17 (3): 348-375, DOI : 10,1016 / 0022-0000 (78) 90014-4
- ^ Уэллс, Дж. Б. (1994). «Типизация и проверка типов в лямбда-исчислении второго порядка эквивалентны и неразрешимы» . Материалы 9-го ежегодного симпозиума IEEE по логике в компьютерных науках (LICS) . С. 176–185. DOI : 10.1109 / LICS.1994.316068 . ISBN 0-8186-6310-3. S2CID 15078292 .
- ^ Клемент (1986). Простой прикладной язык: Mini-ML . LFP'86. ACM. DOI : 10.1145 / 319838.319847 . ISBN 978-0-89791-200-6.
- ^ Воан, Джефф (23 июля 2008 г.) [5 мая 2005 г.]. «Доказательство правильности алгоритма вывода типа Хиндли-Милнера» (PDF) . Архивировано из оригинального (PDF) 24 марта 2012 года. Цитировать журнал требует
|journal=
( помощь ) - ^ Карделли, Лука; Мартини, Симона; Митчелл, Джон С .; Щедров, Андре (1994). «Расширение системы F с выделением подтипов». Информация и вычисления, т. 9 . Северная Голландия, Амстердам. С. 4–56. DOI : 10.1006 / inco.1994.1013 .
- ^ Даан Лейен, Расширяемые записи с ограниченными метками , Институт информационных и вычислительных наук, Утрехтский университет, проект, редакция: 76, 23 июля 2005 г.
- Майерсон, Гарри Г. (1990). «Решение о типизации машинного обучения завершено для детерминированного экспоненциального времени». Материалы 17-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования - POPL '90 . Материалы 17-го симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования . POPL '90. ACM. С. 382–401. DOI : 10.1145 / 96709.96748 . ISBN 978-0-89791-343-0. S2CID 75336 .
- Kfoury, AJ; Тюрин, Дж .; Уржичин, П. (1990). Типизация машинного обучения является полной . Конспект лекций по информатике . CAAP '90. 431 . С. 206–220. DOI : 10.1007 / 3-540-52590-4_50 . ISBN 978-3-540-52590-5.
Внешние ссылки
- Грамотная реализация алгоритма W на Haskell вместе с его исходным кодом на GitHub .
- Простая реализация алгоритма Хиндли-Милнера на Python .