Previous Up Next

Chapter 15  Подтипы

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

Подтипы, как правило, встречаются в объектно-ориентированных (object-oriented) языках, и часто рассматриваются как существенный элемент объектно-ориентированного стиля. Эта связь исследуется в главе 18; однако пока что мы описываем подтипы в ограниченном объеме, затрагивая только функции и записи. Уже тут возникает большинство интересных вопросов, связанных с наличием подтипов. В §15.5 описывается сочетание подтипов с некоторыми другими конструкциями, которые мы рассматривали в предыдущих главах. В последнем разделе главы (§15.6) мы детальнее исследуем семантику подтипов, в которой их использование соответствует добавлению в исполняемый код преобразований типа (coercions).1

15.1  Включение

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

  
Γ ⊢ t1 : T11 T12           Γ ⊢ t2 : T11
Γ ⊢ t1 t2 : T12

Вполне корректный терм

(λ r:{x:Nat}. r.x) {x=0,y=1}

не удовлетворяет этому правилу типизации, поскольку тип аргумента — {x:Nat,y:Nat}, тогда как функция принимает {x:Nat}. Ясно, однако, что для функции существенно только то, чтобы аргумент был записью с полем x; имеются ли другие поля и каковы они, ей безразлично. Более того, это требование можно распознать по типу функции — не нужно проверять ее тело и убеждаться в том, что поля кроме x не используются. Передача аргумента типа {x:Nat,y:Nat} в функцию, ожидающую тип {x:Nat}, всегда безопасна.

Цель введения подтипов в язык — уточнить правила типизации так, чтобы такие термы стали разрешенными. Мы добиваемся этого, формализуя интуитивное представление о том, что некоторые типы более <<информативны>>, чем другие: мы говорим, что S является подтипом T (subtype) (записывается как S <: T), имея в виду, что всякий терм типа S можно безопасно использовать в контексте, в котором ожидается тип T. Такую точку зрения на подтипы часто называют принципом безопасной подстановки (principle of safe substitution).

Более простое интуитивное объяснение таково: запись S <: T означает, что <<каждое значение, соответствующее типу S, соответствует также типу T>>, то есть, <<элементы S являются подмножеством элементов T>>. В §15.6 мы увидим, что иногда полезны другие, более тонкие, интерпретации подтипов, но такая семантика подмножеств (subset semantics) достаточна для большинства нужд.

Связь между отношением типизации и нашим новым отношением подтипирования обеспечивается новым правилом типизации — так называемым правилом включения (subsumption):

  
Γ ⊢ t : S           S <: T
Γ ⊢ t : T

Это правило говорит, что если S <: T, то всякий элемент S также является элементом T. Например, если мы определим отношение подтипирования так, чтобы {x:Nat,y:Nat} <: {x:Nat}, то при помощи правила T-Sub мы сможем вывести ⊢ {x=0,y=1} : {x:Nat}, и таким образом присвоить тип нашему исходному примеру.

15.2  Отношение подтипирования

Отношение подтипирования формально описывается через набор правил вывода, с помощью которых можно получить утверждения вида S <: T, что читается как <<S — подтип T>> (или <<T — надтип S>>). Мы рассмотрим по отдельности каждую разновидность типов (типы функций, типы записей и т. д.); для каждой из них мы формализуем правила, в соответствии с которыми можно разрешить использование элементов одного типа при том, что ожидается другой тип.

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

  S <: S

а во-вторых, оно должно быть транзитивным:

  
S <: U           U <: T
S <: T

Эти правила прямо следуют из нашего интуитивного представления о безопасности подстановки.

В случае типов записей, как мы уже видели, мы хотим считать тип S = { k1:S1 …km:Sm} подтипом T = { l1:T1 …ln:Tn}, если T содержит меньше полей, чем S. В частности, безопасно <<забывать>> последние поля в типах записей. Эта интуитивная идея отражена в так называемом правиле подтипирование в ширину (width subtyping):

  {li:Tii ∈ 1..n+k} <: {li:Tii ∈ 1..n}

Может показаться странным, что <<меньший>> тип — подтип — содержит больше полей. Это проще всего понять, приняв менее строгую точку зрения на типы записей, чем в §11.8, согласно которой тип {x:Nat} описывает <<множество записей, имеющих, по меньшей мере, поле x типа Nat>>. Элементами этого типа являются не только такие значения как {x=3} и {x=5}, но также и такие значения как {x=3,y=100} и {x=3,a=true,b=true}. Аналогично, тип {x:Nat,y:Nat} описывает записи, имеющие по крайней мере поля x и y, оба типа Nat. Значениями этого типа являются такие записи, как {x=3,y=100} и {x=3,y=100,z=true}, но не {x=3} и не {x=3,a=true,b=true}. Таким образом, множество значений, принадлежащих ко второму типу, является строгим подмножеством множества значений, принадлежащих к первому типу. Более длинный тип-запись соответствует более жесткой, т. е. более информативной, спецификации; таким образом, он описывает меньшее множество значений.

Правило подтипирования в ширину применимо только к типам записей, для которых типы общих полей совпадают. Можно также позволить различаться типам отдельных полей, если типы каждого соответствующего поля являются подтипами. Эта интуитивная концепция выражается правилом подтипирования в глубину (depth subtyping):

  
для каждого i,  Si<:Ti
{li:Sii ∈ 1..n} <: {li:Tii ∈ 1..n}

Следующее дерево вывода подтипирования использует правила S-RcdWidth и S-RcdDepth, демонстрируя, что тип вложенных записей {x:{a:Nat,b:Nat},y:{m:Nat}} является подтипом {x:{a:Nat},y:{}}:

 S-RcdWidth
{a:Nat,b:Nat} <: {a:Nat} 
         
 S-RcdWidth
{m:Nat} <: {} 
 S-RcdDepth
{x:{a:Nat,b:Nat},y:{m:Nat}} <: {x:{a:Nat},y:{}} 

Если мы хотим с помощью S-RcdDepth уточнить тип только одного поля записи (а не всех полей, как в предыдущем примере), то для остальных полей можно получить тривиальные отношения подтипирования с помощью правила S-Refl:

 S-RcdWidth
{a:Nat,b:Nat} <: {a:Nat} 
         
 S-Refl
{m:Nat} <: {m:Nat} 
 S-RcdDepth
{x:{a:Nat,b:Nat},y:{m:Nat}} <: {x:{a:Nat},y:{m:Nat}} 

С помощью правила транзитивности S-Trans можно сочетать подтипирование в ширину и в глубину. Например, можно получить надтип, расширив тип одного поля и отбросив другое:

 S-RcdWidth
{x:{a:Nat,b:Nat}, y:{m:Nat}}                   <: {x:{a:Nat,b:Nat}} 
         
 S-RcdWidth
{a:Nat,b:Nat}                    <: {a:Nat} 
 S-RcdDepth
{x:{a:Nat,b:Nat}}                    <: {x:{a:Nat}} 
 S-Trans
{x:{a:Nat,b:Nat},y:{m:Nat}} <: {x:{a:Nat}} 

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

  
{kj:Sjj ∈ 1..n} является перестановкой {li:Tii ∈ 1..n}
{kj:Sjj ∈ 1..n} <: {li:Tii ∈ 1..n}

Например, согласно правилу S-RcdPerm, тип {c:Top,b:Bool,a:Nat} является подтипом {a:Nat,b:Bool,c:Top}, и наоборот. (Отсюда следует, что отношение подтипирования не будет антисимметрично.)

Можно использовать S-RcdPerm совместно с S-RcdWidth и S-Trans, чтобы отбрасывать поля в любом месте записи, а не только в ее конце.

Упражнение 1   [★]: Нарисуйте дерево вывода, показывающее, что {x:Nat,y:Nat,z:Nat} является подтипом {y:Nat}.

Каждое из правил S-RcdWidth, S-RcdDepth и S-RcdPerm дает нам отдельную степень свободы при работе с записями. В целях обсуждения имеет смысл оставить их в виде трех отдельных правил. Например, существуют языки, в которых разрешена только часть этих правил. Например, большинство вариантов исчисления объектов (object calculus) Абади и Карделли (Abadi and Cardelli, 1996) не используют подтипирование в глубину. Однако при реализации языка полезно сочетать эти правила в одном макроправиле, которое обрабатывает все три вида подтипирования сразу. Это правило обсуждается в следующей главе (ср. с. ??).

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

  
T1 <: S1           S2 <: T2
S1 S2 <: T1 T2

