Пирс Б. Типы в языках программирования

Подождите немного. Документ загружается.

24.2. Абстракция данных при помощи экзистенциальных типов 291

Упражнение 24.2.3 Рекомендуется, : Реализуйте переключатели FlipFlop как объекты, ис-

пользуя в качестве типа внутреннего представления Counter. В качестве образца можно взять АТД

FlipFlop из предыдущего подраздела.

Упражнение 24.2.4 Рекомендуется, : При помощи интерпретатора fullomega реализуйте им-

перативный вариант объектов Counter по образцу Упражнения 24.2.2.

24.2.3. Сравнение объектов и АТД

Примеры из предыдущего раздела не составляют полноценную модель объектно-ориентированного

программирования. Многие характеристики объектной ориентированности, рассмотренные нами в Гла-

вах 18 и 19, в том числе наследование типов и реализаций, классы, рекурсия через self и super, здесь

отсутствуют. Мы вернемся к моделированию этих характеристик в Главе 32, когда наша система ти-

пов будет обогащена некоторыми существенными чертами. Однако уже сейчас мы можем провести

интересное сравнение наших простых объектов с обсужденными ранее АТД.

При самом поверхностном взгляде эти два типа программистских идиом лежат на противополож-

ных концах спектра: в процессе программирования через АТД пакеты открываются немедленно после

создания; с другой стороны, когда пакеты используются для построения объектов, они остаются за-

крытыми как можно дольше — до момента, когда их приходится открывать, чтобы применить один

из методов к внутреннему состоянию объекта.

Вследствие этого различия «абстрактный тип счетчиков» в этих двух стилях означает разные вещи.

В программе, написанной в стиле с АТД, значения счетчиков, с которыми работает клиентский код

вроде функции add3, являются элементами внутреннего типа представления (т. е., обыкновенными

числами). В объектной программе каждый счетчик представляет собой отдельный пакет — включая

не только число, но и представления методов get и inc. Это стилистическое различие отражается в

том, что в стиле с АТД тип Counter является связанной переменной, вводимой в конструкции let, а в

объектном стиле Counter обозначает весь экзистенциальный тип

{ X , { state :X , method s :{ get :X -> Nat , inc :X ->X }}}

Таким образом, во время исполнения все значения счетчиков, порожденные АТД — это просто неупа-

кованные элементы одного и того же типа представления, и существует единственная реализация опе-

раций со счетчиками, которая работает с этим внутренним представлением. Напротив, каждый объект-

счетчик несет свой тип представления и свой собственный набор методов, работающих с этим типом

представления.

Эти расхождения между АТД и объектами приводят к различным практическим достоинствам и

недостаткам. Одно очевидное отличие состоит в том, что, поскольку каждый объект сам выбирает свое

представление и несет свои собственные операции, в одной программе можно работать с несколькими

представлениями одного и того же типа объектов. Это особенно удобно, когда в системе присутствует

наследование: можно определить один общий тип объектов, а затем породить множество уточнений,

каждое из которых обладает своим несколько (или сильно) отличным внутренним представлением.

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

работать один общий код, их можно совместно хранить в списках и т. п.

Например, библиотека пользовательского интерфейса может определить общий класс Window

(окно) с подклассами вроде TextWindow (текстовое окно), ContainerWindow (окно-контейнер),

ScrollableWindow (окно с полосами прокрутки), TitledWindow (окно с заголовком), DialogBox (диало-

говое окно) и т. д. В каждом из этих подклассов будут собственные переменные экземпляра (например,

TextWindow может содержать переменную типа String, представляющую текущее содержимое окна, а

ContainerWindow может хранить список объектов типа Window), и у него будут свои собственные реали-

зации для операций вроде repaint (перерисовка) и handleMouseEvent (обработка события с мышью).

С другой стороны, определение типа Window как АТД ведет к менее гибкой структуре. Конкретный

тип представления Window должен будет содержать вариантный тип (§11.10) с вариантом для каж-

дой разновидности окна, и к этому варианту будут приписаны данные, относящиеся именно к этой

разновидности. Операции вроде repaint будут содержать case по вариантам и выполнять соотвеству-

ющий специализированный код. Если разновидностей окон существует много, монолитное объявление

абстрактного типа Window может стать слишком большим и запутанным.

