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

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

19.3. Именные и структурные системы типов 201

У именных систем типов есть как преимущества, так и недостатки в сравнении со структурными.

Возможно, самое большое преимущество состоит в том, что имена типов в именных системах полез-

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

каждый объект во время выполнения помечается словом-заголовком, которое содержит имя типа, пред-

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

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

стирования во время выполнения (например, в Java, для теста instanceOf и при операции приведения

вниз), для печати, для сериализации структур данных в бинарные строки, предназначенные для хра-

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

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

гут поддерживаться и в структурных системах (см. Glew 1999; League, Shao and Trifonov 1999; League,

Trifonov and Shao 2001, а также списки литературы в этих работах), однако там они представляют

собой дополнительный, отдельный механизм; в именных системах метки типа совпадают с типами,

проверяемыми на стадии компиляции.

Менее существенное, но тоже приятное, свойство именных систем — то, что они предлагают есте-

ственный и интуитивно ясный подход к рекурсивным типам, — типам, определение которых упоминает

сам тип. (Мы будем подробно обсуждать рекурсивные типы в Главе 20.) Такие типы встречаются при

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

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

возможных способов: сослаться на List в теле его собственного объявления так же просто, как и на лю-

бой другой тип. Даже взаимно рекурсивные типы не требуют никаких специальных усилий. Множество

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

тип B, а определение типа B — тип A, не возникает вопроса, «кто из них раньше определен». Разумеет-

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

языки вроде ML обычно «упаковывают» рекурсивные типы вместе с другими характеристиками си-

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

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

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

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

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

Еще одно преимущество именных систем состоит в том, что проверка, является ли один тип подти-

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

работу по проверке, что объявленные отношения наследования безопасны, что, по существу, дублирует

структурное отношение наследования, но эту работу требуется проделать только один раз для каждого

типа, там, где этот тип определен, а не при каждой проверке на наследование. Поэтому в программах

проверки типов для именных систем типов несколько проще достигнуть хорошей производительно-

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

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

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

представления данных, сводящие большинство проверок на наследование к простому сравнению, — см.

стр. 178.

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

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

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

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

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

абстрактные типы данных (Глава 24).

При всех этих преимуществах, — особенно полезны метки типа и простое обращение с рекурсивными

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

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

работает почти исключительно со структурными системами типов.

Одна из непосредственных причин этого — то, что, по крайней мере без учета рекурсивных типов,

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

тип — замкнутая сущность; оно содержит в себе все необходимое, чтобы понять его значение. В именной

rev. 104

202 19.4. Определения

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

определений. Как правило, и определения, и доказательства из-за этого оказываются многословнее.

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