Заметим, что отношение подтипирования <<срабатывает в обратную сторону>> (контравариантно, contravariant) для типов аргументов в левой предпосылке, но имеет одно и то же направление (ковариантно, covariant) для типов результатов и для самих функциональных типов. Интуитивное представление состоит в том, что, имея функцию f типа S1 S2, мы знаем, что f принимает аргументы типа S1; ясно, что f может также принять аргумент типа T1, где T1 — любой подтип S1. Тип f сообщает нам также, что эта функция возвращает элементы типа S2; мы имеем право считать, что они также принадлежат и к T2, где T2 — любой надтип S2. То есть, любая функция f типа S1 S2 может также рассматриваться как функция типа T1 T2.

Другая возможная точка зрения состоит в том, что безопасно разрешить использование функции типа S1 S2 в любом контексте, в котором ожидается тип T1 T2, если ни один аргумент, который может быть передан в функцию, не будет для нее неожиданным (T1 <: S1), и ни один ее результат не окажется неожиданным для контекста вызова (S2 <: T2).

Наконец, удобно иметь тип, являющийся надтипом всех остальных типов. Мы вводим новую типовую константу Top, а также правило, которое делает Top наибольшим элементом в отношении подтипирования:

  S <: Top

Тип Top подробнее обсуждается в §15.4.

С формальной точки зрения, отношение подтипирования есть наименьшее отношение, замкнутое относительно установленных нами правил. Для удобства ссылок, на рис. 15.1, 15.2 и 15.3 приведено полное определение простого типизированного лямбда-исчисления с записями и подтипами, причем синтаксические формы и правила, введенные нами в этой главе, выделены серым. Заметим, что присутствие правил рефлексивности и транзитивности означает, что отношение подтипирования является предпорядком (preorder). Однако, из-за правила перестановки полей в записи, частичным порядком оно не является: имеется много пар различных типов, где каждый элемент пары — подтип другого.


<: Top Основано на λ (9.1)



Синтаксис
t::= термы:
x переменная
λx:T.t абстракция
t t применение
 
v::= значения:
λx:T.t значение-абстракция
 
T::= типы:
Top максимальный тип
T T тип функций
 
Γ::= контексты:
пустой контекст
Γ,x:T связывание термовой переменной
 

Вычислениеtttt

        
t1 → t1
t1 t2 → t1 t2
          
t2 → t2
v1 t2 → v1 t2
          
(λx:T11.t12) v2 → [x ↦ v2]t12
ПодтипыS <: TS <: T
         S <: S  
        
S <: U           U <: T
S <: T
 
         S <: Top  
        
T1 <: S1           S2 <: T2
S1 S2 <: T1 T2
 

ТипизацияΓ ⊢ t : TΓ ⊢ t : T

         
x : T ∈ Γ
Γ ⊢ x : T
          
Γ, x:T1 ⊢ t2:T2
Γ ⊢ λx:T1.t2 : T1 T2
          
Γ ⊢ t1 : T11 T12           Γ ⊢ t2 : T11
Γ ⊢ t1 t2 : T12
        
Γ ⊢ t : S           S <: T
Γ ⊢ t : T
 



Figure 15.1: Простое типизированное лямбда-исчисление с подтипами (λ<:)



{} Расширяет λ (9.1)





Новые синтаксические формы
t::= …термы:
{li=tii ∈ 1..n} запись
t.l проекция
 
v::= …значения:
{li=vii ∈ 1..n} запись-значение
 
T::= …типы:
{li:Tii ∈ 1..n} тип записей
 

Новые правила вычисленияtttt

         {li=vii∈ 1..n}.ljvj  
        
t1 → t1
t1.l → t1.l
 
        
tj → tj
{li=vii∈ 1..j-1, lj=tj, lk=tkkj+1..n}                             → {li=vii∈ 1..j-1, lj=tj, lk=tkkj+1..n}
 

Новые правила типизацииΓ ⊢ t : TΓ ⊢ t : T

        
для каждого i,  Γ ⊢ ti : Ti
Γ ⊢ {li=tii∈ 1..n} : {li:Tii∈ 1..n}
 
        
Γ ⊢ t1 : {li:Tii∈ 1..n}
Γ ⊢ t1.lj : Tj
 



Figure 15.2: Записи (совпадает с рис. 11.7)



{} <: Расширяет λ<: (15.1) и правила для простых записей (15.2)



Новые правила подтипированияS <: TS <: T
         {li:Tii ∈ 1..n+k} <: {li:Tii ∈ 1..n}  
        
для каждого i,   Si <: Ti
{li:Sii ∈ 1..n} <: {li:Tii ∈ 1..n}
 
        
{kj:Sjj ∈ 1..n} является перестановкой {li:Tii ∈ 1..n}
{kj:Sjj ∈ 1..n} <: {li:Tii ∈ 1..n}
 



Figure 15.3: Записи и подтипы


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

f=defλr:{x:Nat}. r.x   Rx=def{x:Nat}
xy=def{x=0,y=1}   Rxy=def{x:Nat,y:Nat}

Предполагая обычные правила типизации для числовых констант, мы можем построить такое дерево вывода для утверждения типизации ⊢ f xy : Nat:

⊢ f : Rx Nat
         
⊢ 0 : Nat
         
⊢ 1 : Nat
 T-Rcd
⊢ xy : Rxy 
         
 S-RcdWidth
Rxy <: Rx 
 T-Sub
⊢ xy : Rx 
 T-App
⊢ f xy : Nat 
Упражнение 2   [★]: Является ли приведенное дерево вывода для f xy : Nat единственным?
Упражнение 3   [★]: (1) Сколько различных подтипов имеет {a:Top,b:Top}? (2) Можно ли найти бесконечную нисходящую цепочку в отношении подтипирования — то есть, бесконечную последовательность типов S0, S1, и т. д., такую, что каждый Si+1 является подтипом Si? (3) Можно ли найти бесконечную восходящую цепочку?
Упражнение 4   [★]: Существует ли тип, являющийся подтипом любого другого типа? Существует ли функциональный тип, являющийся надтипом любого другого функционального типа?
Упражнение 5   [★★]: Допустим, что мы расширили наше исчисление конструктором типов-произведений T1 × T2, как описано в §11.6. Естественно добавить правило подтипирования
    
S1 <: T1           S2 <: T2
S1 × S2 <: T1 × T2
соответствующее S-RcdDepth для записей. Правильно ли будет добавить также и такое правило:
    T1 × T2 <: T1

15.3  Свойства подтипов и типизации

Формально определив лямбда-исчисление с подтипами, мы должны теперь проверить, что это определение ничему не противоречит — в частности, что теоремы о сохранении и продвижении для простого типизированного лямбда-исчисления продолжают выполняться при наличии подтипов.

Упражнение 1   [Рекомендуется, ★★]: Прежде чем читать дальше, попробуйте предугадать, где в доказательствах могут возникнуть сложности. В частности, представим, что мы ошиблись при определении подтипирования и добавили к имеющимся у нас еще одно, неверное правило подтипирования. Какие свойства системы могут при этом потеряться? С другой стороны, предположим, что мы отбросили одно из правил подтипирования — могут ли при этом исчезнуть какие-либо свойства?

Вначале сформулируем одно ключевое свойство отношения подтипирования — аналог леммы об инверсии для отношения типизации в простом типизированном лямбда-исчислении (лемма 1). Если нам известно, что S является подтипом функционального типа, то лемма об инверсии с подтипами говорит, что и сам S должен быть функциональным типом; более того, она утверждает, что типы слева от стрелок должны быть связаны отношением подтипирования контравариантно, а типы справа от стрелок — ковариантно. Подобные соображения работают и в случае, когда известно, что S является подтипом типа записей: мы знаем, что S содержит больше полей (S-RcdWidth) в произвольном порядке (S-RcdPerm), и типы общих полей связаны отношением подтипирования (S-RcdDepth).