rev. 104

292 24.2. Абстракция данных при помощи экзистенциальных типов

Второе важное практическое различие между объектами и АТД касается статуса бинарных операций

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

обсуждение этого вопроса было понятным, требуется различать два вида бинарных операций:

• Некоторые бинарные операции можно реализовать целиком в терминах публично доступных опе-

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

на равенство, надо только спросить у каждого из них его текущее состояние (с помощью get) и

сравнить два полученных числа —т. е., операция equal с тем же успехом может жить за предела-

ми барьера абстракции, защищающего конкретное представление счетчиков. Такие операции мы

будем называть слабыми бинарными операциями.

• Другие бинарные операции невозможно реализовать, не имея конкретного привилегированного

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

щую множества чисел. После изучения нескольких учебников по алгоритмам мы выбираем кон-

кретное представление множеств в виде помеченных деревьев, сохраняющих некоторый сложный

инвариант. Эффективная реализация операции union (объединение) для двух множеств долж-

на рассматривать их конкретно как деревья. Однако мы не хотим давать доступ к конкретному

представлению множеств в нашем публичном интерфейсе абстракции множества. Таким образом,

нужно будет устроить привилегированный доступ операции union к обоим ее аргументам, запре-

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

Такие операции мы будем называть сильными бинарными операциями.

Слабые бинарные операции не представляют сложности ни для одного из рассматриваемых нами сти-

лей, поскольку для них несущественно, помещаем ли мы их внутри или вне барьера абстракции. Если

мы поместим их снаружи, их можно определить просто как отдельно стоящие функции (принимающие

либо объекты, либо значения АТД, как потребуется). Точно так же можно поместить их внутрь АТД

(тогда у них будет конкретный доступ к представлению аргументов, хотя он им и не нужен). Поместить

такую операцию внутрь объекта лишь ненамного сложнее, поскольку теперь тип объекта оказывается

рекурсивным.

EqC o u nter = { X , { state :X , methods :{ get :X ->Nat , inc :X ->X ,

eq :X -> EqCounter -> Bool }}}

Однако сильные бинарные операции в нашей модели невозможно представить как методы объектов.

Мы можем выразить их типы так же, как мы это делали для слабых бинарных методов:

Na tSet = { X , { state :X , method s :{ empty :X , sin g l eton : Nat ->X ,

me mber :X -> Nat - > Bool .

union :X -> NatSet - > X }}}

Однако не существует удовлетворительного способа реализовать объект этого типа: все, что нам из-

вестно о втором аргументе операции union — это что он предоставляет операции типа NatSet, однако

они не дают никакого способа выяснить, каковы элементы множества, и поэтому не из чего вычислять

объединение.

Упражнение 24.2.5 : Почему нельзя использовать следующий тип?

Na tSet = { X , { state :X , method s :{ empty :X , sin g l eton : Nat ->X ,

me mber :X -> Nat - > Bool .

union :X ->X - >X }}}

Подводя итог, единые представления АТД прямо поддерживают бинарные операции, а множествен-

ные представления объектов не предоставляют эту поддержку, но взамен дают полезную гибкость.

Преимущества двух стилей дополняют друг друга; ни один из них не является очевидно лучшим.

К этому обсуждению нужно сделать одну поправку. Приведенные сравнения относятся к простой,

«чистой» модели объектов, описанной в этой главе. Классы в популярных объектно-ориентированных

Такая разновидность рекурсии нетривиальным образом взаимодействует с наследованием, см. (Bruce et al. 1996).

rev. 104

24.3. Кодирование экзистенциальных типов 293

языках программирования вроде C или Java позволяют определять некоторые разновидности силь-

ных бинарных методов. Лучше всего их описать как некоторый компромисс между чистыми объектами

и чистыми АТД, рассмотренными нами в этой главе. В этих языках типом объекта в точности является

имя класса, который этот объект породил, и этот класс считается отличным от имен всех остальных

классов, даже если они предоставляют в точности те же операции (см. §19.3). А именно, каждый тип

объектов в этих языках имеет единственную реализацию, данную в соответствующем объявлении клас-

са. Более того, подклассы в этих языках могут добавлять переменные экземпляра только к тем, которые

унаследованы от надклассов. Следствием этих ограничений является то, что объект, принадлежащий

