2014-02-13
698
Полиморфизм
Система типов по Карри обеспечивает полиморфизм, в том смысле, что терм может иметь различные типы. Необходимо различать концепции полиморфизма и перегрузки. Оба этих термина означают, что выражение может иметь несколько типов. Однако в случае полиморфизма все типы сохраняют струкурное сходство. Например, функция идентичности может иметь тип σ —> σ, τ —> τ или (σ —> τ)—> (σ —> τ). При перегрузке функция может иметь различные типы, не связанные друг с другом структурным сходством.
Рассмотренная система типов приводит к некоторым ограничениям на полиморфизм. Например, приемлемо следующее выражение:
if (λx. x) true then (λx.x) 1else 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-полиморфизм.