Лемма 2   [Инверсия отношения подтипирования]:
  1. Если S <: T1T2, то S имеет вид S1 S2, причем T1 <: S1 и S2 <: T2.
  2. Если S <: {li:Tii ∈ 1..n}, то S имеет вид {kj:Sjj ∈ 1..m}, причем содержит по крайней мере метки полей {lii ∈ 1..n} — т. е., {lii ∈ 1..n}{kjj ∈ 1..m} , и для каждой общей метки поля li = kj , Sj <: Ti.

Доказательство: Упражнение [Рекомендуется, ★★].

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

31ex

Лемма 3   
  1. Если Γ ⊢ λx:S1. s2 : T1 T2, то T1 <: S1, и Γ, x:S1s2 : T2.
  2. Если Γ ⊢ {ka=Saa ∈ 1..m} : {li:Tii ∈ 1..n}, то {lii ∈ 1..n}{kaa ∈ 1..m}, и Γ ⊢ sa : Ti для каждой общей метки поля ka = li.

Доказательство: Несложная индукция по деревьям вывода типов с использованием леммы 2 для правила T-Sub.

Затем нам потребуется лемма о подстановке для отношения типизации. Формулировка леммы остается той же, что и в случае простого типизированного лямбда-исчисления (лемма 8), и доказательство также практически совпадает.

Лемма 4   [Подстановка]: Если Γ, x:St : T и Γ ⊢ s : S, то Γ ⊢ [xs]t : T.

Доказательство: Индукция по деревьям вывода типов. Требуется рассмотреть новые варианты для правил T-Sub и для правил типизации записей T-Rcd и T-Proj, используя очевидным образом предположение индукции. В остальном доказательство такое же, как для 8.

Теорема о сохранении формулируется точно так же, как и раньше. Однако наличие подтипов усложняет ее доказательство в нескольких местах.

Теорема 5   [Сохранение]: Если Γ ⊢ t: T и tt, то Γ ⊢ t : T.

Доказательство: Прямолинейная индукция по деревьям вывода типов. Большинство случаев похожи на доказательство сохранения для простого типизированного лямбда-исчисления (9). Нужно лишь рассмотреть новые варианты для правил типизации записей и для включения.

Вариант T-Var: t = x
Не может возникнуть (не существует правил вычисления для переменных).

Вариант T-Abs: t = λx:T1.t2
Не может возникнуть (
t уже является значением).

Вариант T-App: t = t1 t2     Γ ⊢ t1 : T11 T12     Γ ⊢ t2 : T11     T = T12
Исходя из правил вычисления на рис. 
15.1 и 15.2, мы видим, что имеется три правила, позволяющих вывести tt: E-App1, E-App2 и E-AppAbs. Рассмотрим эти варианты.

Подвариант E-App1: t1t1     t′ = t1 t2
Нужный нам результат следует из предположения индукции и правила
T-App.

Подвариант E-App2: t1 = v1     t2t2     t′ = v1 t2
Аналогично.

Подвариант E-AppAbs: t1 = λx:S11.t12     t2 = v2     t′ = [xv2]t12
По лемме 
3(1), T11 <: S11 и Γ, x:S11t12 : T12. Согласно правилу T-Sub, Γ ⊢ t2 : S11. Отсюда, используя лемму о подстановке (4), получаем Γ ⊢ t : T12.

Вариант T-Rcd:

t = {li=tii ∈ 1..n}     Γ ⊢ ti : Ti для каждого i
T = {li:Tii ∈ 1..n}


Единственное правило вычисления, содержащее в левой части запись, — это
E-Rcd. Исходя из предпосылки этого правила, мы видим, что tjtj для некоторого поля tj. Требуемый результат следует из предположения индукции (примененного к соответствующей предпосылке Γ ⊢ tj : Tj) и правила T-Rcd.

Вариант T-Proj: t = t1.lj     Γ ⊢ t1 : {li : Tii ∈ 1..n}    T = Tj
Исходя из правил вычисления на рис. 
15.1 и 15.2, мы видим, что tt может быть выведено из двух правил: E-Proj и E-ProjRcd.

Подвариант E-Proj: t1t1     t′ = t1.lj
Результат следует из предположения индукции и правила
T-Proj.

Подвариант E-ProjRcd: t1 = {ka=vaa ∈ 1..m}    lj=kb    t′ = vb
По лемме 
3(2), имеем {lii ∈ 1..n}{kaa ∈ 1..m} и Γ ⊢ va : Ti для каждого ka = li. В частности, Γ ⊢ vb : Tj, как нам и требуется.

Вариант T-Sub: t : S    S <: T
Согласно предположению индукции,
Γ ⊢ t : S. По правилу T-Sub, Γ ⊢ t : T.

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

Лемма 6   [Канонические формы]:
  1. Если v — замкнутое значение типа T1 T2, то v имеет вид λx:S1.t2.
  2. Если v — замкнутое значение типа {li:Tii ∈ 1..n}, то v имеет вид {ka=vaa ∈ 1..m}, причем {lii ∈ 1..n}{kaa ∈ 1..m}.

Доказательство: Упражнение [Рекомендуется, ★★★].

Утверждение теоремы о продвижении и её доказательство достаточно близки к тому, что мы уже видели для простого типизированного лямбда-исчисления. Большинство трудностей, связанных с подтипами, выведено в лемму о канонических формах, и теперь требуется внести только несколько небольших изменений.

Теорема 7   [Продвижение]: Если t — замкнутый правильно типизированный терм, то либо t является значением, либо существует некоторый терм t такой, что tt.

Доказательство: Прямолинейная индукция по деревьям вывода типов. Вариант с переменной возникнуть не может (поскольку t замкнут). В варианте с лямбда-абстракцией искомый результат следует немедленно, так как абстракции являются значениями. Оставшиеся варианты более интересны.

Вариант T-App: t = t1 t2    t1 : T11 T12    t2 : T11    T = T12
Согласно предположению индукции, терм
t1 либо является значением, либо способен проделать шаг вычисления. То же самое верно и по отношению к t2. Если t1 способен проделать шаг, то применимо правило T-App1. Если t1 — значение, а t2 способен проделать шаг, то применимо правило T-App2. Наконец, если оба терма t1 и t2 являются значениями, то, согласно лемме о канонических формах (6), t1 имеет вид λx:S11.t12, так что к t применимо правило E-AppAbs.

Вариант T-Rcd:

t = {li=tii ∈ 1..n}    для каждого i ∈ 1..n, ti : Ti
T = {li : Tii ∈ 1..n}


Согласно предположению индукции, каждый из термов
ti либо является значением, либо способен проделать шаг вычисления. Если все эти термы — значения, то t сам является значением. Если же какой-либо из них способен проделать шаг, то к t применимо правило E-Rcd.

Вариант T-Proj: t = t1.lj    t1 : {li:Tii ∈ 1..n}    T = Tj
Согласно предположению индукции, терм
t1 либо является значением, либо способен проделать шаг вычисления. Если t1 может проделать шаг, то, по правилу E-Proj, может и t. Если же t1 — значение, то, согласно лемме о канонических формах (6), t1 имеет вид {ka=vaa ∈ 1..m}, причем {lii ∈ 1..n}{kaa ∈ 1..m} и для каждого li = kj имеем vj : Ti. В частности, lj входит в набор меток {kaa ∈ 1..m} терма t1, откуда, по правилу E-ProjRcd, мы видим, что и сам терм t способен проделать шаг вычисления.

Вариант T-Sub: Γ ⊢ t : S    S <: T
Результат прямо следует из предположения индукции.

15.4  Типы Top и Bottom

Наибольший тип Top не является необходимым элементом простого типизированного лямбда-исчисления с подтипами; его можно убрать, не нарушая базовых свойств системы. Однако большинство описаний включают этот тип, по нескольким причинам. Во-первых, он соответствует типу Object, имеющемуся в большинстве объектно-ориентированных языков программирования. Во-вторых, Top служит удобным техническим инструментом в более сложных системах, в которых подтипы сочетаются с полиморфизмом. Например, в Системе F<: (главы 26 и 28) наличие типа Top позволяет получить обыкновенную неограниченную квантификацию на основе ограниченной квантификации и, таким образом, упрощает всю систему. Более того, в F<: можно закодировать даже записи и, таким образом, еще больше упростить повествование (по крайней мере, с академической точки зрения); такое кодирование невозможно без Top. Наконец, поскольку поведение Top устроено несложно, а использование этого типа в примерах часто бывает полезно, нет особых причин от него отказываться.