типу C, всегда обладает всеми переменными экземпляра, упомянутыми в (единственном) объявлении

класса C (и возможно, некоторыми другими). Поэтому для метода такого класса имеет смысл прини-

мать другой C в качестве аргумента и конкретно обращаться ко всем его переменным экземпляра, если

он использует только те переменные, которые определены в C. Поэтому сильные бинарные операции

вроде union могут быть определены в качестве методов. Такого рода «гибридные» объектные модели

формально описаны в работах Пирса и Тёрнера (Pierce and Turner 1993) и Катияра и др. (Katiyar et al.

1994). Более подробно их изучали Фишер и Митчелл (Fisher and Mitchell 1996, 1998; Fisher 1996b, a).

24.3. Кодирование экзистенциальных типов

Кодирование пар в виде полиморфного типа в §23.4.4 подсказывает нам, что подобным же обра-

зом экзистенциальные типы можно закодировать как универсальные, поскольку интуитивно элемент

экзистенциального типа представляет собой пару из типа и значения:

{ X,T}

def

( Y.T Y) Y.

А именно, экзистенциальный пакет рассматривается как значение, которое, получая тип результата и

продолжение, вызывает продолжение и получает окончательный результат. Продолжение принимает

два аргумента — тип X и значение типа T, — и использует их при вычислении окончательного результата.

Такое представление экзистенциальных типов однозначно определяет кодирование конструкций

упаковки и распаковки. Чтобы закодировать пакет

{*S,t} as { X,T}

мы должны с помощью S и t построить значение типа Y. ( X.T Y) Y. Тип начинается с универ-

сального квантора, телом которого является функциональный тип. Следовательно, элемент этого типа

должен начинаться с двух абстракций:

{*S,t} as { X,T}

def

λY. λf:( X.T Y) . . . .

Чтобы закончить построение, нам нужно вернуть результат типа Y; ясно, что получить его можно,

только применив функцию f к подходящим аргументам. Сначала мы даем ей тип S (это естественный

выбор, поскольку других типов в нашем распоряжении сейчас нет):

{*S,t} as { X,T}

def

λY. λf:( X.T Y). f [S] . . .

Применение типа f [S] имеет тип X S (T Y), т. е., ( X S T) Y. Мы можем дать ему как следу-

ющий аргумент терм t, который, согласно правилу T-Pack, имеет тип X S T:

{*S,t} as { X,T}

def

λY. λf:( X.T Y). f [S] t

Типом всего терма-применения f [S] t будет Y, как и требуется.

Чтобы закодировать конструкцию распаковки let {X,x}=t

in t

, мы рассуждаем подобным же

образом. Во-первых, правило типизации T-Unpack говорит нам, что терм t

должен иметь тип вида

{ X,T

}, что t

должен иметь тип T

(в расширенном контексте, включающем связывания X и x:T

и что тип T

ожидается в качестве типа результата всего выражения let...in....

Как и при коди-

рованиии по Чёрчу в §23.4.3, интуиция здесь состоит в том, что форма введения ({*S,t}) кодируется

Строго говоря, то, что перевод требует некоторой информации, отсутствующей в синтаксисе термов, означает, что на

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

определении семантики через преобразования типов для наследования в §15.6.

rev. 104

294 24.4. Дополнительные замечания

в виде активного значения, которое «само производит собственное удаление». Таким образом, коди-

рование формы удаления здесь просто должно взять экзистенциальный пакет t

и применить его к

достаточному количеству аргументов, чтобы получить результат желаемого типа T

let {X,x}=t

in t

def

. . .

Первым аргументом t

должен быть требуемый тип результата для всего выражения, т. е., T

let {X,x}=t

in t

def

] . . .

Тип терма-применения t

] равен ( X. T

) T

. Значит, если сейчас нам удастся передать

ему аргумент типа ( X. T

), задача будет выполнена. Такой аргумент можно получить путем

абстракции тела t

по переменным X и x:

let {X,x}=t

in t

def

] (λX. λx:T

. t

)

Кодирование завершено.

Упражнение 24.3.1 Рекомендуется, : Возьмите чистый лист бумаги и, не заглядывая в кни-

гу, восстановите кодирование, приведенное выше.

