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

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

32.5. Отправка сообщений объектам 371

32.5. Отправка сообщений объектам

Теперь можно исправить сломанную версию sendinc из §32.3, проведя абстракцию по подинтер-

фейсам вместо подтипов Counter.

se ndinc =

λM <: Coun terM . λc : O bject M .

let {X , b } = c in

{*X ,

{ state = b. methods . inc (b. state ),

me thods = b . methods }}

as Obje ct M;

se ndinc : M <: Cou nterM . Object M -> O bject M

С интуитивной точки зрения, тип sendinc можно прочитать так: «дайте мне интерфейс объекта, рас-

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

с таким же интерфейсом».

Упражнение 32.5.1 : Почему эта версия sendinc правильно типизирована, в то время как преды-

дущая таковой не являлась?

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

лиморфные функции вызова методов соответствующей сигнатурой интерфейса, CounterM либо

ResetCounterM (мы предполагаем, что sendget и sendreset определены аналогичным образом).

se ndget [ Cou nterM ] ( send inc [ Count e rM ]) c ;

6 : Nat

se ndget [ ResetCounterM ]

( sendre s e t [ R e s e t C o u n t e r M ]

( sen dinc [ ResetCounterM ] rc ));

0 : Nat

Упражнение 32.5.2 Рекомендуется, : Определите sendget и sendreset.

32.6. Простые классы

Рассмотрим теперь классы, начиная (как мы делали и в Главе 18) c простых классов без self.

В §18.6 мы определили простой класс (для императивного кодирования объектов, где объекты пред-

ставляли собой записи из методов) как функцию, переводящую состояния в объекты — способ порож-

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

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

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

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

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

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

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

рассматривать как простую запись из методов,

counterClass =

{ get = λr: Counter R . r.x ,

inc = λr : Cou n terR . {x = succ (r . x )}}

as { get : CounterR - > Nat , inc : CounterR -> CounterR };

counterClass : { get : CounterR - > Nat , inc : CounterR -> CounterR }

rev. 104

372 32.7. Полиморфные обновления

или, с использованием оператора CounterM для сокращения аннотации,

counterClass =

{ get = λr: Counter R . r.x ,

inc = λr : Cou n terR . {x = succ (r . x )}}

as CounterM C o unterR ;

counterClass : CounterM Cou nterR

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

состояние с методами (т. е., с классом) в объект.

c = {* CounterR ,

{ state = {x =0} ,

me thods = co u n t e r C l a s s }}

as Counter ;

c : Counte r

Определение подкласса представляет собой просто построение новой записи с методами; при этом

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

resetCoun t e r C l as s =

let super = co u n t e r C l a s s in

{ get = super . get ,

inc = super . inc ,

reset = λr : Cou n terR . {x =0}}

as R e s e t C o u n t e r M Cou nterR ;

resetCoun t e r C l as s : R e s e t C o u n t e r M Cou nterR

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

как в конце Главы 18, нужны еще две вещи: способность добавлять в подклассах новые переменные

экземпляра и обработка self. В следующих двух разделах мы справляемся с первой из этих задач; в

§32.9 решается вопрос работы с self.

32.7. Полиморфные обновления

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

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

записи, и соответствующее уточнение типов записей. Нужда в этих новшествах возникает оттого, что,

позволяя изменение числа переменных экземпляра между классами, мы делаем надклассы полиморф-

ными по отношению к переменным экземпляра их подклассов. Посмотрим, как это происходит.

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

сохраняющий текущее значение счетчика, и заставив метод reset возвращаться к этому сохраненному

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

нам нужно расширить тип представления с {x:Nat} до {x:Nat, old:Nat}. Такая разница представле-

ний немедленно создает техническую сложность. Наша способность использовать метод inc от клас-

са resetCounterClass при определении backupCounterClass зависит от способности кода вести себя

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

различным: inc в типе ResetCounter ожидает состояние типа {x:Nat} и возвращает новое состояние

того же типа, в то время как inc в типе BackupCounter ожидает и порождает состояния типа {x:Nat,

old:Nat}.

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

деле, знать, что тип состояния равен {x:Nat} либо {x:Nat, old:Nat}; надо только знать, что состояние