Естественно спросить, можно ли также дополнить отношение подтипирования наименьшим элементом — типом Bot, который является подтипом всякого другого типа. Это возможно: такое расширение формально представлено на рис. 15.4


<: Bot Расширяет λ<: (15.1)



Новые синтаксические формы
T::= …типы:
Bot минимальный тип
Новые правила подтипированияS <: TS <: T
         Bot <: T



Figure 15.4: Наименьший тип


Прежде всего, следует заметить, что тип Bot пуст; замкнутых значений типа Bot не существует. Если бы такое значение, например, v, существовало, то правило включения вместе с правилом S-Bot позволили бы нам вывести ⊢ v : Top Top, откуда, по лемме о канонических формах (6, которая по-прежнему выполняется в нашем расширении), следовало бы, что терм v должен иметь вид λx:S1.t2 для некоторых S1 и t2. С другой стороны, по правилу включения, мы также имеем ⊢ v : {}, откуда по лемме о канонических формах следует, что терм v должен быть записью. Но из правил синтаксиса ясно, что v не может одновременно являться функцией и записью, так что предположение ⊢ v : Bot ведет к противоречию.

Пустота типа Bot не означает его бесполезности. Напротив: Bot дает программисту удобный способ выразить информацию о том, что некоторые операции (в частности, порождение исключения или вызов продолжения) не должны возвращать никакого значения. Если мы присвоим таким выражениям тип Bot, то получим нам два полезных результата: во-первых, это сообщает программисту, что никакого результата не ожидается (поскольку если бы выражение имело результат, это оказалось бы значение типа Bot); во-вторых, это дает знать программе проверки типов, что такое выражение можно безопасно использовать в контексте, ожидающем любой тип значения. Например, если терм error из главы 14, вызывающий исключение, получит тип Bot, то терм вроде

λ x:T. if <, x > then < > else error

будет правильно типизирован, поскольку, независимо от того, каков тип нормального результата, терм error может получить тот же самый тип через включение, так что две ветви условного выражения совместимы, как того требует правило T-If.1

К сожалению, наличие Bot существенно усложняет разработку программы проверки типов для нашей системы. Простой алгоритм проверки типов в языке с подтипами должен опираться на рассуждения вроде <<если терм-применение t1 t2 правильно типизирован, то t1 должен иметь функциональный тип>>. При наличии Bot приходится уточнить это утверждение до следующего вида: <<если t1 t2 правильно типизирован, то t1 должен иметь либо функциональный тип, либо Bot>>; этот вопрос подробнее обсуждается в §16.4. Сложности еще более возрастают в системах с ограниченной квантификацией; см. §28.8.

Эти сложности показывают, что добавление в систему Bot — более серьезный шаг, чем добавление Top. В системах, рассматриваемых в этой книге, мы его опускаем.

15.5  Подтипы и другие элементы языка

По мере того, как мы вводим подтипы в наше простое исчисление, продвигая его в направлении полноценных языков программирования, каждый новый элемент языка необходимо тщательно исследовать, чтобы выяснить, как он взаимодействует с подтипами. В этом разделе мы рассмотрим некоторые конструкции, введенные нами на этот момент.2 В последующих главах будет обсуждаться (значительно более сложное) взаимодействие подтипов с такими элементами языка, как параметрический полиморфизм (главы 26 и 28), рекурсивные типы (главы 20 и 21) и операторы типов (глава 31).

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

Оператор приписывания типа (ascription) t as T был введен в §11.4. Он позволяет программисту записать в тексте программы автоматически проверяемое утверждение о том, что некоторый подтерм составного выражения имеет определенный тип. Приписывание типов также используется в примерах в тексте этой книги для управления распечаткой типов — с его помощью программы проверки типов получают указания, что следует использовать более легкую для чтения сокращенную форму, а не тот тип, который был вычислен для терма во внутреннем представлении.

В языках с подтипами, таких, как Java или C++, приписывание типов оказывается намного более интересной операцией. В этих языках оно часто называется приведением типов (casting) и записывается в виде (T)t. Имеются две совершенно различные формы приведения типов — восходящее (up-casts) и нисходящее (down-casts). Первая разновидность не представляет сложностей; вторая, включающая динамическую проверку типов (dynamic type-testing), требует существенного расширения языка.

Восходящее приведение, в котором терму приписывается надтип (supertype) того типа, который был бы ему присвоен естественным образом, является частным случаем обыкновенного оператора приписывания типа. Мы сообщаем компилятору терм t и тип T, с точки зрения которого мы хотим <<рассматривать>> t. Программа проверки типов убеждается, что T — действительно один из типов терма t, пытаясь построить дерево вывода

Γ ⊢ t : S
         
S <: T
 T-Sub
Γ ⊢ t : T 
 T-Ascribe
Γ ⊢ t as T : T 

с использованием <<естественного>> типа T, правила включения T-Sub и правила приписывания типа из §11.4:

  
Γ ⊢ t1 : T
Γ ⊢ t1 as T : T

Восходящее приведение типов можно рассматривать как разновидность абстрагирования (abstraction) — т. е. как способ спрятать некоторые детали значения, чтобы их нельзя было использовать в некотором окружающем контексте. Например, если t является записью (или, в более общем случае, объектом), то при помощи восходящего приведения можно скрыть некоторые из ее полей (или методов).

С другой стороны, нисходящее приведение позволяет приписывать термам типы, которые программа проверки статически вывести не может. Чтобы разрешить нисходящее приведение, мы вносим несколько неожиданное изменение в правило типизации для as:

  
Γ ⊢ t1 : S
Γ ⊢ t1 as T : T

То есть, мы проверяем, что терм t1 правильно типизирован (т. е., имеет некоторый тип S), а затем присваиваем ему тип T, не выдвигая при этом никаких требований о взаимном отношении S и T. Например, с помощью нисходящего приведения мы можем написать функцию, принимающую какой угодно вообще аргумент, приводящую этот аргумент к типу записи, содержащей числовое поле, и возвращающую это поле

f = λ (x:Top) (x as {a:Nat}).a;

В сущности, программист говорит программе проверки типов: <<Я знаю (из соображений, слишком сложных, чтобы объяснить их в рамках правил типизации), что f всегда будет применяться к аргументам-записям, содержащим числовое поле a; я хочу, чтобы ты мне поверила>>.

Разумеется, слепая вера в такие утверждения имела бы ужасающие последствия для безопасности нашего языка: если программист почему-либо допустит ошибку и применит f к записи, не содержащей поля a, результат может (в зависимости от устройства компилятора) быть совершенно непредсказуемым. Вместо этого, мы должны руководствоваться принципом <<Доверяй, но проверяй>>. Во время компиляции программа проверки просто принимает тип, указанный в нисходящем приведении. Однако она вставляет в код проверку, которая во время выполнения должна убедиться, что представленное значение на самом деле имеет нужный тип. Другими словами, правило вычисления для выражений приписывания типа не должно просто отбрасывать аннотацию, как делало наше исходное правило:

  v1 as T → v1

а вместо этого должно сравнивать реально наблюдаемый (во время выполнения) тип значения с объявленным типом:

  
⊢ v1 : T
v1 as T → v1

Например, если мы применяем вышеуказанную функцию f к аргументу {a=5,b=true}, то наше правило (успешно) проверит, что ⊢ {a=5,b=true} : {a:Nat}. С другой стороны, если мы ее применим к {b=true}, то правило E-Downcast будет непригодно, и вычисление окажется в тупике. Такая проверка во время выполнения восстанавливает свойство сохранения типов.

Упражнение 1   [★★ ↛]: Докажите это.

Разумеется, при этом мы теряем свойство продвижения, поскольку правильно типизированная программа может оказаться в тупике при попытке выполнения неверного нисходящего приведения типа. Языки, содержащие нисходящее приведение, обычно решают это одним из двух способов: либо неудачное нисходящее приведение порождает динамическое исключение, которое программа может перехватить и обработать (см. главу 14), либо вместо операции нисходящего приведения используется динамическая проверка типа:

  
Γ ⊢ t1 : S           Γ, x:T ⊢ t2 : U           Γ ⊢ t3 : U
Γ ⊢ if t1 in T then xt2 else t3 : U
  