Упражнение 24.3.2 : Какие утверждения нам нужно доказать, чтобы быть уверенными, что

кодирование экзистенциальных типов выполнено правильно?

Упражнение 24.3.3 : Можно ли провести операцию в обратном направлении и закодировать

универсальные типы в терминах экзистенциальных?

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

Соответствие между АТД и экзистенциальными типами впервые было описано Митчеллом и Плот-

киным (Mitchell and Plotkin 1988). Они же заметили и связь с объектами. Пирс и Тёрнер (Pierce and

Turner 1994) детально исследовали эту связь — см. Главу 32, где приведены подробности и дальнейшие

ссылки. Взаимодополняющие преимущества объектов и АТД обсуждали Рейнольдс (Reynolds 1975),

Кук (Cook 1991), Брюс и др. (Bruce et al. 1996) и многие другие. В частности, работа Брюса и др.

(Bruce et al. 1996) содержит подробное обсуждение бинарных методов.

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

простой формы абстрактных типов данных. Для адекватного отображения (близкой, но намного более

богатой) проблематики систем модулей, наличествующих в языках вроде ML, исследовались многие

более сложные механизмы. Начать изучение литературы в этой области можно с работ Карделли и

Леруа (Cardelli and Leroy 1990), Леруа (Leroy 1994), Харпера и Лилибриджа (Harper and Lillibridge

1994), Лилибриджа (Lillibridge 1997), Харпера и Стоуна (Harper and Stone 2000) и Крэри и др. (Crary

et al. 2002).

Структура типов представляет

собой синтаксическую

дисцилину для обеспечения

уровней абстракции.

Джон Рейнольдс (Reynolds

1983)

rev. 104

Глава 25

Реализация Системы F на ML

В этой главе мы расширяем реализацию λ из Главы 10 и включаем в нее универсальные и эк-

зистенциальные типы из Глав 23 и 24. Поскольку правила, определяющие эту систему, управляются

синтаксисом (подобно самой λ , но в отличие от исчислений с наследованием или эквирекурсивными

типами), реализация ее на OCaml не представляет труда. Наиболее интересное расширение по срав-

нению с интерпретатором λ состоит в представлении типов, которые могут включать связывания

переменных (в кванторах). Для этих типов мы используем метод индексов де Брауна, введенный нами

в Главе 6.

25.1. Представление типов без использования имен

Для начала мы расширяем синтаксис типов типовыми переменными, а также кванторами общности

и существования.

type ty =

TyVar of int * int

| TyArr of ty * ty

| TyAll of string * ty

| TySome of string * ty

Здесь действуют такие же соглашения, как при представлении термов в §7.1. Типовые переменные

состоят из двух целых чисел: первое указывает расстояние до конструкции, связывающей перемен-

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

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

Затем мы расширяем контексты, позволяя им хранить связывания для типовых переменных помимо

термовых. Для этого мы добавляем новый конструктор в тип binding:

type bindin g =

Nam eBind

| VarBind of ty

| Ty V a rBind

Как и в предшествовавших интерпретаторах, связывание NameBind используется только функциями

синтаксичского анализа и распечатки. Конструктор VarBind несет при себе тип, как и раньше. Новый

конструктор TyVarBind никаких дополнительных данных не несет, поскольку (в отличие от термовых

переменных) типовые переменные в этой системе не привязаны ни к каким дополнительным ограни-

чениям. В системе с ограниченной квантификацией (Глава 26) и видами высшего порядка (Глава 29) с

каждым TyVarBind будет связана соответствующая аннотация.

295

296 25.2. Сдвиг типов и подстановка

25.2. Сдвиг типов и подстановка

Поскольку теперь типы содержат переменные, требуется определить функции для сдвига и подста-

новки типов.

Упражнение 25.2.1 : Используя в качестве образца функцию сдвига термов из Определения 6.2.1

(стр. 68), выпишите математическое определение аналогичной функции, сдвигающей переменные в

типах.

В §7.2 мы построили сдвиг и подстановку для термов как две отдельные функции, но отметили,

что реализация, доступная на сайте книги, использует единую функцию «отображения» для обеих

задач. Можно определить подобную функцию отображения также для сдвига и подстановки типов.

Рассмотрим теперь эти функции.

Основное наблюдение состоит в том, что сдвиг и подстановка ведут себя совершенно одинаково со

