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

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

13.5. Безопасность 131

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

отношению к которому будет вычислен терм t. Тогда с помощью Σ мы можем вычислить тип резуль-

тата t, не обращаясь прямо к µ. Например, если Σ равна l

Unit, l

Unit Unit , то мы можем

немедленно решить, что !l

имеет тип Unit Unit. В общем случае, можно переформулировать пра-

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

Σ l T

Γ Σ l : Ref T

(T-Loc)

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

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

ным образом с учетом структур типизации памяти.

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

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

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

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

до сих пор: лемма о подстановке (9.3.8) говорит нам, что, если Γ t : T, то мы можем заменить

свободные переменные t значениями типов, указанных в Γ, и получим замкнутый терм типа T, кото-

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

T (если какой-либо результат вообще получится). В §13.5 мы увидим, как формализовать подобную

интуицию для состояний памяти и структур типизации памяти.

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

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

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

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

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

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

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

щаемых в свежевыделенных ячейках; это интуитивное рассуждение будет формализовано в теореме о

сохранении типов (13.5.3).

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

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

, сама ссылка

имеет тип Ref T

Γ Σ t

: T

Γ Σ ref t

: Ref T

(T-Ref)

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

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

выделенными ячейками памяти и их типами.

Соответственно, если t

имеет значением адрес типа Ref T

, то разыменование этого терма всегда

даст значение типа T

Γ Σ t

: Ref T

Γ Σ !t

: T

(T-Deref)

Наконец, если t

обозначет ячейку типа Ref T

, то мы можем сохранить в этой ячейке t

, при

условии, что t

также имеет тип T

Γ Σ t

: Ref T

Γ Σ t

: T

Γ Σ t

:= t

: Unit

(T-Assign)