⊢ v1 : T
if v1 in T then xt2 else t3  → [x ↦ v1]t2
  
v1 : T
if v1 in T then xt2 else t3  → t3

В таких языках как Java нисходящие приведения типов встречаются довольно часто. Например, с их помощью организуется своего рода <<полиморфизм для бедных>>. Например, <<классы-контейнеры>>, такие как Set или List, в Java мономорфны: вместо того, чтобы иметь тип List T (список, содержащий элементы типа T) для каждого типа T, Java дает программисту только List — тип списков, чьи элементы принадлежат наибольшему типу Object. Поскольку в Java Object является надтипом любого типа объектов, это означает, что на самом деле списки могут содержать что угодно: когда нам требуется добавить какой-то элемент к списку, мы просто используем включение и повышаем тип этого элемента до Object. Однако когда мы извлекаем элемент из списка, процедура проверки типов знает только то, что он обладает типом Object. Этот тип не позволяет вызывать большинство методов объекта, поскольку описание Object упоминает только несколько самых общих методов, имеющихся у всех объектов Java. Чтобы сделать с элементом что-либо полезное, приходится приводить его вниз к некоторому ожидаемому типу T.

Многократно предлагалось — например, разработчиками языков Pizza (Odersky and Wadler, 1997), GJ (Bracha, Odersky, Stoutamire, and Wadler, 1998), PolyJ (Myers, Bank, and Liskov, 1997) и NextGen (Cartwright and Steele, 1998), — ввести в систему типов Java настоящий полиморфизм (ср. главу 23), поскольку он и безопасней, и эффективней приема с нисходящим приведением типов, а кроме того, не требует никаких проверок во время исполнения. С другой стороны, такие расширения увеличивают сложность языка, и без того достаточно громоздкого, и нетривиально взаимодействуют с другими элементами языка (см., например, работы Игараси, Пирса и Уодлера (Igarashi, Pierce, and Wadler, 1999, Igarashi, Pierce, and Wadler, 2001)); это усиливает позиции тех, кто считает нисходящие приведения разумным практическим компромиссом между безопасностью и сложностью.

Нисходящие приведения играют ключевую роль также и в поддержке рефлексии (reflection) в Java. Используя рефлексию, программист может потребовать от среды исполнения Java динамически загрузить файл с байт-кодом и сконструировать экземпляр содержащегося в этом файле класса. Ясно, что процедура проверки типов никак не может статически предсказать, какой класс будет загружены таким образом (к примеру, байт-код может быть получен откуда-нибудь из сети), так что она может только присвоить новым экземплярам наибольший тип Object. Опять же, чтобы осуществить какую-либо полезную работу, приходится приводить новый объект к некоторому ожидаемому типу T, обрабатывать исключения, которые могут возникнуть, если класс в байт-коде на самом деле не совместим с этим типом, и, наконец, использовать этот объект с типом T.

В заключение разговора про нисходящие приведения нужно сделать замечание о реализации. Исходя из данных нами правил, кажется, что их введение в язык требует добавления всех механизмов проверки типов в среду времени выполнения. Хуже того: поскольку, как правило, во время выполнения значения представляются иначе, чем во время компиляции (в частности, функции компилируются в байт-код или в команды машинного языка), нам, видимо, придется написать отдельную процедуру для вычисления типов, производимого при проверке во время выполнения. Чтобы избежать этого, в реальных языках нисходящие приведения сочетаются с тегами типов (type tags) — тегами размером в одно слово (довольно похожими на конструкторы типов данных в ML и на теги вариантов в §11.10), которые предоставляют <<метку>> информации о типах, используемых при компиляции, и служат для динамической проверки подтиирования. В главе 19 подробно рассматривается пример такого механизма.

Варианты

Правила подтипирования для вариантов (см. §11.10) почти совпадают с правилами для записей; единственное различие состоит в том, что правило подтипирования в ширину, S-VariantWidth, позволяет добавлять, а не отбрасывать, новые варианты при переходе от подтипа к надтипу. По интуитивному представлению, выражение с тегом <l=t> принадлежит к типу вариантов <li:Tii ∈ 1..n>, если его метка l — одна из возможных меток {li}, перечисленных в определении типа; добавление новых меток к этому множеству уменьшает информацию, которой мы располагаем об элементах типа. Одновариантный тип <l1:T1> точно указывает, какой меткой обозначаются его элементы; двухвариантный тип <l1:T1,l2:T2> говорит, что его элементы отмечены либо меткой l1, либо меткой l2, и т. д. С другой стороны, когда мы используем вариантные значения, это всегда происходит с помощью выражения case, в котором на каждый вариант, указанный для типа, имеется одна ветвь. Если вариантов будет больше, это приведет только к тому, что предложения case будут включать ненужные дополнительные ветви.


<> <: Расширяет λ<: (15.1) и простые правила для вариантов (11.11)



Новые синтаксические формы
t::= …термы:
<l=t> (без as) постановка тега
 

Новые правила типизацииΓ ⊢ t : TΓ ⊢ t : T

          
Γ ⊢ t1 : T1
Γ ⊢ <l1=t1> : <l1:T1>
Новые правила подтипированияS <: TS <: T
         <li:Tii ∈ 1..n> <: <li:Tii ∈ 1..n+k>  
        
для каждого i,    Si <: Ti
<li:Sii ∈ 1..n> <: <li:Tii ∈ 1..n>
 
        
<kj:Sjj ∈ 1..n> явл. перестановкой <li:Tii ∈ 1..n>
<kj:Sjj ∈ 1..n> <: <li:Tii ∈ 1..n>
 



Figure 15.5: Варианты и подтипы


Еще одно следствие сочетания подтипов и вариантов — то, что мы теперь можем отказаться от аннотаций в конструкции навешивания тега, и писать просто <l=t> вместо <l=t> as <li:Tii ∈ 1..n>, как нам приходилось делать в §11.10. Теперь мы можем упростить правило типизации для этой конструкции и сказать, что <l1=t1> имеет точный тип <l1=T1>. Любой более крупный вариантный тип получается через включение и правило S-VariantWidth.

Списки

Мы уже видели несколько примеров ковариантных конструкторов типов (записи и варианты, а также функциональные типы по правой части типа) и один контравариантный конструктор (стрелка, по левой части типа). Конструктор List также ковариантен: если у нас есть список, элементы которого имеют тип S1, и при этом S1 <: T1, то мы можем без опаски считать, что список имеет элементы типа T1.

  
S1 <: T1
List S1 <: List T1

Ссылки

Не все конструкторы типов являются либо ковариантными, либо контравариантными. К примеру, конструктор Ref должен быть инвариантным, чтобы сохранить типовую безопасность.

  
S1 <: T1           T1 <: S1
Ref S1 <: Ref T1

Чтобы Ref S1 считался подтипом Ref T1, мы требуем, чтобы S1 и T1 были эквивалентны (equivalent) с точки зрения отношения подтипирования — каждый из них должен быть подтипом другого. Это позволяет нам переупорядочивать поля записей внутри конструктора Ref — скажем, Ref {a:Bool,b:Nat} <: Ref {b:Nat,a:Bool}, — но ничего больше.

Правило подтипирования так сильно ограничено потому, что в любом данном контексте значение типа Ref T1 может использоваться двумя способами: для чтения (оператор !) и записи (:=). Когда значение используется для чтения, контекст ожидает получить значение типа T1. Поэтому, если на самом деле ссылка вернет значение типа S1, нужно, чтобы было S1 <: T1, а иначе ожидания контекста будут нарушены. С другой стороны, если та же самая ссылочная ячейка используется для записи, то новое значение, предоставляемое контекстом, будет иметь тип T1. Если тип ссылки на самом деле Ref S1, то кто-нибудь потом может прочитать значение по ссылке и использовать его как S1; это будет безопасно только в том случае, если T1 <: S1.

Упражнение 2   [★ ↛] (1) Напишите короткую программу, которая приведет к ошибке времени выполнения (т. е., вычисление зайдет в тупик), если мы откажемся от первой предпосылки S-Ref. (2) Напишите другую программу, которая приведет к ошибке, если будет отброшена вторая предпосылка.