всеми конструкторами, кроме переменных. Если мы абстрагируем их поведение на переменных, они

совпадают. Вот, например, специализированная функция сдвига для типов, которую мы получаем,

механически переводя на OCaml решение Упражнения 25.2.1:

let t y p e S h i ft A b o v e d c tyT =

let rec walk c tyT = match tyT with

TyVar (x ,n) -> if x >= c then TyVar (x+d ,n+d ) else TyVar (x ,n +d)

| TyArr ( tyT1 , tyT2 ) -> TyArr ( walk c tyT1 , walk c tyT2 )

| TyAll ( tyX , tyT2 ) -> TyAll (tyX , walk (c +1) tyT2 )

| TySome ( tyX , tyT2 ) -> tySome ( tyX , walk (c +1) tyT2 )

in walk c tyT

Аргументами для этой функции являются число d, на которое требуется сдвинуть свободные перемен-

ные, отсечение c, ниже которого сдвигать не следует (чтобы избежать сдвига переменных, связанных

кванторами внутри типа), и подлежащий сдвигу тип tyT.

Если мы абстрагируем обработку варианта TyVar из typeShiftAbove в новый аргумент onvar, а

также избавимся от аргумента d, упомниаемого только в варианте TyVar, мы получим обобщенную

функцию отображения

let tymap onvar c tyT =

let rec walk c tyT = match tyT with

TyArr ( tyT1 , tyT2 ) -> TyArr ( walk c tyT1 , walk c tyT2 )

| TyVar (x ,n ) -> onvar c x n

| TyAll ( tyX , knK1 , tyT2 ) -> TyAll ( tyX , knK1 , walk (c +1) tyT2 )

| TySome ( tyX , knK1 , tyT2 ) -> TySome (tyX , knK1 , walk (c +1) tyT2 )

in walk c tyT

откуда функцию сдвига можно восстановить, снабдив tymap вариантом для TyVar в качестве параметра

(функции, абстрагированной по c, x и n):

let t y p e S h i ft A b o v e d c tyT =

tymap

( fun c x n -> if x >= c then TyVar ( x+d ,n+ d ) else TyVar (x ,n+d ))

c tyT

Удобно также определить специализированную версию typeShiftAbove для случая, когда исходное

отсечение равно 0:

let typeShift d tyT = ty p e S h i f tA b o v e d 0 tyT

При помощи другой конкретизации tymap можно также реализовать операцию подстановки типа

tyS вместо типовой переменной номер j в типе tyT:

let typeSubst tyS j tyT =

tymap

( fun j x n -> if x = j then ( type S h ift j tyS ) else ( TyVar (x ,n )))

j tyT

rev. 104

25.3. Термы 297

Когда мы будем при проверке типов и вычислении использовать подстановку типов, подстановка

всегда будет производиться вместо нулевой (самой внешней) переменной, и нам всегда нужно будет

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

typeSubstTop.

let t y p e S u b s t T o p tyS tyT =

typ e S hift ( -1) ( t ypeSubst ( typeS h ift 1 tyS ) 0 tyT )

25.3. Термы

На уровне термов требуется проделать подобную же работу. Сначала мы расширяем тип данных

term из Главы 10 формами введения и удаления универсальных и экзистенциальных типов:

type term =

TmVar of info * int * int

| TmAbs of info * st ring * ty * term

| TmApp of info * term * term

| TmTAbs of info * string * term

| TmTApp of info * term * ty

| TmPack of info * ty * term * ty

| Tm Unpack of info * string * string * term * term

Определения сдвига и подстановки для термов подобны тем, что мы видели в Главе 10. Однако

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

типов. Функция отображения выглядит так:

let tmmap onvar ontype c t =

let rec walk c t = match t with

TmVar ( fi ,x ,n ) -> on var fi c x n

| TmAbs ( fi , x , tyT1 , t2 ) -> TmAbs ( fi ,x , ont ype c tyT1 , walk (c +1) t2 )

| TmApp ( fi , t1 , t2 ) -> TmApp ( fi , walk c t1 , walk c t2 )

| TmTAbs ( fi , tyX , t2 ) -> TmTAbs (fi , tyX , walk ( c +1) t2 )

