10.2 Полиморфизм

Система типов по Карри обеспечивает полиморфизм, в том смысле, что терм может иметь различные типы. Необходимо различать концепции полиморфизма и перегрузки. Оба этих термина означают, что выражение может иметь несколько типов. Однако в случае полиморфизма все типы сохраняют струкурное сходство. Например, функция идентичности может иметь тип σ —> σ, τ —> τ или (σ —>τ) —> (σ —> τ ). При перегрузке функция может иметь различные типы, не связанные друг с другом структурным сходством.

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

Рассмотренная система типов приводит к некоторым ограничениям на полиморфизм. Например, приемлемо следующее выражение:

if (λx. x) true then (λx.x) 1 else 0

Если использовать правила типизации, то можно получить, что это выражение имеет тип int. Два экземпляра функции идентичности имеют типы bool —>bool и int —> int соответственно.

Рассмотрим выражение:

let I = λx. x in if I true then I 1 else 0

Согласно определению, это иной способ записи для

(λI. if I true then I 1 else 0) (λx. x)

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

Для преодоления этого ограничения добавим правило типизации, в котором let-конструкции рассматривается как первичная:

Это правило определяет let-полиморфизм.

10.2.2 Наиболее общие типы

Некоторые выражения не имеют типа, например, λf. f f или λf. (f true, f.1) Типизируемые выражения обычно имеют много типов, хотя некоторые имеют только один.

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

Введем понятие типовых переменных. Типы могут быть сконструированы с помощью применения конструкторов типа либо к типовым константам, либо к переменным. Будем использовать буквы α и β для типовых переменных, а σ и τ - для произвольных типов. Определим понятие замены типовой переменной на некоторый тип. Будем использовать ту же нотацию, что и при подстановке термов. Например:

(σ —> bоо1)[ σ := (σ —> τ)] = (σ —> τ)—> bool

Расширим это определение, добавив параллельные подстановки:

Можно рассматривать типовые константы как 0-арные конструкторы, т. е. считать, что int задается как int (). Имея определение подстановки, можно счиать, что тип σ является более общим, чем тип σ' и записывать этот факт как . Это отношение выполняется тогда и только тогда, когда существует набор подстановок θ такой, что σ' = σ θ. Например:

Имеет место:

Теорема 4. Каждый типизируемый терм имеет некоторый основной тип, т. е. если Т :: τ, то существует некоторый σ, такой что Т :: σ и для любого σ', если Т :: σ', то .

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