Массивы

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

  
S1 <: T1           T1 <: S1
Array S1 <: Array T1

Интересно, что Java разрешает ковариантное подтипирование для массивов:

  
S1 <: T1
Array S1 <: Array T1

(в синтаксисе Java, S1[] <: T1[]). Такая конструкция исходно была введена, чтобы возместить отсутствие параметрического полиморфизма при типизации некоторых базовых операций, вроде копирования массивов. Сейчас большинство специалистов считают ее ошибкой в проектировании языка, поскольку она серьезно снижает производительность программ, использующих массивы. Это происходит потому, что небезопасное правило подтипирования приходится компенсировать проверкой во время выполнения, при каждом присваивании каждому массиву, чтобы убедиться в том, что записываемое значение принадлежит подтипу действительного типа элементов массива.

Упражнение 3   [★★★ ↛]: Напишите короткую программу на Java с использованием массивов, так, чтобы она проходила проверку типов, но ломалась (порождая ArrayStoreException) во время выполнения.

Снова ссылки

Путем введения двух независимых конструкторов типов, Source (<<кран>>3) и Sink (<<слив>>), можно получить более тонкую реализацию ссылок, впервые исследованную Рейнольдсом (Reynolds, 1988) в языке Forsythe. С интуитивной точки зрения, Source T предоставляет возможность считывать значения типа T из ячейки (но не присваивать значение), а Sink T предоставляет возможность записывать значение в ячейку. Ref T сочетает обе эти возможности и дает разрешение как на чтение, так и на запись.

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

  
Γ ∣ Σ ⊢ t1 : Source T11
Γ ∣ Σ ⊢ !t1 : T11
  
Γ ∣ Σ ⊢ t1 : Sink T11           Γ ∣ Σ ⊢ t2 : T11
Γ ∣ Σ ⊢ t1 := t2 : Unit

Теперь, если у нас есть только возможность считывать значение ячейки, и гарантируется, что эти значения будут иметь тип S1, то мы можем без опаски <<сузить>> эту возможность до возможности читать значения типа T1, если S1 является подтипом T1. Таким образом, конструктор Source ковариантен.

  
S1 <: T1
Source S1 <: Source T1

С другой стороны, возможность записывать значения типа S1 в данную ячейку может быть понижена до возможности записывать значения некоторого меньшего типа T1: конструктор Sink контравариантен.

  
T1 <: S1
Sink S1 <: Sink T1

Наконец, выразим интуитивное представление о том, что тип Ref T1 представляет комбинацию возможностей к чтению и к записи, при помощи двух правил подтипирования, которые позволяют сузить ссылку Ref до <<крана>> Source или до <<слива>> Sink.

  Ref T1 <: Source T1
  Ref T1 <: Sink T1

Каналы

На таком же интуитивном представлении (и на тех же самых правилах подтипирования) основан подход к типам каналов (channel types) в современных языках для параллельного программирования, таких как Pict (Pierce and Turner, 2000, Pierce and Sangiorgi, 1993). Главный тезис здесь состоит в том, что с точки зрения типизации канал межпроцессного взаимодействия ведет себя точно так же, как ссылочная ячейка: его можно использовать для чтения и для записи, и поскольку трудно статически определить, какие операции чтения соответствуют каким операциям записи, единственный простой способ обеспечить типовую безопасность — требовать, чтобы все значения, передаваемые по каналу, принадлежали к одному типу. Теперь при передаче какому-либо процессу только возможности записи в определенный канал, такой процесс может безопасно передавать эту возможность другому процессу, который обещает записывать в канал значения меньшего типа — конструктор <<канал для записи>> контравариантен. Аналогично, при передаче только возможности чтения из канала её можно безопасно сузить до возможности чтения значений любого большего типа — конструктор <<канал для чтения>> является ковариантным.

Базовые типы

В полноценном языке с богатым набором базовых типов часто бывает полезно ввести отношение подтипирования между этими базовыми типами. Например, во многих языках булевские значения true и false на самом деле представляются в виде чисел 1 и 0. Мы можем, если пожелаем, сообщить об этом программисту, введя аксиому подтипирования Bool <: Nat. Тогда можно писать компактные выражения вроде 5 * b вместо if b then 5 else 0.

15.6  Семантика подтипов, основанная на преобразованиях типов

На протяжении этой главы мы следовали интуитивному представлению о том, что подтипы <<не влияют на семантику>>. Наличие подтипов никак не влияет на процесс исполнения программ; оно лишь позволяет добавить некоторую гибкость в правила типизации. Такая интерпретация проста и естественна, но ведет к некоторому снижению эффективности, особенно при численных расчетах и при доступе к полям записей. Такие потери могут оказаться неприемлемыми для высокопроизводительных реализаций. В этом разделе мы сделаем набросок альтернативной семантики на основе преобразования типов (coercion semantics) и обсудим некоторые вопросы, возникающие в связи с этим новым подходом. При желании этот раздел можно пропустить.

Проблемы семантики, основанной на подмножествах

Как мы видели в §15.5, часто бывает удобно разрешить подтипирование между различными базовыми типами. Однако некоторые <<интуитивно понятные>> связи между базовыми типами могут отрицательно повлиять на производительность. Допустим, например, что мы введем аксиому Int <: Float, чтобы можно было использовать целые числа в вычислениях с плавающей точкой без явных преобразований — например, писать 4.5 + 6 вместо 4.5 + intToFloat(6). При семантике, основанной на подмножествах, это означает, что множество целых числовых значений должно буквально являться подмножеством значений с плавающей точкой. Однако в большинстве реальных машин конкретные представления целых чисел и чисел с плавающей точкой совершенно различны: целые обычно представлены в формате с дополнением до двух, а числа с плавающей точкой состоят из мантиссы, показателя степени и знака, плюс некоторые особые случаи вроде NaN (не-число).

Чтобы согласовать такое расхождение в представлениях и семантику на основе подмножеств, мы можем принять общее теговое (tagged) (или упакованное, boxed) представление для чисел: целое число представляется как машинное целое, снабженное тегом (располагающимся либо в отдельном слове-заголовке, либо в старших разрядах слова, содержащего само целое число), а число с плавающей точкой представляется как машинное число с плавающей точкой, снабженное другим тегом. В таком случае тип Float относится ко всему множеству помеченных тегами чисел, а тип Int относится только к помеченным целым.

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

Другая проблема с производительностью возникает, когда подтипы сочетаются с записями, в частности, при применении правила перестановки полей. Наше простое правило вычисления для проекции поля

  {li=vii ∈ 1..n}.lj → vj

можно читать так: <<найти среди меток полей записи lj и вернуть соответствующее значение vj>>. Однако в настоящей реализации мы, безусловно, не хотим проводить линейный просмотр полей записи в поисках нужной метки. В языке без подтипов (или с подтипами, но без правила перестановки) можно получить значение намного быстрее: если метка lj идет третьей в типе записи, то мы уже во время компиляции знаем, что все значения данного типа будут содержать в третьем поле lj, так что во время выполнения нам вовсе не нужно смотреть на метки (мы вообще можем исключить их из представления записей во время выполнения, в сущности, превращая записи в кортежи). Чтобы получить значение поля lj, мы генерируем команду косвенной загрузки через регистр, указывающий на начало записи, со смещением в 3 слова. Наличие правила перестановки делает этот метод невозможным, поскольку информация о том, что некоторое значение записи принадлежит типу, в котором lj является третьим полем, ничего не говорит нам о том, где на самом деле внутри записи хранится поле lj. Опять же, сложные приемы оптимизации и кодирования могут уменьшить потери, но в общем случае проекция поля может так или иначе потребовать поиска во время выполнения.3

Семантика, основанная на преобразовании типов

Обе эти проблемы можно решить, если принять другую семантику, в которой подтипирование <<исчезает при компиляции>> и заменяется преобразованиями типа во время выполнения. Если, скажем, во время проверки типов Int повышается до Float, то во время выполнения мы физически изменяем представление числа с машинного целого на машинное число с плавающей точкой. Аналогично, использование правила перестановки при подтипировании компилируется в фрагмент кода, который физически изменяет порядок полей записи. После этого элементарные численные операции и доступ к полям могут выполняться без дополнительных расходов на снятие тегов или поиск.

