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

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

18.11. Открытая рекурсия и порядок вычислений 191

• Можно защитить ссылку на self в теле instrCounterClass, избежав таким образом ее слишком

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

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

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

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

в Главе 32.

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

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

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

применяем дальнейшие улучшения в Главе 27.

• Можно забыть о кодировании объектов и классов в терминах лямбда-абстракций, записей и fix, и

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

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

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

пытаться обойти проблемы с заранее заданными правилами для применения и fix. Этот подход

развивается в Главе 19.

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

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

t превращается в функцию λ_:Unit.t, называемую санк. Такая «санковая форма» t с точки зрения

синтаксиса является значением; все действия, связанные с вычислением t, откладываются до тех пор,

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

виде а затем, позже, запросить его результат.

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

(напр., SetCounter) на объектный санк (Unit SetCounter). При этом надо (1) изменить тип парамет-

ра self, передаваемого в класс, (2) добавить абстракцию-заглушку прежде, чем мы вернем объект-

результат, и (3) заменить каждое вхождение self в телах методов на (self unit).

setCounterClas s =

λr : Co u n t erRep .

λself : Unit - > SetC o u n t er .

λ_ : Unit .

{ get = λ_: Unit . !( r.x ) ,

set = λi : Nat . r.x := i,

inc = λ_ : Unit . ( self unit ). set ( succ (( self unit ). get unit ))};

setCounterClas s : CounterRep ->

( Unit -> SetCounter ) -> Unit -> SetCounte r

Поскольку мы не хотим изменять тип newSetCounter (эта функция по-прежнему должна возвращать

объект), нам нужно немного модифицировать ее определение, чтобы она передавала аргумент unit в

санк, получающийся при создании неподвижной точки setCounterClass.

newSetCounter =

λ_ : Unit . let r ={ x = ref 1} in

fix ( s et C o u n t e rC l a s s r ) unit ;

newSetCounter : Unit -> SetCount e r

Подобные изменения требуются и в определении instrCounterClass. Заметим, что никакое из них

не требует от нас никких творческих способностей: как только мы изменили тип self, все остальное

вытекает из правил типизации.

instrCoun t e r C l as s =

λr : InstrCounte r .

λself : Unit - > InstrCounter .

λ_ : Unit .

let super = se tC o u n t e r Cl a s s r self unit in

{ get = super . get ,

rev. 104

192 18.12. Более эффективная реализация

set = λi : Nat . (r. a := succ (!( r.a )); super . set i) ,

inc = super .inc ,

acc esses = λ_: Unit . !( r.a )};

instrCoun t e r C l as s : I n s t rC o u n t e r R ep ->

( Unit -> I n s t r C o u n t e r ) -> Unit -> InstrCounter

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

рожденный конструкцией fix.

newInstrCounte r =

λ_ : Unit . let r = {x= ref 1 , a = ref 0} in

fix ( instrCounte r C l a ss r ) unit ;

newInstrCounte r : Unit -> In s t r C o u n t e r

Теперь с помощью newInstrCounter мы можем создать объект.

ic = n e w I n s t r Co u n t e r unit ;

ic : InstrCounter

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

Следующие тесты показывают, что метод accesses подсчитывает обращения и к set, и к inc, как

мы и добивались.

( ic . set 5; ic . ac cesses unit );

1 : Nat

( ic . inc unit ; ic . get unit );

6 : Nat

ic . ac cesses unit ;

2 : Nat

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

дующие расширения к имеющимся у нас классам:

1. Перепишите instrCounterClass, чтобы он подсчитывал также обращения к get.

2. Расширьте свой измененный instrCounterClass подклассом, добавляющим метод reset, как в

§18.4.

3. Добавьте еще один подкласс, который поддерживает еще и резервные значения (метод backup,

§18.7).

18.12. Более эффективная реализация

Тесты в конце предыдущего раздела показывают, что наша реализация классов осуществляет «от-

крытую рекурсию» при вызове методов через self, как это принято в языках вроде Smalltalk, C

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

эффективности. Все санки, вставленные нами для того, чтобы заставить вычисление fix завершаться,

откладывают вычисление таблиц методов для классов. Заметим, в частности, что все вызовы self в