содержит переменную x. Другими словами, можно унифицировать оба этих метода, если дать им тип

S<:{x:Nat}.S S.

Теперь с полями возникает та же самая проблема, что и с целыми объектами в §32.3: в нашем

теперешнем языке тип S<:{x:Nat}.S S населен только функцией тождества. Чтобы бороться с этим,

rev. 104

32.7. Полиморфные обновления 373

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

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

Если

r является записью с полем x типа T, а t — терм типа T, то запись r x=t будет означать «запись,

совпадающая с r, за исключением поля x, значение которого равно t». Заметим, что такая операция

обновления вполне функциональна — она не изменяет r, а создает клонированную запись с другим

значением поля x.

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

жающую ожидаемое поведение тела метода inc:

f = λX <:{ a : Nat }. λx: X . r a = succ ( r . a);

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

бы такое:

Γ r : R Γ R <: {l

} Γ t :T

Γ r l

=t : R

Но это правило некорректно. Например, дупоустим, у нас есть

s = { x={ a =5 , b =6} , y= true };

Поскольку s : {x:{a:Nat,b:Nat},y:Bool}, и при этом {x:{a:Nat,b:Nat},y:Bool} <: {{a:Nat}}, вы-

шеприведенное правило позволило бы нам написать

s x ={ a =8} : {x :{ a: Nat ,b : Nat },y : Bool }

что было бы неверно, поскольку s x={a=8} редуцируется до {x={a=8},y=true}.

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

{x:{a:Nat,b:Nat},y:Bool} <: {x:{a:Nat}}. Наследование в глубину требуется запретить для полей,

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

метить поля особым знаком #.

Правила для таких «обновляемых записей» и для самой операции обновления приведены на

Рис. 32.1. Мы усложняем синтаксис типов записей, так что каждое поле оказывается снабжено меткой

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

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

ченные записи будут вести себя так же, как раньше). Правило наследования в глубину S-RcdDepth

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

правило наследования S-RcdVariance, позволяющее изменять отметки полей с # на пустую строку —

иными словами, «забывать», что какое-то поле может обновляться. Правило типизации для операции

обновления требует, чтобы заменяемое поле было помечено знаком #. Правило E-Update реализует

операцию обновления.

Теперь функция f, обсуждавшаяся выше, пишется так:

f = λX <:{# a : Nat }. λr : X. r a = succ ( r .a );

f : X <{# a: Nat }. X -> X

и используется так:

r = {# a=0 , b= true };

f [{# a: Nat ,b: Bool }] r;

{# a=1 , b= true } : {#a : Nat , b: Bool }

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

ного отношения наследования:

Утверждение 32.7.1 Если R <: {#l:T

}, то R {...#l:R

. . .}, причем R

<: T

и T

<: R

Упражнение 32.7.2 Рекомендуется, : Соблюдается ли в этом исчислении свойство мини-

мальной типизации? Если да, докажите. Если нет, покажите, как исправить ситуацию.

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

них перечислены в разделе §32.10) или используя полиморфизм как в (Pierce and Turner 1994) — альтернатива более тяже-

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

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

rev. 104

374 32.8. Добавление переменных экземпляра

<: Top {} Основано на F

(26.1) с записями (11.7)

Новые синтаксические формы

t ::= . . . термы:

{ ι

i 1..n

} запись

t l=t обновление поля

T ::= . . . типы:

{ ι

i 1..n

} тип записей

ι ::= # инвариантное (обновляемое) поле

пропущено ковариантное (фиксированное) поле

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

{ι

j 1..n

} l

=v {ι

j 1..i 1

, ι

=v, ι

k i 1..n

} (E-UpdateV)

{

i 1..n

}.l

(E-ProjRcd)

{ ι

i 1..j 1

, ι

k j 1..n

} { ι

i j 1

, ι

k j 1..n

}

(E-Rcd)

Новые правила наследования Γ S <: T

Γ { ι

i 1..n k

} <: { ι

i 1..n

} (S-RcdWidth)

для каждого i, Γ S

<: T

если ι

#, то Γ T

<: S

Γ { ι

i 1..n

} <: { ι

i 1..n

}

(S-RcdDepth)

Γ {...#l

...} <: {...l

...} (S-RcdVariance)

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

для каждого i, Γ t

: T

Γ { ι

i 1..n

} : { ι

i 1..n

}

(T-Rcd)

Γ t

: { ι

i 1..n

}

Γ t

: T

(T-Proj)

Γ r : R Γ R <: {#l

} Γ t : T

Γ r l

=t : R

(T-Update)

Рис. 32.1. Полиморфное обновление

32.8. Добавление переменных экземпляра

При помощи конструкций из предыдущего раздела мы можем написать counterClass, полиморф-

ный по отношению к типу своего внутреннего состояния.

Cou nterR = {# x: Nat };

counterClass =

λR <: Coun terR .

{ get = λs: R . s .x ,

inc = λs : R. s x = succ (s . x)}

as CounterM R ;

counterClass : R <: Cou n terR . Count erM R

Чтобы построить объект нашего нового класса counterClass, мы просто задаем CounterR в качестве

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

c = {* CounterR ,

{ state = {# x =0} ,

me thods = co u n t e r C l a s s [ C o unterR ]}}

as Obje ct Counte rM ;

c : Counte r

Заметим, что объекты, построенные с помощью нового класса, имеют тот же самый тип Counter

Object CounterM, что и построенные нами ранее: изменения в обращении с переменными состояния

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

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

В том же стиле мы можем написать и resetCounterClass.

resetCoun t e r C l as s =

λR <: Coun terR .

rev. 104

32.9. Классы с переменной SELF 375

let super = co u n t e r C l a s s [ R] in

{ get = super . get ,

inc = super .inc ,

reset = λs : R. s x =0}

as R e s e t C o u n t e r M R ;

resetCoun t e r C l as s : R <: C o unterR . ResetCounterM R

Наконец, теперь мы можем написать backupCounterClass, на этот раз абстрагируясь по подтипам

BackupCounterR (это и было смыслом всего нашего упражнения).

backupCounterM = λR . { get :R -> Nat , inc :R ->R , reset :R ->R , backup :R ->R };

backupCounterR = {# x :Nat ,# old : Nat };

backupCo u n t e rC l a s s =

λR <: BackupCounte r R .

let super = resetCounter C l a s s [ R] in

{ get = super . get ,

inc = super .inc ,

reset = λs : R. s x = s. old ,

ba ckup = λs:R. s old =s.x }

as B a c k u p C ou n t e r M R ;

backupCo u n t e rC l a s s : R <: B a c k u pC o u n t e r R . BackupCounterM R ;

32.9. Классы с переменной self

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

методам класса рекурсивно ссылаться друг на друга. Это расширение имеет смысл и в чисто функци-

ональном окружении.

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

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

counterClass =

λR <: Coun terR .

λself : Unit - > Co u nterM R.

λ_ : Unit .

{ get = λs: R . s .x ,

inc = λs : R. s x = succ (s . x)}

as CounterM R ;

Как и в §18.9, с помощью аргумента Unit мы откладываем вычисление во время операции fix, созда-

ющее методы объекта. Тип self включает соответствующую абстракцию по Unit.

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

counterClass и применяем ее к unit.

c = {* CounterR ,

{ state = {# x =0} ,

me thods = fix ( counterClass [ Cou n terR ]) unit }}

as Obje ct Counte rM ;

c : Counte r

Теперь мы определяем подкласс с операцией set, обладающий следующим интерфейсом:

SetCoun t e r M = λR . { get : R -> Nat , set :R -> Nat - >R inc :R - >R };

Реалиация setCounterClass определяет метод set и использует методы set и get из self при реали-

зации своего метода inc:

setCounterClas s =

λR <: Coun terR .

λself : Unit -> SetCOunterM R.

λ_ : Unit .

rev. 104

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

let super = co u n t e r C l a s s [ R] self unit in

{ get = super . get ,

set = λs : R. λn: Nat . s x =n ,

inc = λs : R. ( self unit ). set s ( succ (( self unit ). get s ))}

as S e t CounterM R;

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

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

InstrCounterM =

λR . { get : R -> Nat , set :R -> Nat - >R , inc :R ->R , a ccesses :R -> Nat };

InstrCounterR = {# x: Nat ,# count : Nat };

instrCoun t e r C l as s =

λR <: InstrCounterR .

λself : Unit - > InstrCounterM R.

λ_ : Unit .

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

{ get = super . get ,

set = λs : R. λn: Nat .

let r = super . set s n in

r count = succ (r . count ) ,

inc = super .inc ,

acc esses = λs: R . s . count }

as I n s t r C o u n t e r M R ;

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

терминах метода set переменной self.

Для проверки мы создаем объект-счетчик с отслеживанием обращений и посылаем ему несколько

сообщений.

ic = {* InstrCount erR ,

{ state = {# x =0 ,# count =0} ,

me thods = fix ( instrCou n t e r C la s s [ InstrCounterR ]) unit }}

as Obje ct InstrC o u n t e r M ;

ic : Object InstrCounterM

sendaccesses [ InstrCounterM ] ( sendin c [ I n s t r C o u n t e r M ] ic );

1 : Nat

Упражнение 32.9.1 Рекомендуется : Определите подкласс instrCounterClass, добавляющий

методы backup и reset.

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

Первая «чисто функциональная» интерпретация объектов в рамках типизированного лямбда-

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

ли (Cardelli 1984), а затем множество ее вариантов изучали Кэймин и Редди (Reddy 1988; Kamin

and Reddy 1994), Кук и Палсберг (Cook and Palsberg 1989) и Митчелл (Mitchell 1990a). Бестипо-

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

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

ных объектно-ориентированных примеров, но при систематической интерпретации типизированных

объектно-ориентированных языков она вызывает трудности. Наиболее успешным проектом в этом от-

ношении явились работы Кука и его соавторов (Cook, Hill and Canning 1990; Canning, Cook, Hill and

Olthoﬀ 1989a; Canning, Cook, Hill, Olthoﬀ and Mitchell 1989b).

rev. 104

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

Пирс и Тёрнер (Pierce and Turner 1994) ввели кодирование, опирающееся только на систему типов

с экзистенциальными типами, без рекурсивных типов. Это привело Хофмана и Пирса (Hofmann and

Pierce 1995b) к первой единообразной управляемой типами интерпретации объектов в рамках функ-

ционального исчисления. На той же конференции Брюс представил работу (Bruce 1994) по семанти-

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

прямое отображение в денотационную модель F

, но недавно ее переформулировали как способ ко-

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

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

Карделли представили исчисление, где объекты служат примитивным элементом (Abadi and Cardelli

1996). Однако позднее Абади, Карделли и Вишванатан (Abadi, Cardelli and Viswanathan 1996) откры-

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

рекурсивных типов. Обзор этих достижений можно найти у Брюса и др. (Bruce et al. 1990), а также у

Абади и Карделли (Abadi and Cardelli 1996).

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

наследования — классов, имеющих более одного надкласса, — Компаньони и Пирсом (Compagnoni

and Pierce 1996). Основная техническая идяея состоит в том, чтобы добавить в F

типы-пересечения

(§15.7).

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

фикации второго порядка, которые мы расмотрели в §32.3. Помимо двух решений, использованных

нами в этой главе — ограниченной квантификации высших порядков и элементарной конструкции

для полиморфного обновления записей, — есть еще несколько других стилистических вариантов поли-

морфного обновления (Cardelli and Mitchell 1991; Cardelli 1992; Fisher and Mitchell 1996; Poll 1996), а

также структурное развертывание рекурсивных типов (Abadi and Cardelli 1996), позитивное насле-

дование (Hofmann and Pierce 1995a), полиморфная перепаковка экзистенциальных типов (Pierce 1996)

и деструкторы типов (Hofmann and Pierce 1998).

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

1987, 1988, 1989b), Реми (R´emy 1990, 1989, 1992), Вуйона (Vouillon 2000, 2001) и других. Он также лежит

в основе объектно-ориентированных конструкций OCaml (R´emy and Vouillon 1998).

Начни сначала, — важно

ответил Король, — и

продолжай, пока не дойдешь до

конца. Как дойдешь — кончай!

Льюис Кэрролл, пер.

Н. Демуровой

rev. 104

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

rev. 104

Приложения

379