| TmTApp ( fi , t1 , tyT2 ) -> TmTApp (fi , walk c t1 , on type c tyT2 )

| TmPack ( fi , tyT1 , t2 , tyT3 ) ->

Tm Pack (fi , ontype c tyT1 , walk c t2 , ontype c tyT3 )

| Tm Unpack (fi , tyX ,x , t1 , t2 ) ->

TmU npack ( fi , tyX ,x , walk c t1 , walk (c +2) t2 )

in walk c t

Заметим, что tmmap принимает четыре аргумента — на один больше, чем tymap. Чтобы понять, почему,

обратите внимание, что термы могут содержать два различных типа переменных: термовые переменные

и типовые переменные, встроенные в аннотации типа внутри термов. Поэтому, например, при сдвиге

есть два типа «листьев», где нам может потребоваться проделать какую-то существенную работу: тер-

мовые переменные и типы. Параметр ontype сообщает функции отображения, что следует делать при

обработке конструктора термов, содержащего аннотацию типа, как, например, в случае TmAbs. Если

бы у нас был язык большего размера, было бы еще несколько таких случаев.

Сдвиг термов можно определить, передав соответствующие аргументы в tmmap.

let t e r m S h i ft A b o v e d c t =

tmmap

( fun fi c x n -> if x >= c then TmVar ( fi ,x+d ,n+d )

else TmVar (fi ,x ,n+d ))

( typeShiftA b o v e d )

c t

Функция для подстановки одного терма вместо другого выглядит подобным же образом:

let termSubst j s t =

tmmap

( fun fi j x n -> if x = j then term S hift j s else TmVar (fi ,x , n))

rev. 104

298 25.4. Вычисление

( fun j tyT -> tyT )

j t

Заметим, что аннотации типов не изменяются в termSubst (типы не могут содержать термовых пере-

менных, так что подстановка термов на них никак не влияет).

Нам также нужна функция для подстановки типа в терм — она используется, например, в правиле

вычисления для применения типа:

(λX.t

) [T

] X T

(E-TappTabs)

Ее также можно определить через функцию отображения термов:

let rec t y t e rmSubst tyS j t =

tmmap ( fun fi c x n -> TmVar ( fi ,x ,n ))

( fun j tyT -> type S ubst tyS j tyT ) j t

В этом случае функция, которую мы передаем в tmmap для обработки термовых переменных — функция

тождества (она просто восстанавливает исходную термовую переменную); когда мы видим аннотацию

типа, мы проводим в ней подстановку на уровне типов.

Наконец, как мы это делали для типов, определяем вспомогательные функции, упаковывающие

базовые функции подстановки для удобства eval и typeof.

let t e r m S u b s t T o p s t =

ter m S hift ( -1) ( t ermSubst 0 ( termS h ift 1 s) t)

let t y t e r m S ub s t T o p tyS t =

ter m S hift ( -1) ( t y t e r m Subst ( typeShift 1 tyS ) 0 t )

25.4. Вычисление

Расширения функции eval прямо порождаются на основе правил вычисления с Рис. 23.1 и 24.1. Вся

сложная работа уже проделана в функциях подстановки из предыдущего раздела.

let rec eval1 ctx t = match t with

...

| TmTApp ( fi , TmTAbs (_ ,x ,_ , t11 ), tyT2 ) ->

tytermSubstTop tyT2 t11

| TmTApp ( fi , t1 , tyT2 ) ->

let t1 ’ = eval1 ctx t1 in

Tm TApp (fi , t1 ’ , tyT2 )

| Tm Unpack (fi ,_ ,_ , TmPack (_ , tyT11 , v12 , _), t2 ) when isval ctx v12 ->

tytermSubstTop tyT11 ( termSubstTop ( termShi f t 1 v12 ) t2 )

| Tm Unpack (fi , tyX ,x , t1 , t2 ) ->

let t1 ’ = eval1 ctx t1 in

TmU npack ( fi , tyX ,x , t1 ’ ,t2 )

| TmPack ( fi , tyT1 , t2 , tyT3 ) ->

let t2 ’ = eval1 ctx t2 in

Tm Pack (fi , tyT1 ,t2 ’ , tyT3 )

...

Упражнение 25.4.1 : Почему в первом варианте TmUnpack требуется termShift?

25.5. Типизация