телах методов превращаются в (self unit), — то есть, методы переменной self вычисляются заново

каждый раз, как мы вызываем любой из них!

rev. 104

18.12. Более эффективная реализация 193

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

движных точек для того, чтобы «завязать узел» в иерархии классов при построении объектов.

Вместо

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

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

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

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

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

в ячейке, чтобы она содержала настоящие методы. Вот, например, снова setCounterClass:

setCounterClas s =

λr : Co u n t erRep . λself : Ref SetCounte r .

{ get = λ_: Unit . !( r.x ) ,

set = λi : Nat . r.x :=i ,

inc = λ_ : Unit . (! self ). set ( succ ((! self ). get unit ))};

setCounterClas s : CounterRep -> ( Ref SetCounter ) -> Se t C o u nter

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

setCounterClass эта ячейка инициализируется значением-заглушкой:

dummySetCounte r =

{ get = λ_: Unit . 0,

set = λi : Nat . unit ,

inc = λ_ : Unit . unit };

dummySetCounte r : SetCounter

newSetCounter =

λ_ : Unit .

let r = {x = ref 1} in

let cAux = ref dummySetCounter in

( cAux := ( s e t C o u nt e r C l a s s r cAux ); ! cAux );

newSetCounter : Unit -> SetCount e r

Однако поскольку все операции разыменования (!self) защищены лямбда-абстракциями, никаких об-

ращений к ячейке не будет до тех пор, пока в нее функцией newSetCounter не будет записано настоящее

значение.

Чтобы поддержать построение подклассов setCounterClass, требуется провести еще одно уточнение

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

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

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

видели в §15.5.4, типы Ref SetCounter и Ref InstrCounter несовместимы — невозможно продвинуть

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

пытаемся создать super в определении instrCounterClass.

instrCoun t e r C l as s =

λr : instrCounterRep . λself : Ref InstrCounter .

let super = se tC o u n t e r Cl a s s r self in

{ get = super . get ,

set = λi : Nat . (r. a := succ (!( r.a )); super . set i) ,

inc = super .inc ,

acc esses = λ_: Unit . !( r.a )};

Ошибка: несоответствие типа параметра

Выйти из этого затруднения можно, заменив конструктор Ref в типе self на Source — т. е., пере-

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

В сущности, это та же идея, что мы использовали в решении Упражнения 13.5.8. Я благодарен Джеймсу Рили за

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

rev. 104

194 18.13. Резюме

(оно классу все равно не нужно). Как мы видели в §15.5.6, конструктор Source разрешает ковариант-

ное наследование — т. е., выполняется Source InstrCounter <: Source SetCounter, так что создание

super в instrCounterClass будет правильно типизировано.

setCounterClas s =

λr : Co u n t erRep . λself : So urce SetC o u n t er .

{ get = λ_: Unit . !( r.x ) ,

set = λi : Nat . r.x :=i ,

inc = λ_ : Unit . (! self ). set ( succ ((! self ). get unit ))};

setCounterClas s : CounterRep -> ( Source SetCo u n t e r ) -> S e t C ounter

instrCoun t e r C l as s =

λr : instrCounterRep . λself : Source InstrCounter .

let super = se tC o u n t e r Cl a s s r self in

{ get = super . get ,

set = λi : Nat . (r. a := succ (!( r.a )); super . set i) ,

inc = super . inc ,

acc esses = λ_: Unit . !( r.a )};

instrCoun t e r C l as s : I n s t rC o u n t e r R ep ->

( So urce InstrCounter ) -> InstrCounter

Чтобы построить объект-счетчик с подсчетом доступа, мы сначала, как и раньше, определяем

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

dummyInst r C o u n te r =

{ get = λ_: Unit . 0,

set = λi : Nat . unit ,

inc = λ_ : Unit . unit };

dummyInst r C o u n te r : I n s t r C o u n t e r

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

instrCounterClass, чтобы создать настоящие методы, и заменяем значение в ссылочной ячейке.

newInstrCounte r =

λ_ : Unit .

let r = {x = ref 1, a= ref 0} in

let cAux = ref dummyInstrC o u n t er in

( cAux := ( i n s t rC o u n te r C l as s r cAux ); ! cAux );