с более сложными конструкциями — в частности, с мощными механизмами абстракции типов (па-

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

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

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

List(T) кажется несводимо составным — где-то в программе будет только одно определение конструк-

тора List, и к этому определению требуется обращаться, чтобы понять поведение List(T), так что

рассматривать List(T) как атомарное имя не получается. Некоторые именные языки были расшире-

ны такими «обобщенными» конструкциями (Myers, Bank and Liskov 1997; Agesen, Freund and Mitchell

1997; Bracha, Odersky, Stoutamire and Wadler 1998; Cartwright and Steele 1998; Stroustrup 1997), но в

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

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

предпочитают структурный подход.

Прояснение отношений между именными и структурными системами типов остается темой актив-

ных исследований.

19.4. Определения

Мы приступаем к формальному определению FJ.

19.4.1. Синтаксис

Синтаксис FJ приведен на Рис. 19.1. Метапеременные A, B, C и D имеют своими значениями име-

на классов; f и g — имена полей; m — имена методов; x — имена параметров; s и t — термы; u и

v — значения; Cl — объявления классов; K — объявления конструкторов; M — объявления методов.

Мы предполагаем, что множество переменных включает особую переменную this, но что this нико-

гда не служит именем аргумента метода. При этом this считается неявно связанной в теле каждого

объявления метода. Правило вычисления для вызовов методов (E-InvkNew на Рис. 19.3) подставит

соответствующий объект вместо переменной this, в дополнение к подстановке значений аргументов

вместо имен параметров.

Мы пишем f как сокращение f

,...,f

(и подобным образом C, x, t и т. п.), а также M как сокраще-

ние M

...M

(без запятых). Подобным образом мы сокращаем и операции над парами последовательно-

стей, а именно «C f» вместо «C

,...,C

», где n — длина последовательностей C и f, «C f;» вместо

«C

;...C

;» и this.f=f; вместо «this.f

;...;this.f

;». Предполагается, что последо-

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

имен.

Объявление class C extends D {C f; K M} вводит класс с именем C и надклассом D. Новый класс

имеет поля f с типами C, единственный конструктор K и набор методов M. Переменные экземпляра,

объявленные внутри C, добавляются к тем, которые были объявлены в D и его надклассах. Имена новых

переменных должны отличаться от старых.

Напротив, методы C могут либо переопределять методы

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

именно C.

Объявление конструктора C (C f) {super(f); this.f=f;} показывает, как следует инициализи-

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

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

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

инициализирующего поля параметрами g, а затем параметры f присваиваются полям с теми же име-

нами, объявленным в классе C. (Эти ограничения проверяются в правиле типизации для классов на

В Java переменные экземпляра надкласса могут объявляться заново — такое определение скрывает исходную пере-

менную в текущем классе и его подклассах. В FJ мы опускаем это свойство языка.

rev. 104

19.4. Определения 203

Синтаксис

CL ::= объявления классов:

class C extends C {C f; K M}

K ::= объявления конструкторов:

C (C f) {super(f); this.f=f;}

M ::= объявления методов:

C m(C x) {return t}

t ::= термы:

x переменная

t.f обращение к полю

t.m(t) вызов метода

new C(t) создание объекта

(C)t приведение типа

v ::= значения:

new C(v) создание объекта

Наследование C<:D

C <: C

C <: D D <: E

C <: E

CT C class C extends D {...}

C <: D

Рис. 19.1. Облегченная Java (синтаксис и наследование)

Рис. 19.4.) В полной Java конструктор подкласса должен содержать вызов конструктора надкласса (ес-

ли конструктор надкласса принимает аргументы); именно поэтому здесь тело конструктора вызывает

super для инициализации полей экземпляра. Если бы нас не заботила задача сделать FJ строгим под-

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

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

Объявление метода D m(C x) {return t} вводит метод с именем m, типом результата D и параметра-

ми x типов С. Телом метода является единственный оператор return t. Переменные x связаны внутри

t. Кроме того, считается, что внутри t связана особая переменная this.

Таблица классов CT — отображение имен классов C на объявления классов CL. Программа пред-

ставляет собой пару CT, t , состоящую из таблицы классов и терма. Чтобы облегчить нотацию в

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

У каждого класса есть надкласс, объявляемый через extends. Отсюда возникает вопрос: какой

надкласс имеет класс Object? Есть несколько способов справиться с этой сложностью; простейшее

решение, которое мы здесь принимаем — считать Object особо выделенным именем класса, определение

которого отсутствует в таблице классов. Вспомогательная функция, ищущая поля в таблице классов,

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

обозначаемую ; предполагается также, что у класса Object нет методов.

Глядя на таблицу классов, мы можем считать отношение наследования между классами. За-

пись C <: D будет означать, что C является подтипом D – то есть, отношение наследования — это

транзитивно-рефлексивное замыкание отношения непосредственного наследования, задаваемого выра-

жениями extends в CT . Формально оно определяется на Рис. 19.1.

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

ям: (1) CT C class C... для каждого C dom CT ; (2) Object dom CT ; (3) Для каждого имени

класса C, встречающегося где-либо в CT , выполняется C dom CT ; (4) в отношении наследования,

построенном на основе CT , нет циклов — т. е., отношение <: антисимметрично.

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

что определение A может использовать A как тип своих методов и переменных экземпляра. Разрешена

и взаимная рекурсия между определениями классов.

В полной Java у класса Object есть несколько методов. В языке FJ мы их игнорируем.

rev. 104

204 19.4. Определения

Поиск полей ﬁelds C C f

ﬁelds Object

CT C class C extends D {C f; K M} ﬁelds D D g

ﬁelds C D g, C f

Поиск типов методов mtype m, C C C

CT C class C extends D {C f; K M} B m (B x) {return t;} M

mtype m, C B B

CT C class C extends D {C f; K M} m не определен в M

mtype m, C mtype m, D

Поиск тел методов mbody m, C (x,t)

CT C class C extends D {C f; K M} B m (B x) {return t;} M

mbody m, C (x,t)

CT C class C extends D {C f; K M} m не определен в M

mbody m, C mbody m, D

Разрешенное переопределение драйверов override m, D, C C

для каждого mtype m, D D D, имеем C D и C

override m, D, C C

Рис. 19.2. Облегченная Java (вспомогательные определения)

Упражнение 19.4.1 : По аналогии с правилом S-Top, в нашем лямбда-исчислении с наследованием

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

Почему оно нам здесь не нужно?

19.4.2. Вспомогательные определения

В правилах типизации и вычисления мы будем пользоваться некоторыми вспомогательными опре-

делениями. Эти определения представлены на Рис. 19.2. Поля класса C, запиываемые ﬁelds C , пред-

ставляют собой последовательность C f, связывающую тип каждого поля с его именем, для всех полей,

объявленных в классе C и его надклассах. Тип метода m в классе C, обозначаемый mtype m, C — пара,

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

тата B. Подобным образом, тело метода m в классе C, обозначаемое mbody m, C , — пара, записываемая

как (x,t), состоящая из последовательности параметров x и терма t. Предикат override m, D, C C

решает, можно ли определить метод m с типами аргументов C и типом результата C

в подклассе класса

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

иметь тот же самый тип.

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

Мы используем стандартную операционную семантику с вызовом по значению (Рис. 19.3). Три

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

в §19.2. Остальные правила формализуют стратегию вызова по значению. Значения, которые могут

получиться при нормальном завершении вычислителя, — это полностью вычисленные термы создания

объектов вида new C(v).

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

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

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

соответствует семантике Java: приведение во время выполнения никак на объект не воздействует, —

оно либо завершается успешно, либо терпит неудачу и порождает исключение. В FJ, вместо того,

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

никакое правило вычисления к нему не применимо.

rev. 104

19.4. Определения 205

Вычисление t t’

ﬁelds C C f

new C(v).f

(E-ProjNew)

mbody m, C (x,t

)

new C(v).m(u) x u, this new C(v) t

(E-InvkNew)

C <: D

(D)(new C(v)) new C(v)

(E-CastNew)

.f t

(E-Field)

.m(t) t

.m(t)

(E-Invk-Recv)

.m(v, t

, t) v

.m(v, t

, t)

(E-Invk-Arg)

new C(v, t

, t) new C(v, t

, t)

(E-New-Arg)

(C)t

(E-Cast)

Рис. 19.3. Облегченная Java (вычисление)

Типизация термов Γ t : C

x:C Γ

Γ x : C

(T-Var)

Γ t

: C

ﬁelds C

C f

Γ t

: C

(T-Field)

Γ t

: C

mtype m, C

D C Γ t : C C <: D

Γ t

.m(t) : C

(T-Invk)

ﬁelds C D f Γ t : C C <: D

Γ new C(t) : C

(T-New)

Γ t

: D D <: C

Γ (C)t

: C

(T-UCast)

Γ t

: D C <: D C D

Γ (C)t

: C

(T-DCast)

Γ t

: D C : D D : C предупреждение о глупости

Γ (C)t

: C

(T-SCast)

Типизация методов M OK в C

x:C, this:C t

<: C

CT C class C extends D {...} override m, D, C C

m (C x) {return t

} OK в C

Типизация классов C OK

K C(D g, C f) {super(g); this.f=f} ﬁelds D D g M OK в C

class C extends D {C f; K M} OK

Рис. 19.4. Облегченная Java (типизация)

19.4.4. Типизация

Правила типизации для термов, объявлений методов и объявлений классов приведены на Рис. 19.4.

Контекст Γ представляет собой конечное отображение переменных на типы, записываемое x:C. Утвер-

ждения о типизации для термов имеют вид Γ t : C, что читается «в контексте Γ терм t имеет

тип C». Правила типизации управляются синтаксисом,

причем для каждого типа терма имеется по

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

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

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

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

сокращением для Γ x

, . . . , Γ x

, а C <: D для C

<: D

, . . . , C

<: D

Небольшой технической инновацией в FJ является понятие «глупого» приведения типа. Есть три

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

что в настоящей Java только такую формулировку и можно выбрать. См. Упражнение 19.4.6.

rev. 104

206 19.4. Определения

типа приведений: приведение вверх, где тип приводимого объекта является подклассом целевого типа,

приведение вниз, где тип приводимого объекта — надкласс целевого типа, и глупое приведение, где

между двумя типами нет никакого отношения наследования. Компилятор Java отвергает терм, где со-

держится глупое приведение, как неверный, однако мы вынуждены разрешать глупые приведения в FJ,

если хотим сформулировать теорему о сохранении типов в семантике с малым шагом. Это происходит

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

Рассмотрим, например, следующее выражение, где используются классы A и B, определенные в §19.2:

(A)(Object)new B() (A)new B()

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

в правило T-SCast; типизация в FJ соответствует типизации в Java только в том случае, если это

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

Утверждения о типизации для объявлений методов имеют вид M OK в C, что читается «объявление

метода M сформулировано верно, если оно встречается в классе C». При выводе используется отношение

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

для них типами, плюс особая переменная this типа C.

Утверждения о типизации для классов имеют вид C OK, что читается «оъявление класса C сфор-

мулировано верно». При выводе проверяется, что конструктор вызывает super с полями надкласса

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

верны.

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

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

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

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

проверены все классы в этой таблице. Достаточно, чтобы каждый класс был в конце концов проверен.

Упражнение 19.4.2 : Множество проектных решений в FJ продиктованы желанием сделать

язык подмножеством Java, в смысле, что каждая правильно или неправильно типизированная про-

грамма на FJ должна быть, соответственно, правильно или неправильно типизирована на Java, и

поведение правильно типизированных программ должно быть одинаково в обоих языках. Предполо-

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

подобное базовое исчисление. Как бы Вы изменили FJ, чтобы язык получился проще или изящнее?

Упражнение 19.4.3 Рекомендуется, : Операция присваивания нового значения полю объек-

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

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

Главы 13.

Упражнение 19.4.4 : Расширьте FJ аналогами конструкций try и raise из Java. Исполь-

зуйте описание исключений из Главы 14 как образец.

Упражнение 19.4.5 : Подобно Java, FJ представляет отношение типизации в алгоритмиче-

ской форме. Правило включения отсутствует; вместо этого, несколько других правил содержат

проверку наследования среди своих предпосылок. Можно ли перестроить систему в более деклара-

тивном стиле, исключив все или большинство из этих предпосылок, и добавив вместо этого единое

правило включения?

Упражнение 19.4.6 : В полной Java наряду с классами имеются интерфейсы, указывающие ти-

пы методов, но не их реализацию. Интерфейсы полезны, поскольку с их помощью можно построить

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

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

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

Наличие интерфейсов в Java диктует алгоритмический подход к отношению типизации, посколь-

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

Причина лежит во взаимодействии условных выражений (которые в Java записываются как t

: t

) с интерфейсами.

rev. 104

19.5. Свойства 207

1. Покажите, как расширить FJ интерфейсами в стиле Java.

2. Покажите, что при наличии интерфейсов отношение наследования необязательно замкнуто

относительно объединений. (Напомним, что в §16.3 существование объединений играло ключе-

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

3. Каково правило Java для типизации условных выражений? Разумно ли оно?

Упражнение 19.4.7 : В FJ поддерживается ключевое слово this из Java, но не поддерживается

super. Покажите, как его добавить.

19.5. Свойства

Для FJ можно доказать стандартную теорему о сохранении типов.

Теорема 19.5.1 Сохранение : Если Γ t : C и t t’, то Γ t’ : C’ для некоторого C’ <: C.

Доказательство: Упражнение .

Кроме того, выполняется вариант стандартной теоремы о продвижении: если программа правильно

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

В последнем случае мы для выявления ошибочного приведения пользуемся механизмом контекстов

времени выполнения.

Лемма 19.5.2 Пусть имеется правильно типизированный терм t.

1. Если t new C

(t).f, то ﬁelds C

C f и f f.

2. Если t new C

(t).m(s), то mbody m, C

x, t

и x s .

Доказательство: Не представляет труда.

Определение 19.5.3 Множество контекстов времени выполнения для FJ определяется следующим об-

разом:

E ::= контексты времени выполнения:

дыра

E.f обращение к полю

E.m(t) вызов метода (получатель)

v.m(v,E,t) вызов метода (аргумент)

C(v,E,t) создание объекта (аргумент)

(C)E приведение типа

Контекст времени выполнения — это терм с дырой (обозначаемой ) внутри. Запись E t обозна-

чает обыкновенный терм, получающийся при замене дыры в E на t.

Контексты времени выполнения описывают понятие «следующего подтерма, подлежащего вычис-

лению», в том смысле, что, имея t t’, мы можем единственным образом выразить t и t’ в виде

t E r и t’ E r’ для некоторых E, r и r’, так, чтобы выполнялось r r’ согласно одному из

правил вычисления E-ProjNew, E-InvkNew либо E-CastNew.

Теорема 19.5.4 Продвижение : Пусть имеется замкнутый правильно типизированный терм t в

нормальной форме. Тогда либо (1) t явлется значением, либо (2) для некоторого контекста времени

выполнения E имеем t E (C)(new D(v)) , причем D : C.

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

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

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

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

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

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

Разумеется, в полной Java неудачное приведение не приводит к немедленной остановке программы:

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

rev. 104

208 19.6. Сравнение кодирования и объектов в виде элементарного понятия

Упражнение 19.5.5 : Используя в качестве заготовки одну из программ проверки типов для

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

для Облегченной Java.

Упражнение 19.5.6 : В исходной статье об FJ (Igarashi, Pierce and Wadler 1999), помимо

прочего, проводилась формализация понятия полиморфных типов по образцу GJ. Расширьте про-

грамму проверки типов и интерпретатор из Упражнения 19.5.5, включив в него эти конструкции.

(Прежде, чем Вы попытаетесь выполнить это упражнение, Вам придется прочесть Главы 23, 25,

26 и 28.)

19.6. Сравнение кодирования и объектов в виде элементарного

понятия

Мы рассмотрели два различных подхода к семантике и типизации для простых объектно-

ориентированных языков. В Главе 18 мы закодировали объекты и наследование при помощи набора

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

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

механизмами.

Каждый из этих подходов может быть полезен по-своему. Исследование кодирования объектов об-

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

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

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

а также как объекты взаимодействуют с другими свойствами языка. С другой стороны, подход к объек-

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

поведении с точки зрения типизации; такое представление лучше приспособлено для высокоуровневого

проектирования языков и документации.

Разумеется, в конечном счете хотелось бы сохранить обе точки зрения — иметь высокоуровневый

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

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

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

уровня, где нет ничего, кроме регистров, указателей и последовательностей команд), и, наконец, до-

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

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

ществует много реализаций этой исследовательской программы — для самой FJ это проделали Лиг,

Трифонов и Шао (League, Trifonov and Shao 2001), для других объектно-ориентированных базовых

исчислений Хофман и Пирс (Hoﬀmann and Pierce 1995b), Брюс (Bruce 1994, 2002), Абади, Карделли и

Вишванатан (Abadi, Cardelli and Viswanathan 1996), а также другие авторы.

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

Эта глава написана на основе исходной публикации по FJ Игараси, Пирса и Уодлера (Igarashi, Pierce

and Wadler 1999). Основная разница в представлении материала состоит в том, что здесь, как и вообще

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

время как в исходной статье использовалось недетерминистское отношение бета-редукции.

Существует несколько различных доказательств типовой безопасности для подмножеств Java. В

самом раннем из них Дроссопулу, Айзенбах и Хуршид (Drossopoulou, Eisenbach and Khurshid 1999), ис-

пользуя метод, впоследствии механически проверенный Саймом (Syme 1997), доказывают безопасность

для значительного подмножества последовательной Java. Подобно FJ, они работают в рамках операци-

онной семантики с малым шагом, но они избегают сложных вопросов «глупого приведения», исключая

приведения целиком из своего подмножества. Нипков и Охаймб (Nipkow and Oheimb 1998) приводят ме-

ханически проверенное доказательство безопасности для несколько более широкого базового языка. Их

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

rev. 104

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

шагом», и проблема с глупыми приведениями в таком контексте не возникает. Флатт, Кришнамур-

ти и Феллейсен (Flatt, Krishnamurthi and Felleisen 1998a, 1998b) используют операционную семантику

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

приведения рассматриваются так же, как в FJ. Их система несколько больше FJ по размеру (правила

синтаксиса, типизации и операционной семантики приимерно втрое больше по объему), а доказатель-

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

Из этиз трех работ, работа Флатта, Кришнамурти и Феллейсена ближе всего к FJ с одной важной

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

исчисление, отражающее только те свойства Java, которые важны для некоторой конкретной задачи. В

их случае, задачей было проанализировать расширение Java классами-примесями в стиле Common Lisp.

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

Java, поскольку основной интерес предприятия заключался в доказательстве безопасности Java как

таковой.

В литературе по основаниям объектно-ориентированных языков можно найти множество статей

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

классы как элементарный механизм (напр., Wand 1989a, Bruce 1994, Bono, Patel, Shmatikov and Mitchell

1999b, Bono, Patel and Shmatikov 1999a), либо переводящих классы в более низкоуровневые конструкции

(напр., Fisher and Mitchell 1998, Bono and Fisher 1998, Abadi and Cardelli 1996, Pierce and Turner 1994).

Родственное направление исследований рассматривает модели объектно-ориентированных языков,

где классы заменяются какой-либо формой переопределения или делегации (Ungar and Smith 1987),

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

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

базовых понятий. Самое развитое и самое известное из них – исчисление объектов Абади и Кардел-

ли (Abadi and Cardelli 1996). Еще одно популярное исчисление разработано Фишером, Хонселлом и

Митчеллом (Fisher, Honsell and Mitchell 1994).

Сильно отличающийся поход к объектам, классам и наследованию, известный под названием муль-

тиметоды, формализован Кастаньей, Гелли и Лонго (Castagna, Ghelli and Longo 1995). Дополнитель-

ные ссылки можно найти в примечании на стр. 182.

В каждом большом языке

заключен маленький, и он

пытается выйти наружу.

Игараси, Пирс и Уодлер

(Igarashi, Pierce and Wadler

1999)

В каждой большой программе

заключена маленькая, и она

пытается выйти наружу.

Тони Хоар, Эффективное

производство больших

программ (1970)

Я толстый, но внутри я худой.

Вам никогда не приходило в

голову, что у каждого толстяка

внутри сидит худой человек?

Джордж Оруэлл, Глоток

воздуха (1939)

rev. 104

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

rev. 104