Новые варианты в функции typeof также прямо следуют из правил типизации для абстракции

и применения типов, а также для упаковки и распаковки экзистенциальных пакетов. Мы приводим

полное определение typeof, так что новые варианты для TmTAbs и TmTApp можно сравнить со старыми,

для обычной абстракции и обычного применения функции.

rev. 104

25.5. Типизация 299

let rec type of ctx t =

match t with

| TmVar ( fi , i ,_) -> getT y p e Fr o m C on t e xt fi ctx i

| TmAbs ( fi , x , tyT1 , t2 ) ->

let ctx ’ = ad d b i n ding ctx x ( VarBin d ( tyT1 )) in

let tyT2 = typeof ctx ’ t2 in

TyArr ( tyT1 , typeShift ( -1) tyT2 )

| TmApp ( fi , t1 , t2 ) ->

let tyT1 = typeof ctx t1 in

let tyT2 = typeof ctx t2 in

( match tyT1 with

TyArr ( tyT11 , tyT12 ) ->

if tyeqv ctx tyT2 tyT11 then tyT12

else err or fi "несоответствие типа параметра"

| _ -> error fi "ожидается функциональный тип" )

| TmTAbs ( fi , tyX , t2 ) ->

let ctx = addbinding ctx tyX TyVarBin d in

let tyT2 = typeof ctx t2 in

TyAll ( tyX , tyT2 )

| TmTApp ( fi , t1 , tyT2 ) ->

let tyT1 = typeof ctx t1 in

( match tyT1 with

TyAll (_ , tyT12 ) -> t y p e S u b s t T o p tyT2 tyT12

| _ -> error fi "ожидается универсальный тип" )

| TmPack ( fi , tyT1 , t2 , tyT ) ->

( match tyT with

Ty Some (tyY , tyT2 ) ->

let tyU = typeof ctx t2 in

let tyU ’ = typeSubstTop tyT1 tyT2 in

if (=) tyU tyU ’ then tyT

else err or fi "несоответствие объявленному типу"

| _ -> error fi "ожидается экзистенциальный тип" )

| Tm Unpack (fi , tyX ,x , t1 , t2 ) ->

let tyT1 = typeof ctx t1 in

( match tyT1 with

Ty Some (tyY , tyT11 ) ->

let ctx ’ = ad d b i n ding ctx tyX T y VarBind in

let ctx ’’ = addbind i n g ctx ’ x ( VarBind tyT11 ) in

let tyT2 = typeof ctx ’ ’ t2 in

typ e S hift ( -2) tyT2

| _ -> error fi "ожидается экзистенциальный тип" )

Наиболее интересный участок кода — случай TmUnpack. Здесь производятся следующие шаги: (1)

Проверяем тип подвыражения t

и убеждаемся, что оно имеет экзистенциальный тип { X,T

}. (2)

Расширяем контекст Γ связыванием типовой переменной X и связыванием термовой переменной x:T

и убеждаемся, что t

имеет некоторый тип T

. (3) Сдвигаем индексы свободных переменных в T

вниз на

два, так что этот тип имеет смысл относительно исходного контекста Γ. (4) Возвращаем получившийся

тип в качестве типа всего выражения let...in....

Ясно, что если X имеет свободные вхождения в T

, то на шаге (3) мы получим бессмысленный

тип, содержащий свободные переменные с отрицательными индексами; в этом месте проверка типов

должна потерпеть неудачу. Мы можем этого добиться, если переопределим функцию typeShiftAbove

так, чтобы она замечала попытки создать типовую переменную с отрицательным индексом, и сообщала

об ошибке, а не возвращала бессмыслицу.

let t y p e S h i ft A b o v e d c tyT =

tymap

( fun c x n -> if x >= c then

if x +d <0 then err "Неверная область видимости!"

else TyVar (x +d ,n+ d )

rev. 104

300 25.5. Типизация

else TyV ar (x , n+d ))

c tyT

Такая проверка будет сообщать об ошибке области видимости всякий раз, когда тип, вычисляемый нами

для тела t

конструкции удаления экзистенциального типа let {X,X}=t

in t

, содержит связанную

типовую переменную X.

let {X ,x }=({* Nat ,0} as { X ,X }) in x ;

Ошибка: Неверная область видимости!

rev. 104