С интуитивной точки зрения, семантика, основанная на преобразованиях типа, для языка с подтипами выражается в виде функции, которая переводит термы этого языка в язык нижнего уровня, в котором подтипы отсутствуют. В конечном счете, этот низкоуровневый язык может быть машинным кодом некоторого конкретного процессора. Однако в целях изложения мы продолжим обсуждение на более абстрактном уровне. В качестве исходного языка мы возьмём язык, используемый нами в большей части этой главы, — простое типизированное лямбда-исчисление с подтипами и записями. В качестве низкоуровневого целевого языка мы выбираем язык чистого простого типизированного лямбда-исчисления с записями и типом Unit (который используется для моделирования Top).

Формально компиляция представляется тремя функциями перевода — для типов, для подтипирования и для типизации. В случае типов функция перевода просто заменяет Top типом Unit. Мы записываем эту функцию в виде − .

   Top =Unit
   T1 T2 =     T1  →  T2  
   {li:Tii ∈ 1..n} =    {li: Ti i ∈ 1..n} 

Например, Top{a:Top,b:Top} = Unit{a:Unit,b:Unit}. (Остальные функции перевода также будут обозначаться символами − ; из контекста всегда будет ясно, какая именно функция имеется в виду.)

Чтобы перевести терм, мы должны знать, где при выводе его типа используется правило включения, поскольку именно в этих местах будет добавлено преобразование типа во время выполнения. Один из удобных способов формализации этого наблюдения состоит в определении перевода как функции на деревьях вывода утверждений о типизации. Аналогично, чтобы породить функцию преобразования, переводящую значения типа S в тип T, мы должны знать не только сам факт того, что S является подтипом T, но и почему это так. Мы добиваемся этого, порождая преобразования из деревьев вывода подтипирования.

Для формализации перевода требуется дополнительное соглашение по именованию деревьев вывода. Запись C :: S <: T будет означать: <<C — дерево вывода подтипирования с заключением S <: T>>. Аналогично, D :: Γ ⊢ t : T будет значить: <<D — дерево вывода типов с заключением Γ ⊢ t : T>>.

Рассмотрим сначала функцию, которая на основе дерева вывода C для утверждения о подтипировании S <: T порождает преобразование C . Это преобразование — не что иное как функция (в целевом языке перевода λ) из типа S в тип T . Определим его, рассматривая по отдельности каждый случай финального правила, используемого в C.


/T <: T  (S-Refl) = λx: T . x
   
/S <: Top  (S-Top) = λx: S. unit
   
C1 :: S <: U      C2 :: U <: T /S <: T  (S-Trans) = λx: S . C2 ( C1 x)
   
C1 :: T1 <: S1      C2 :: S2 <: T2 /S1S2 <: T1T2  (S-Arrow) = λf: S1S2 . λx: T1 . C2(f( C1 x))
   
/{li:Tii ∈ 1..n+k} <: {li:Tii ∈ 1..n}  (S-RcdWidth) = λr:{li: Ti i ∈ 1..n+k}. {li=r.lii ∈ 1..n}
   
для каждого i    Ci :: S1 <: Ti/{li:Sii ∈ 1..n} <: {li:Tii ∈ 1..n}  (S-RcdDepth) = λr:{li: Si i ∈ 1..n}. {li= Ci (r.li)i ∈ 1..n}
   
{kj:Sjj ∈ 1..n} перестановка {li:Tii ∈ 1..n}/{kj:Sjj ∈ 1..n} <: {li:Tii ∈ 1..n}  (S-RcdPerm) = λr:{kj: Sj j ∈ 1..n}. {li=r.lii ∈ 1..n}
 

Лемма 1   Если C :: S <: T, то C : ST.

Доказательство: Прямолинейная индукция по C.

71ex Деревья вывода типизации переводятся аналогично. Если D — дерево вывода для утверждения Γ ⊢ t : T, то его перевод D  — терм целевого языка типа T . Такая функция перевода часто называется Пенсильванской трансляцией (Penn translation), в честь исследовательской группы Пенсильванского университета, которая впервые ее исследовала (Breazu-Tannen, Coquand, Gunter, and Scedrov, 1991).


x:T ∈ Γ/Γ ⊢ x : T  (T-Var) =x
   
D2 :: Γ, x:T1t2 : T2/Γ ⊢ λx:T1.t2 : T1 T2  (T-Abs) =λx: T1 . D2
   
D1 :: Γ ⊢ t1 : T11 T12      D2 :: Γ ⊢ t2 : T11 /Γ ⊢ t1 t2 : T12  (T-App) = D1 D2
   
для каждого i, Di :: Γ ⊢ ti : Ti/Γ ⊢ {li=tii ∈ 1..n} : {li:Tii ∈ 1..n}  (T-Rcd) ={li= Di i ∈ 1..n}
   
D1 :: Γ ⊢ t1 : {li:Tii ∈ 1..n}/Γ ⊢ t1.lj : Tj  (T-Proj) = D1 .lj
   
D :: Γ ⊢ t : S      C :: S <: T /Γ ⊢ t : T  (T-Sub) = C D
 

Теорема 2   Если D :: Γ ⊢ t : T, то Γ ⊢ D : T , где Γ  — поточечное расширение функции перевода типов на контексты типизации: ∅ = ∅ и Γ, x:T = Γ , x: T .

Доказательство: Прямолинейная индукция по D, с использованием леммы 1 для варианта T-Sub.

Определив эти функции перевода, можно отказаться от правил вычисления для высокоуровневого языка с подтипами и вместо этого вычислять термы, подвергая их сначала проверке типов (через правила типизации и подтипирования для высокоуровневого языка), переводя деревья проверки типов в низкоуровневый целевой язык, и, наконец, определяя их операционное поведение через отношение вычисления для этого низкоуровневого языка. Такая стратегия действительно используется в некоторых высокопроизводительных реализациях языков с подтипами: например, в экспериментальном компиляторе языка Java, разработанном Йельской группой (League, Shao, and Trifonov, 1999, League, Trifonov, and Shao, 2001).

Упражнение 3   [★★★, ↛]: Модифицируйте приведенную нами функцию перевода так, чтобы целевым языком служило простое типизированное лямбда-исчисление с кортежами (а не с записями). Убедитесь, что теорема 2 по-прежнему выполняется.

Когерентность

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

   Bool <: Int     =λb:Bool. if b then 1 else 0
   Int <: String     =intToString
   Bool <: Float     =λb:Bool. if b then 1.0 else 0.0
   Float <: String     =floatToString

Здесь intToString и floatToString — примитивы, генерирующие строковое представление чисел. Для примера предположим, что intToString(1) = "1", а floatToString(1.0) = "1.000".

Предположим теперь, что мы пытаемся вычислить терм

(λ x:String.x) true

с помощью семантики преобразования типов. Этот терм типизируем, если принять во внимание вышеперечисленные аксиомы. Однако, его можно типизировать двумя разными способами: либо мы переводим Bool в Int, и затем в String через включение, показывая, что true — подходящий аргумент для функции типа String String, либо сначала мы переводим Bool во Float, и оттуда в String. Однако при переводе этих преобразований в λ получается различное поведение. Если мы переводим true в Int, получается 1, откуда через intToString выходит строка "1". Однако если мы сначала проведем преобразование во Float, а затем, через floatToString, в String (следуя структуре дерева вывода типа, где true : String доказывается через Float), мы получим "1.000". Но "1" и "1.000" — совершенно различные строки; даже длина у них разная. Другими словами, выбор способа доказательства для ⊢ (λx:String.x) true : String влияет на то, как ведет себя оттранслированная программа! Однако этот выбор целиком содержится внутри компилятора — программист работает только с термами, а не с деревьями вывода, — что означает, что мы спроектировали язык, который не позволяет программисту не только управлять поведением написанных им программ, но даже и предсказывать его.

Правильное решение проблем такого рода заключается во введении когерентности (coherence) — дополнительного требования, которое налагается на определения функций перевода.

Определение 4   Функция перевода из деревьев вывода типов одного языка в термы другого когерентна, если для всякой пары деревьев вывода D1 и D2 с одним и тем же заключением Γ ⊢ t : T переводы D1 и D2 являются поведенчески эквивалентными термами целевого языка.

