John Harrison - Введение в функциональное программирование (1108517), страница 13
Текст из файла (страница 13)
Зафиксировав t, докажемприведённое выше утверждение для всевозможных Γ и ∆, поскольку в ходе шагаиндукции для абстракций эти множества изменяются. Если t — переменная,справедливо t : σ ∈ Γ, из чего следует и t : σ ∈ ∆, откуда получаем требуемое.Если t — константа, желаемый вывод очевиден, поскольку множество константи их типов не зависит от контекста. В случае терма t, имеющего вид комбинациитермов s u, для некоторого типа τ выполняется Γ ` s : τ → σ и Γ ` u : τ .
Согласноиндуктивному предположению, ∆ ` s : τ → σ и ∆ ` u : τ , откуда также получаемтребуемое. Наконец, если терм t представляет собой абстракцию λx.s, то согласнопоследнему правилу типизации σ имеет вид τ → τ 0 , а также справедливо, что Γ ∪42Глава 4. Типы4.2. Полиморфизм{x : τ } ` s : τ 0 . Так как Γ ⊆ ∆, мы получаем Γ ∪ {x : τ } ⊆ ∆ ∪ {x : τ }, откуда поиндуктивному предположению ∆ ∪ {x : τ } ` s : τ 0 . Применяя правило типизацииабстракций, получаем требуемое. Во-вторых, элементы контекста, представляющие переменные, которые неявляются свободными в заданном терме, могут игнорироваться.Лемма 4.2 Если Γ ` t : σ, то справедливо также Γt ` t : σ, где Γt содержитисключительно свободные переменные терма t (Γt = {x : α | x : α ∈ Γ и x ∈ F V (t)}).Доказательство: Аналогично предыдущей лемме, докажем наше утверждениедля произвольного контекста Γ и соответствующего ему Γt путём структурнойиндукции по t.
Если t — переменная, то Γ ` t : σ требует наличия в контекстеэлемента x : σ. Согласно первому правилу типизации {x : σ} ` x : σ, что итребуется. Тип константы не зависит от контекста, так что лемма справедливаи в этом случае. Если терм t представляет собой комбинацию термов вида s u,то для некоторого τ справедливо Γ ` s : τ → σ и Γ ` u : τ . Согласно индуктивномупредположению, Γs ` s : τ → σ и Γu ` u : τ . Согласно лемме о монотонности,получаем Γsu ` s : τ → σ и Γsu ` u : τ , поскольку F V (s u) = F V (s) ∪ F V (u).Применив правило вывода типа комбинации термов, получаем Γsu ` t : σ.
Наконец,если t имеет вид λx. s, это подразумевает Γ ∪ {x : τ } ` s : τ 0 , где σ имеетформу τ → τ 0 . Согласно индуктивному предположению, (Γ ∪ {x : τ })s ` s : τ 0 ,откуда (Γ ∪ {x : τ })s − {x : τ } ` (λx. s) : σ. Теперь нам требуется лишь отметить,что (Γ ∪ {x : τ })s − {x : τ } ⊆ Γt и ещё раз применить лемму о монотонности. Приступим к доказательству основного результата этого раздела.Теорема 4.3 (О сохранении типа) Если Γ ` t : σ и t −→ t0 , то из этого следует,ηчто Γ ` t0 : σ.Доказательство: Поскольку по условию теоремы терм t является η-редексом,он должен иметь структуру (λx. t x), причём x 6∈ F V (t).
Следовательно, еготип может быть выведен лишь из последнего правила типизации, при этом σимеет вид τ → τ 0 , и справедливо {x : τ } ` (t x) : τ 0 . Дальнейший анализтребует применения правила вывода типа комбинаций. Поскольку контекстможет содержать не более одного утверждения о типе каждой переменной,справедливо {x : τ } ` t : τ → τ 0 . Так как по условию x 6∈ F V (t), то применивлемму 4.2, получаем ` t : τ → τ 0 , что и требовалось. Собрав воедино результаты аналогичных доказательств для другихпреобразований, получаем, что если Γ ` t : σ и t −→ t0 , то выполняетсятакже Γ ` t0 : σ.
Важность этого вывода в том, что если бы правила вычислений,применяемые в ходе исполнения программы, могли изменять типы выражений, этоподорвало бы основы статической типизации.4.2ПолиморфизмТипизация по Карри предоставляет в наше распоряжение разновидностьполиморфизма, позволяя назначить заданному терму различные типы. Следуетразличать схожие понятия полиморфизма и перегрузки. Оба они подразумевают,434.2. ПолиморфизмГлава 4. Типычто выражение может иметь множество типов. Однако, в случае полиморфизма всеэти типы структурно связаны друг с другом, так что допустимы любые из них,удовлетворяющие заданному образцу.
Например, тождественной функции можноназначить тип σ → σ, или τ → τ , либо даже (σ → τ ) → (σ → τ ), но все они имеютодинаковую структуру. С другой стороны, суть перегрузки в том, что заданнаяфункция может иметь различные типы, структура которых может различаться, либоже допустимо лишь ограниченное множество типов. Например функции + можетбыть позволено иметь тип int → int → int либо f loat → f loat → f loat, но не bool →bool → bool.5 Ещё одним близким понятием являются подтипы, представляющиесобой более жёсткую форму перегрузки.
Введение подтипов позволяет трактоватьнекоторый тип как подмножество другого. Однако, этот подход на практикеоказывается куда сложнее, чем кажется на первый взгляд.64.2.1Проблемы let-полиморфизмаК сожалению, определённая выше система типов накладывает некоторыенежелательные ограничения на полиморфизм.
Например, следующее выражениеабсолютно корректно:if (λx. x) true then (λx. x) 1 else 0Докажем, что это выражение может быть типизировано согласно нашимправилам. Предположим, что константам можно назначить типы в пустом контексте,и что мы можем двукратно применить правило типизации комбинации термов дляназначения типа if (принимая во внимание, что выражение вида if b then t1 else t2является всего лишь сокращённой записью для COND b t1 t2 ).{x : int} ` x : int{x : bool} ` x : bool` (λx. x) : bool → bool ` true : bool ` (λx.
x) : int → int ` 1 : int` (λx. x) true : bool` (λx. x) 1 : int` 0 : int` 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)Нетрудно убедиться, что тип этого выражения не может быть выведен врамках наших правил. Мы имеем единственный экземпляр тождественной функции,5Стрейчи, которому принадлежит авторство понятия полиморфизма, использовал терминыпараметрический и ad hoc полиморфизм вместо принятых в данном пособии терминов полиморфизми перегрузка соответственно.6Например, если тип α является подтипом α0 , должен ли тип α → β считаться подтипом α0 → βили наоборот? В зависимости от конкретной ситуации, более предпочтительной оказывается либопервая, либо вторая интерпретация («ковариантность» либо «контравариантность» типов).44Глава 4. Типы4.2.
Полиморфизмкоторому должны назначить единственный тип. Подобное ограничение на практикенеприемлемо, поскольку функциональное программирование предполагает частоеиспользование let. Если правила типизации не будут изменены, многие выгодыполиморфизма окажутся потерянными. Нашим решением будет отказ от трактовкиконструкции let как сокращённой записи в пользу реализации её как примитиваязыка, после чего ко множеству правил типизации следует добавить новое правило:Γ ` s : σ Γ ` t[s/x] : τΓ ` let x = s in t : τЭто правило, которым вводится понятие let-полиморфизма, демонстрирует,что по крайней мере с точки зрения типизации, let-связанные переменныетрактуются как простые подстановки соответствующих выражений вместо ихимён. Дополнительная посылка Γ ` s : σ требуется исключительно для того,чтобы гарантировать существование корректного типа выражения s, причём точноезначение этого типа нас не интересует.
Цель данного ограничения в том, чтобыизбежать ошибочных выводов о существовании корректных типов для таких термов,какlet x = λf. f f in 0Теперь мы в состоянии вывести тип нашего проблемного выражения, пользуясьприведёнными выше правилами:{x : σ} ` x : σСм. выше` λx. x : σ → σ ` if (λx. x) true then (λx. x) 1 else 0 : int` let I = λx. x in if I true then I 1 else 0 : int4.2.2Наиболее общий типКак было сказано ранее, тип некоторых выражений, таких как λf. f fлибо λf. (f true, f 1), вывести невозможно. Типизируемые выражения обычноимеют множество типов, хотя некоторые из них, например, true — в точности один.Мы уже упоминали, что разновидность полиморфизма, доступная в языке ML,называется параметрической, т. е.
всевозможные типы выражения должны обладатьструктурным подобием. Более того, для каждого типизируемого выражениясуществует так называемый наиболее общий (главный) тип, причём все возможныетипы данного выражения представляют собой экземпляры наиболее общего типа.Прежде, чем изложить этот результат формально, введём некоторые термины.Начнём с расширения определения типа, дополнив его понятием переменнойтипа. Это значит, что типы могут быть построены путём применения конструкторовтипов как к типам-константам, так и к переменным.
Будем использовать греческиебуквы α и β для обозначения переменных типа, а σ и τ — произвольных типов.При помощи этой расширенной нотации мы в состоянии определить понятиеподстановки типа в другой тип вместо переменной типа. Такая подстановкасовершенно аналогична подстановке термов, так что мы даже будем использоватьте же самые обозначения (например, (σ → bool)[(σ → τ )/σ] = (σ → τ ) → bool).Однако, формальное определение подстановки типов проще, чем для термов, таккак не требует учёта связывания переменных. Для удобства дальнейшего изложения454.2. ПолиморфизмГлава 4. Типырасширим его на случай множественной параллельной подстановки:αi [τ1 /α1 , .
. . , τn /αk ] = τi if αi 6= β for 1 ≤ i ≤ kβ[τ1 /α1 , . . . , τn /αk ] = β if αi 6= β for 1 ≤ i ≤ k(σ1 , . . . , σn )con[θ] = (σ1 [θ], . . . , σn [θ])conЧтобы не загромождать определение, мы трактуем типы-константы какнуль-арные конструкторы типов, т. е.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