newInstrCounte r : Unit -> In s t r C o u n t e r

Код для построения таблицы методов (в instrCounterClass и в setCounterClass) теперь зовется

один раз при создании объекта, а не при каждом вызове метода. Таким образом, мы добиваемся своей

цели, однако, по-прежнему, не столь эффективно, как нам хотелось бы: в конце концов, таблица мето-

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

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

гать. В Главе 27 мы увидим, как добиться этого при помощи ограниченной квантификации, вводимой

в Главе 26.

18.13. Резюме

В первом разделе этой главы были перечислены несколько характеристик объектно-

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

с примерами, разработанными в этой главе.

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

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

rev. 104

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

ссылочной ячейки в §18.2 до записи, содержащей несколько ссылок, в §18.9. Каждый объект

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

типа Counter (и, возможно, каких-то еще), соответствующей внутреннему представлению этого

объекта.

2. Инкапсуляция. То, что переменные экземпляра каждого объекта доступны только изнутри его

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

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

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

3. Наследование. В нашей реализации наследование между типами объектов — это просто обык-

новенное наследование между типами записей, состоящих из функций.

4. Наследование реализаций. Мы моделировали наследование реализаций через копирование

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

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

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

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

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

с теми же самыми переменными.

5. Открытая рекурсия. Открытая рекурсия, предоставляемая в настоящих объектно-

ориентированных языках через переменную self (или this), моделируется нами через аб-

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

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

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

Упражнение 18.13.1 : Еще одно свойство объектов, часто оказывающееся полезным, — поня-

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

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

ты, созданные в разное время (различными вызовами функций new). Как можно расширить модель

объектов из этой главы, чтобы поддержать тождество объектов?

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

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

щества специалистов по языкам программирования. Одно из первый решений было дано Рейнольдсом

(Reynolds 1978); всеобщий интерес к этой задаче пробудила статья Карделли (Cardelli 1984). Понятие

о self как о неподвижной точке было разработано Куком (Cook 1989), Куком и Палсбергом (Cook

and Palsberg 1898), Камином (Kamin 1988) и Редди (Reddy 1988); соотношения между этими моделями

исследовались Камином и Редди (Kamin and Reddy 1994) и Брюсом (Bruce 1991).

Некоторые важные ранние работы в этой области собраны в книге (Gunter and Mitchell 1994). Обзор

более поздних достижений можно найти у Брюса, Карделли и Пирса (Bruce, Cardelli and Pierce 1999),

а также у Абади и Карделли (Abadi and Cardelli 1996). Брюс (Bruce 2002) дает современную картину

исследований в этой области. Альтернативные подходы к основам объектов и их систем типов можно

найти у Палсберга и Шварцбаха (Palsberg and Schwartzbach 1994) и у Кастаньи (Castagna 1997).

Дополнительные исторические замечания можно найти в конце Главы 32.

Наследованию придается

слишком большое значение.

Гради Буч

rev. 104

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

rev. 104

Глава 19

Расширенный пример: Облегченная

Java

В Главе 18 мы видели, как при помощи лямбда-исчисления с наследованием, записями и ссылками

можно смоделировать некоторые ключевые конструкции объектно-ориентированного программирова-

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

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

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

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

19.1. Введение

Формальное моделирование может оказать большую помощь в проектировании сложных искус-

ственных объектов вроде языков программирования. С помощью формальной модели можно точно

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

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

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

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

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

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

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

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

механизмы.

Облегченная Java (Featherweight Java, FJ) была предложена в статье Игараси, Пирса и Уодлера

(Igarashi, Pierce and Wadler 1999) в качестве одного из вариантов минимального ядра, на основе ко-

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

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

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

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

отбросить как можно больше конструкций, — даже присваивание, — но сохранить основные четры ти-

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

том смысле, что всякая программа на FJ является буквально еще и программой на Java.

FJ лишь ненамного превышает по размеру лямбда-исчисление или объектное исчисление Абади и

Карделли (Abadi and Cardelli 1996), и намного меньше, чем другие формальные модели языков, по-

добно Java, основанных на классах, включая модели Дроссопулу, Айзенбаха и Хуршида (Drossopoulou,

Eisenbach and Khurshid 1999), Сайма (Syme 1997), Нипкова и Охаймба (Nipkow and Oheimb 1998), а