В частности, вышеприведенные функции перевода (без базовых типов) когерентны. Чтобы восстановить когерентность после добавления базовых типов (с вышеуказанными аксиомами), достаточно изменить определение элементарной функции floatToString так, чтобы выполнялось floatToString(0.0) = "0" и floatToString(1.0) = "1".

Доказательство когерентности, особенно для более сложных языков, может быть нелегкой задачей. См. работы Рейнольдса (Reynolds, 1980), Бреазу-Таннена и др. (Breazu-Tannen, Coquand, Gunter, and Scedrov, 1991), Куриена и Гелли (Curien and Ghelli, 1992) и Рейнольдса (Reynolds, 1991).

15.7  Типы-пересечения и типы-объединения

Можно существенно уточнить отношение подтипирования, если добавить в язык типов операцию пересечения (intersection). Типы-пересечения изобретены Коппо, Дезани, Салле и Поттингером (Coppo and Dezani-Ciancaglini, 1978, Coppo, Dezani-Ciancaglini, and Sallé, 1979, Pottinger, 1980). Доступное введение в эту тему можно найти у Рейнольдса (Reynolds, 1988, Reynolds, 1998b), Хиндли (Hindley, 1992) и Пирса (Pierce, 1991b).

Тип-пересечение T1T2 содержит термы, принадлежащие к обоим типам T1 и T2 — то есть, T1T2 является, в смысле теории порядков, пересечением (точной нижней гранью) T1 и T2. Такая интуиция отражается в трех новых правилах подтипирования:

  T1T2 <: T1
  T1T2 <: T2
  
S <: T1           S <: T2
S <: T1T2

Одно дополнительное правило отражает естественную взаимосвязь между типами-пересечениями и функциональными типами.

  S T1 S T2 <: S (T1 T2)

Интуитивная идея, лежащая в основе этого правила, такова: если мы знаем, что терм имеет функциональные типы S T1 и S T2, то мы, безусловно, можем передать в эту функцию терм типа S и ожидать в качестве результата как T1, так и T2.

Мощность понятия типов-пересечений можно продемонстрировать утверждением, что в варианте простого типизированного лямбда-исчисления с подтипами, типами-пересечениями и вызовом по имени, множество нетипизированных лямбда-термов, которым можно присвоить типы, в точности совпадает с множеством нормализуемых (normalizing) термов. Т. е., терм типизируем тогда и только тогда, когда его вычисление завершается! Отсюда немедленно следует, что проблема реконструкции типов (см. главу 22) для исчисления с типами-перечислениями неразрешима.

С прагматической точки зрения ценность типов-пересечений состоит в том, что они поддерживают некоторую форму конечной перегрузки операторов (finitary overloading). Например, мы можем присвоить тип (Nat Nat Nat) (Float Float Float) такой операции сложения, которую можно применить как к натуральным числам, так и к числам с плавающей точкой (например, используя теговые биты в представлении аргументов для выбора правильной машинной команды во время выполнения).

К сожалению, мощность типов-пересечений ведет к некоторым практическим трудностям для разработчиков языков. Пока что лишь один полноценный язык, Forsythe (Reynolds, 1988), содержит типы-пересечения в их наиболее общем виде. Ограниченная форма, называемая типы-уточнения (refinement types), может оказаться более разумной (Freeman and Pfenning, 1991, Pfenning, 1993b, Davies, 1997).

Двойственное понятие типов-объединений (union types) T1T2 также оказывается весьма полезным. В отличие от типов-сумм и вариантов (которые также иногда называют <<объединениями>>, что приводит к путанице), T1T2 обозначает обыкновенное объединение множества значений, принадлежащих к типу T1, и множества значений, принадлежащих к типу T2, безо всякого тега, указывающего на источник данного элемента. Таким образом, Nat Nat — всего лишь псевдоним для Nat. Пересекающиеся типы-объединения уже давно играют важную роль при анализе программ (Palsberg and Pavlopoulou, 1998), но до сих пор редко встречались в языках программирования (важное исключение — Algol 68, ср. van Wijngaarden, Mailloux, Peck, Koster, Sintzoff, Lindsey, Meertens, and Fisker, 1975). Впрочем, в последнее время их все чаще применяют в контексте систем типов для обработки <<полуструктурированных>> форматов баз данных, таких как XML (Buneman and Pierce, 1998, Hosoya, Vouillon, and Pierce, 2001).

Основное формальное различие между непересекающимися и пересекающимися типами-объединениями состоит в том, что для последних отсутствует какой-либо аналог конструкции case: если известно, что значение v имеет тип T1T2, то мы можем безопасно применять к нему только те операции, которые имеют смысл как для T1, так и для T2. (Например, если T1 и T2 — записи, то можно обращаться к их общим полям.) Бестеговый тип union в языке C приводит к нарушению типовой безопасности именно потому, что в языке игнорируется это ограничение, и над элементом типа T1T2 разрешена любая операция, имеющая смысл либо для T1, либо для T2.

15.8  Дополнительные замечания

Идея подтипов в языках программирования восходит к 1960-м годам, к языку Simula (Birtwistle, Dahl, Myhrhaug, and Nygaard, 1979) и его родственникам. Первые попытки формального анализа принадлежат Рейнольдсу (Reynolds, 1980) и Карделли (Cardelli, 1984).

Правила типизации и, особенно, подтипирования, работающие с записями, несколько сложнее, чем те, что мы видели до сих пор, поскольку в них либо имеется переменное число предпосылок (по одной на поле), либо используются дополнительные механизмы вроде перестановок индексов полей. Существует множество других способов записи этих правил, однако все они либо столь же сложны, либо избегают сложности, полагаясь на неформальные соглашения (например, многоточие: <<l1:T1 … ln:Tn>>). Недовольство таким положением дел привело Карделли и Митчелла к разработке исчисления операций над записями (<<Operations on Records>>, Cardelli and Mitchell, 1991), в котором макрооперация создания записи с многими полями выражается через базовое значение — пустую запись, а также операцию добавления одного поля за раз. C этой точки зрения можно также рассмотреть дополнительные операции, вроде изменения значения поля или конкатенации записей (Harper and Pierce, 1991). Правила типизации для этих операций оказываются достаточно тонкими, особенно при наличии параметрического полиморфизма, так что разработчики языков предпочитают работать с обыкновенными записями. Тем не менее, система Карделли и Митчелла остается важным концептуальным достижением. Альтернативный анализ записей, основанный на полиморфизме строчных переменных (row-variable ploymorphism), разработан Вандом (Wand, 1987, Wand, 1988, Wand, 1989b), Реми (Rémy, 1990, Rémy, 1989, Rémy, 1992) и другими, и служит основой для объектно-ориентированных конструкций языка OCaml (Rémy and Vouillon, 1998, Vouillon, 2000).

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


1
В этой главе изучается λ<:, простое типизированное лямбда-исчисление с подтипами (рис. 15.1) и записями (рис. 15.3); соответствующая реализация на OCaml называется rcdsub. (В некоторых примерах также используются числа; для их проверки требуется fullsub.)
1
В языках с полиморфизмом, например, в ML, в качестве типа результата для error и других подобных конструкций также можно использовать тип X.X. При этом тот же самый результат достигается другими средствами: вместо того, чтобы присваивать error тип, который может быть повышен до любого другого, ему присваивают схему типа, которая может быть конкретизирована до любого типа. Хотя эти два решения основаны на различных механизмах, они в то же время весьма похожи: в частности, тип X.X также пуст.
2
Большинство расширений, обсуждаемых в этом разделе, не реализованы в программе проверки типов fullsub.
3
Буквально <<источник>>. Здесь используется метафора входящей и выходящей труб в бассейне. — прим. перев.
3
Аналогичные наблюдения применимы и к поиску полей и методов объектов в языках, в которых подтипирование объектов допускает перестановку полей. Именно поэтому, например, Java ограничивает подтипирование между классами так, что новые поля могут добавляться только в конце. Подтипирование между интерфейсами (а также между классом и интерфейсом) разрешает перестановку — иначе интерфейсы оказались бы практически бесполезны. При этом руководство по языку явно предупреждает, что поиск метода в интерфейсе в общем случае происходит медленнее, чем в классе.

Previous Up Next