На Рис. 13.1 изображены правила типизации (а также, для справки, синтаксические правила и

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

13.5. Безопасность

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

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

rev. 104

132 13.5. Безопасность

Unit Ref Расширяет λ с типом Unit (9.1 и 11.2)

Синтаксис

t ::= термы

x переменная

λx:T.t абстракция

t t применение

unit константа unit

ref t порождение ссылки

!t разыменование

t:=t присваивание

l адрес в памяти

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

λx:T.t значение-абстракция

unit значение единичного типа

l адрес в памяти

T ::= типы:

T T тип функций

Unit единичный тип

Ref T тип ссылочных ячеек

Γ ::= контексты:

пустой контекст

Γ, x:T связывание термовой переменной

µ ::= состояния памяти:

пустое

µ, l v связывание адреса

Σ ::= структуры типизации памяти:

пустая

Σ, l:T типизация адреса

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

µ t

(E-App1)

µ t

µ v

(E-App2)

(λ x:T

) v

µ x v

(E-AppAbs)

l dom µ

ref v

µ l µ, l v

(E-RefV)

µ t

ref t

µ ref t

(E-Ref)

µ l v

!l µ v µ

(E-DerefLoc)

µ t

µ !t

(E-Deref)

l := v

µ unit l v

(E-Assign)

µ t

:= t

µ t

:= t

(E-Assign1)

µ t

:= t

µ v

:= t

(E-Assign2)

см. далее. . .

Рис. 13.1. Ссылки

(«правильно типизированные термы не находятся в тупике») можно сформулировать и доказать почти

так же, как и ранее (см. 13.5.7); требуется лишь рассмотреть в доказательстве несколько новых неслож-

ных вариантов, относящихся к новым конструкциям. Теорема о сохранении несколько интереснее, так

что давайте сначала обратимся к ней.

Поскольку мы расширили как отношение вычисления (начальным и конечным состояниями па-

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

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

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

Если Γ Σ t : T и t µ t µ , то Γ Σ t : T (Неверно!)

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

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

rev. 104

13.5. Безопасность 133

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

x : T Γ

Γ Σ x : T

(T-Var)

Γ, x:T

Σ t

: T

Γ Σ λx:T

: T

(T-Abs)

Γ Σ t

: T

Γ Σ t

: T

Γ Σ t

: T

(T-App)

Γ Σ unit : Unit (T-Unit)

Σ l T

Γ Σ l : Ref T

(T-Loc)

Γ Σ t

: T

Γ Σ ref t

: Ref T

(T-Ref)

Γ Σ t

: Ref T

Γ Σ !t

: T

(T-Deref)

Γ Σ t

: Ref T

Γ Σ t

: T

Γ Σ t

:= t

: Unit

(T-Assign)

Рис. 13.2. Ссылки (продолжение)

катастрофическим. Следующее требование выражает нужное нам ограничение:

Определение 13.5.1 Состояние памяти µ правильно типизировано относительно типового контек-

ста Γ и структуры типизации памяти Σ, что записывается Γ Σ µ, если dom µ dom Σ и

Γ Σ µ l : Σ l для каждого l dom µ .

Неформально, состояние памяти µ корректно по отношению к структуре типизации Σ, если каждое

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

Упражнение 13.5.2 : Можете ли Вы найти контекст Γ, состояние памяти µ и две различных

структуры типизации Σ

и Σ

, так, чтобы одновременно выполнялось Γ Σ

µ и Γ Σ

µ?

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

ния:

Если

Γ Σ t : T

t µ t µ

Γ Σ µ

то Γ Σ t : T. (Все еще неверно.)

Это утверждение работает для всех правил вычисления, кроме правила выделения памяти E-RefV.

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

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

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

области определения Σ, и неверно будет, что терм t (который наверняка упоминаниет l) типизируем

относительно Σ.

Ясно, что, поскольку состояние памяти в процессе вычисления может расширяться, нам нужно

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

свойства сохранения:

Теорема 13.5.3 Сохранение : Если

Γ Σ t : T

t µ t µ

Γ Σ µ

то для некоторого Σ Σ,

rev. 104

134 13.5. Безопасность

Γ Σ t : T

Γ Σ µ.

Заметим, что теорема о сохранении утверждает только, что есть какое-то состояние памяти Σ Σ

(т. е., совпадающее с Σ на всех старых адресах), такое, что новый терм t правильно типизирован

относительно Σ ; она ничего не говорит о том, как именно Σ выглядит. Неформально, разумеется,

понятно, что Σ либо совпадает с Σ, либо равняется в точности Σ, l T

, где l — свежевыделенный

адрес (новый элемент области определения µ ), а T

— тип начального значения, хранимого по адресу l

в расширенном состоянии памяти µ, l v

, однако явное внесение этих подробностей усложнило бы

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

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

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

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

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

Для доказательства сохранения нам требуется еще несколько технических лемм. Первая из них —

несложное расширение стандартной леммы о подстановке (9.3.8).

Лемма 13.5.4 Подстановка : Если Γ, x:S Σ t : T и Γ Σ s : S, то Γ Σ x s t : T.

Доказательство: В точности как в Лемме 9.3.8.

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

ствующего типа не изменяет общую структуру типизации памяти.

Лемма 13.5.5 Если

Γ Σ µ

Σ l T

Γ Σ v : T

то Γ Σ l v µ.

Доказательство: Непосредственно из определения отношения Γ Σ µ.

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

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

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

Лемма 13.5.6 Если Γ Σ t : T и Σ Σ, то Γ Σ t : T.

Доказательство: Несложная индукция.

Теперь мы можем доказать теорему о сохранении.

Доказательство 13.5.3: Несложная индукция по деревьям вывода вычисления, с использованием вы-

шеприведенных лемм и свойства обращения для правил типизации (это прямолинейное расширение

свойства 9.3.1).

Утверждение теоремы о продвижении (9.3.5) также требуется расширить, чтобы учесть состояния

памяти и структуры типизации:

Теорема 13.5.7 Продвижение : Допустим, t — замкнутый, правильно типизированный терм (то

есть, Σ t : T) для некоторых T и Σ. Тогда либо t является значением, либо для любого состо-

яния памяти µ, такого, что Σ µ, существуют терм t и состояние памяти µ , такие, что

t µ t µ .

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

казательство Теоремы 9.3.5. (Лемма о канонических формах 9.3.4 требует двух дополнительных

утверждений: что все значения типа Ref T являются адресами, и подобное утверждение для Unit.)

Упражнение 13.5.8 Рекомендуется, : Является ли отношение вычисления из этой главы

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

правильно типизированную функцию вычисления факториала в нашем текущем исчислении (расши-

ренном числами и булевскими значениями).

rev. 104

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

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

Способ представления материала, выбранный в этой главе, основан на подходе Харпера (Harper

1994, 1996). Описание в подобном же стиле дано в статье Райта и Феллейсена (Wright and Felleisen

1994).

Сочетание ссылок (или других вычислительных эффектов) с полиморфным выводом типов в стиле

ML ведет к некторым нетривиальным проблемам (см. 22.7). Этим вопросам уделялось немалое вни-

мание в теоретической литературе. См. труды Тофте (Tofte 1990), Хоанга и др. (Hoang et al. 1993),

Жувело и Гиффорда (Jouvelot and Giﬀord 1991), Талпина и Жувело (Talpin and Jouvelot 1992), Леруа

и Вайса (Leroy and Weis 1991), Райта (1992), Харпера (Harper 1994, 1996), а также процитированные

там источники.

Статическое предсказание возможного наличия псевдонимов — давно известная проблема как в

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

ния. Во влиятельнаой ранней работе Рейнольдса по этой проблеме (Reynolds 1978, 1989) введен термин

синтаксическое упроавление помехами. Его идеи недавно привели к новому всплеску активности —

см. работы О’Херна и др. (O’Hearn et al. 1995), а также Смита и др. (Smith et al. 2000). Более общие

подходы к исследованию псевдонимов описываются в работах Рейнольдса (Reynolds 1981) и Ишитака

и О’Херна (Ishitaq and O’Hearn 2001). См. также литературу, процитированную в этих работах.

Подробное обсуждение методов сборки мусора можно найти у Джонса и Линса (Jones and Lins

1996). Более семантически-ориентированный подход представлен работой Моррисета и др. (Morrisett

et al. 1995).

Найти причину этого эффекта

Или, верней, дефекта, потому

что

Дефектный сей эффект

небеспричинен.

Гамлет II, ii, 101 (перевод

М. Лозинского)

Палец, указывающий на луну —

не луна.

Буддистская пословица

rev. 104

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

rev. 104

Глава 14

Исключения

В Главе 13 мы увидели, как моожно расширить операционную семантику простого типизированного

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

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

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

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

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

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

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

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

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

риант (или опцию), как мы видели в $11.10. Но если исключительная ситуация действительно исклю-

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

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

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

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

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

ваем этот последний вариант (§14.1), когда всякое исключение немедленно останавливает программу,

затем добавляем механизм для перехвата и обработки исключений (§14.2), и, наконец, улучшаем оба

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

точкой возникновения исключения и обработчиком (§14.3).

14.1. Порождение исключений

Для начала мы добавляем в лямбда-исчисление простейший из возможных механизмов для опове-

щения об исключениях: терм error («ошибка»), который, будучи исполнен, прекращает вычисление

терма, где он содержится. Необходимые дополнения изображены на Рис. 14.1.

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

мализовать в нашей операционной семантике «ненормальное завершение». Мы принимаем простей-

шее решение: результатом оборвавшейся программы служит сам терм error. Правила E-AppErr1 и

E-AppErr2 реализуют это поведение. E-AppErr1 говорит, что, если мы встречаем терм error при

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

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

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

применение и немедленно вернуть error.

Обратите внимание, что мы не включили error в список значений — только в список термов. Это

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

Системы, изучаемые в этой главе — простое типизированное лямбда-исчисление (Рис. 9.1), расширенное различными

примитивами для порождения и обработки исключений (Рис. 14.1 и 14.2). Реализация первого из этих расширений на

OCaml называется fullerror. Язык, где исключения сопровождаются значениями (Рис. 14.3), не реализован.

137

138 14.1. Порождение исключений

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

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

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

error ошибка

времени исполнения

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

error t

error (E-AppErr1)

error error (E-AppErr2)

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

Γ error : T (T-Error)

Рис. 14.1. Ошибки

E-AppErr2 — т. е., не будет неоднозначности по поводу того, следует ли вычислить терм

(λx : Nat .0) error

как применение (и вернуть в результате 0) или прерваться: возможен только второй из этих вариантов.

Подобным образом, то, что в E-AppErr2 мы использовали метапеременную v

(а не t

, имеющую

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

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

образом, терм вроде

( fix (λx : Nat .x )) error

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

ется детерминистским.

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

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

(λx : Bool .x ) error

он имеет тип Bool. В

(λx : Bool .x ) ( error true )

он имеет тип Bool Bool.

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

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

тип (Теорема 9.3.3). С этим можно справиться различными методами. В языке с наследованием мы

можем дать терму error минимальный тип Bot (см. $15.4), который при необходимости повышается

до любого типа. В языке с параметрическим полиморфизмом (см. Главу 23) терму error можно дать

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

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

Упражнение 14.1.1 : Не проще ли было бы просто просить программиста помечать error его

предполагаемым типом при каждом использовании?

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

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

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

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

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

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

переформулировать с учетом этого.

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

нормальной форме. Тогда либо t — значение, либо t = error.

rev. 104

14.2. Обработка исключений 139

error try Расширяет λ с ошибками (14.1)

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

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

try t with t ловля ошибок

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

try v

with t

(E-TryV)

try error with t

(E-TryError)

try t

with t

try t

with t

(E-Try)

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

Γ t

: T Γ t

: T

Γ try t

with t

: T

(T-Try)

Рис. 14.2. Обработка ошибок

14.2. Обработка исключений

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

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

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

ит из множества записей активации, по одной на каждый активный вызов функции; когда возникает

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

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

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

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

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

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

на стеке вызовов).

Наша формулировка обработчиков исключений, приведенная на Рис. 14.2, похожа как на ML, так

и на Java. Выражение try t

with t

означает «вернуть результат вычисления t

, если при этом не

возникнет ошибка; иначе выполнить обработчик t

». Правило вычисления E-TryV говорит, что, когда

терм t

свелся к значению v

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

не понадобится. С другой стороны, E-TryError говорит, что, если при вычислении t

получилась

ошибка error, то нам следует заменить конструкцию try термом t

и продолжить его вычисление. E-

Try говорит, что, до тех пор, пока t

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

его вычислять, не трогая t

Правило типизации для try прямо следует из его операционной семантики. Результатом всей кон-

струкции try может быть либо результат главного тела t

, либо результат обработчика t

; нужно

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

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

нению с предыдущим разделом.

14.3. Исключения, сопровождаемые значениями

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

грамме, что «случилось нечто необычное». Как правило, полезно бывает отсылать также некоторую

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

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

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

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

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

exn

. Пока

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

rev. 104

140 14.3. Исключения, сопровождаемые значениями

исключения Расширяет λ (9.1)

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

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

raise t порождение исключений

try t with t обработка исключений

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

(raise v

) t

raise v

(E-AppRaise1)

(raise v

) raise v

(E-AppRaise2)

raise t

(E-Raise)

raise (raise v

) raise v

(E-RaiseRaise)

try v

with t

(E-TryV)

try raise v

with t

(E-TryRaise)

try t

with t

try t

with t

(E-Try)

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

Γ t

: T

exn

Γ raise t

: T

(T-Exn)

Γ t

: T Γ t

: T

exn

Γ try t

with t

: T

(T-Try)

Рис. 14.3. Исключения, сопровождаемые значениями

Атомарный терм error заменяется конструктуором терма raise t, где t — дпополнительная ин-

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

прежним, но обработчик t

в try t

with t

теперь интерпретируется как функция, принимающая до-

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

Правило вычисления E-TryRaise релизует нужное нам поведение, принимая дополнительную ин-

формацию, сопровождающую raise, из тела t

, и передавая ее обработчику t

. Правила E-AppRaise1

и E-AppRaise2 проносят исключения через применения, в точности как E-AppErr1 и E-AppErr2 на

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

где дополнительная информация является значением; если мы попробуем вычислить raise с допол-

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

нам придется вычислять дополнительную информацию при помощи E-Raise. Правило E-RaiseRaise

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

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

отбросить try, если его основное тело уже свелось к значению, так же, как мы это делали в §14.2.

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

либо raise.

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

бы дополнительная информация имела тип T

exn

; все выражение raise целиком получает любой тип

T, какого требует контекст. В правиле T-Try мы проверяем, что обработчик t

является функцией,

которая, получая дополнителную информацию типа T

exn

, выдает результат того же типа, что и t

Теперь, наконец, давайте рассмотрим возможные альтернативы для типа T

exn

1. Можно принять в качестве T

exn

просто тип Nat. Это соответствует соглашению errno, используе-

мому, например, в функциях операционной системы Unix: каждый системный вызов возвращает

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

ошибочных ситуациях.

2. Можно принять в качестве T

exn

тип String. При этом не нужно искать номера ошибок в таблицах,

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

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

придется разбирать эти строки, чтобы понять, что произошло.

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

rev. 104