Примеры в этой главе являются термами Облегченной Java (Рис. 19.1–19.4). Соответствующей реализации на OCaml

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

годится для выполнения примеров.

197

198 19.2. Обзор

также Флатта, Кришнамурти и Феллейсена (Flatt, Krishnamurthi and Felleisen 1998a, 1998b). Посколь-

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

Например, как мы увидим, описать поведение конструкции приведения типа в Java труднее, чем можно

было предположить.

Основное применение FJ — моделирование расширений Java. Поскольку сама FJ очень мала, мож-

но уделить все внимание ключевым аспектам конкретного расширения. Более того, поскольку дока-

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

для довольно большого расширения. Первая же статья о FJ продемонстрировала это свойство, доба-

вив в FJ обобщенные классы и методы по образцу GJ (Bracha, Odersky, Stoutamire and Wadler 1998).

Следующая статья (Iagarashi, Pierce and Wadler 2001) построила формальное описание сырых типов,

введенных в GJ, чтобы облегчить перевод Java-программ на GJ. Игараси и Пирс (Igarashi and Pierce

2000) воспользовались FJ как основой для изучения свойств внутренних классов в Java. Уроме того,

FJ использовалась для изучения компиляции с сохранением типов (League, Trifonov and Shao 2001), а

также семантических оснований Java (Studer 2001).

Целью разработки FJ было как можно сильнее упростить и сократить доказательство типовой без-

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

Java. Всякая конструкция, которая удлинняла доказательство, не делая его существенно другим, под-

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

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

конструкции Java: присваивание, интерфейсы, перегрузка функций, посылка сообщений переменной

super, нулевые указатели, базовые типы (int, bool), объявления абстрактных методов, внутренние

классы, замещение полей надкласса полями подкласса, контроль доступа (public, private, и т. д.), а

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

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

между методами с использованием this, наследование и приведение типов.

Главное упрощение, принятое в FJ — отсутствие присваивания. Мы предполагаем, что значения всех

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

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

перечислений, представить невозможно. Тем не менее, этот фрагмент вычислительно полон (несложно

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

например, многие программы из книги Феллейсена и Фридмана о Java (Felleisen abd Friedman 1998)

написаны в чисто функциональном стиле.

19.2. Обзор

Программа на FJ состоит из набора определений классов и терма, подлежащего вычислению —

последний соответствует телу метода main в Java. Вот несколько типичных определений классов на FJ.

class A exte nds Obj ect { A () { super (); } }

class B exte nds Obj ect { B () { super (); } }

class Pair extends Ob ject {

Ob ject fst ;

Ob ject snd ;

// Конструктор:

Pair ( Object fst , Object snd ) {

super (); this . fst = fst ; this . snd = snd ; }

// Определение метода:

Pair setfst ( Object newfst ) {

re turn new Pair ( newfst , this . snd ); } }

Ради синтаксической регулярности мы всегда указываем надкласс (даже если это Object), всегда

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

при доступе к полю или вызове метода (скажем, this.snd), даже если это this. Конструкторы всегда

имеют одну и ту же стилизованную форму: имеется по одному параметру на каждое поле, с тем же

rev. 104

19.2. Обзор 199

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

оставшиеся поля инициализируются значениями соответствующих параметров. В нашем примере над-

классом всех приведенных классов служит Object, где никаких полей нет, так что вызовы super не

имеют аргументов. Конструкторы — единственное место, где в программах на FJ встречаются super

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

return с параметром-телом, как можно видеть на примере setfst.

В FJ есть пять видеов термов. В нашем примере new A(), new B() и new Pair(...) — конструкторы

объектов, а ....setfst(...) — вызов метода. В теле setfst, терм this.snd является обращением к

полю, а вхождения newfst и this — переменные.

В контексте приведенных опеределений, терм

new Pair ( new A() , new B ()). setfs t ( new B ())

дает при вычислении new pair(new B(), new B()).

Оставшийся пятый вид термов – приведение типа (см. 15.5.1). Терм

(( Pair ) new Pair ( new Pair ( new A () , new B ()) ,

new A ()). fst ). snd

дает при вычислении new B(). Подтерм (Pair)t, где t равняется new Pair(...).fst, является приведе-

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

что он содержит объект типа Object, в то время как следующее обращение к полю snd определено

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

объект класса Object, хранимый в поле fst, классу Pair (в данном случае проверка будет успешной).

Отказ от побочных эффектов приводит к приятному побочному эффекту: вычисление можно цели-

ком формализовать в рамках синтаксиса FJ, не обращаясь к дополнительным механизмам для модели-

рования кучи (см. Главу 13). Имеется три основных правила вычисления: одно для обращения к полю,

одно для вызова метода и одно для приведения типа. Напомним, что в лямбда-исчислении правило

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

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

new. В лямбда-исчислении действует лозунг «все на свете функции», здесь «все на свете объекты».

Следующий пример показывает правило для обращения к полям (E-ProjNew) в действии:

new Pair(new A(), new B()).snd new B()

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

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

Здесь это поля fst и snd, и обращение к полю snd выбирает второй параметр.

Вот как действует правило для вызовов метода (E-InvkNew):

new Pair (new A(), new B()).setfst(new B())

newfst new B()

this new Pair(new A(),new B())

new Pair(newfst, this.snd)

т. е., new Pair(new B(), new Pair(new A(), new B()).snd)

Получаетелем при вызове метода является объект new Pair(new A(),new B()), так что мы ищем ме-

тод setfst в классе Pair, и видим, что этот метод имеет формальный параметр newfst и тело new

Pair(newfst, this.snd). Вызов метода сводится к телу, в котором формальный параметр заменяется

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

редукции (E-AppAbs) в лямбда-исчислении. Основные отличия том, что класс получателя определяет,

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

замена переменной this на получатель (при этом поддерживается «открытая рекурсия через self»).

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

В отличие от Java, в синтаксисе FJ this считается переменной, а не ключевым словом

Читатели, знакомые с исчислением объектов Абади и Карделли (Abadi and Cardelli 1996), увидят много общего и их

правилом ς-редукции.

rev. 104

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

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

это различие со стандартной семантикой Java невозможно обнаружить.

Вот правило для приведения типов (E-CastNew) в действии:

(Pair)new Pair(new A(), new B()) new Pair(new A(), new B())

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

является подклассом класса-цели приведения. Если этот так (как в нашем случае), правило редукции

убирает приведение. Если нет, как в терме (A)new B(), никакое правило не применимо, и вычисление

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

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

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

(«непонятное сообщение»), либо при попытке привести объект к чему-то иному, чем надкласс текущего

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

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

приведения вниз (а также без «глупых приведений» — этот технический термин разъясняется ниже).

Мы принимаем стандартную стратегию вычисления с вызовом по значению. Вот шаги вычисления

второго приведенного нами терма-примера. Подлежащий редукции подтерм на каждом шаге подчер-

кивается.

((Pair) (new Pair(new Pair(new A(),new B()), new A()).fst.snd

((Pair)new Pair(new A(),new B())).snd

new Pair(new A(),new B()).snd

new B()

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

Прежде, чем перейти к формальному определению FJ, следует исследовать одно существенное сти-

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

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

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

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

улучшить читаемость примеров, например:

Na tPair = { fst : Nat , snd : Nat };

Роль этих определений чисто косметическая: имя NatPair служит простым сокращением для

{fst:Nat,snd:Nat}, и два этих выражения взаимозаменимы в любом контексте. Наши формальные

описания различных исчислений игнорируют сокращения.

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

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

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

через имя. «Голые» типы вроде {fst:Nat,snd:nat} просто не могут оказаться в этих синтаксических

позициях.

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

новое имя (в определении класса или интерфейса), программист должен явно объявить, какие классы и

интерфейсы расширяет новый тип (или, в случае нового класса и уже существующего интерфейса, «ре-

ализует»). Компилятор проверяет эти объявления и убеждается, что возможности, предоставляемые

новым классом или интерфейсом, действительно расширяют имеющиеся в каждом надклассе и над-

интерфейсе — эта проверка соответствует наследованию записей в типизированном лямбда-исчислении.

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

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

оно им и не является.

Системы типов, подобные системе Java, где имена типов существенны и наследование определя-

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

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

структурными.

rev. 104