Пирс Б. Типы в языках программирования
Подождите немного. Документ загружается.
Типы в языках программирования
Бенджамин Пирс
8 ноября 2009 г.
2
rev. 104
Предисловие
Исследование систем типов, а также языков программирования с точки зрения теории типов, в
последнее время превратилось в энергично развивающуюся научную дисциплину, имеющую важные
приложения в проектировании программ, дизайне языков программирования, реализации высокопро-
изводительных компиляторов и в области безопасности. Настоящий текст представляет собой подробное
введение в основные понятия, достижения и методы этой дисциплины.
Предполагаемая аудитория
Книга предназначена для двух основных групп читателей: с одной стороны, для аспирантов и иссле-
дователей, специализирующихся на языках программирования и теории типов; с другой стороны, для
аспирантов и продвинутых студентов из других областей информатики, которые хотели бы получить
введение в основные понятия теории языков программирования. Для первой из этих групп книга дает
обширный обзор рассматриваемой области, с глубиной, достаточной для чтения исследовательской ли-
тературы. Для второй она предоставляет подробный вводный материал и обширное собрание примеров,
упражнений и практических ситуаций. Книга может служить как для вводных курсов аспирантского
уровня, так и для более продвинутых семинаров по языкам программирования.
Цели
Основной моей задачей был охват материала, включая базовую операционную семантику и связан-
ные с ней способы построения доказательств, бестиповое лямбда-исчисление, простые системы типов,
универсальный и экзистенциональный полиморфизм, реконструкцию типов, иерархии типов, ограни-
ченную квантификацию, рекурсивные типы и операторы над типами, а также краткое обсуждение
некоторых других тем.
Второй задачей был прагматизм. Книга сосредоточена на использовании систем типов в языках
программирования, за счет некоторых тем (например, денотационной семантики), которые, вероят-
но, были бы включены в более математически ориентированный текст по типизированным лямбда-
исчислениям. В качестве базового вычислительного формализма выбрано лямбда-исчисление с вызо-
вом по значению, которое соответствует большинству современных языков программирования и легко
расширяется императивными конструкциями вроде ссылок и исключений. При рассмотрении каждо-
го языкового элемента основными вопросами являются: практическая мотивация для введения этого
элемента; методы доказательства безопасности языков, включающих его; а также трудности, с кото-
рыми приходится сталкиваться при его реализации — в особенности, построение и анализ алгоритмов
проверки типов.
Также задачей было уважение к разнообразию в рассматриваемой дисциплине; книга охватывает
множество отдельных тем и несколько хорошо исследованных их сочетаний, но при этом не предпри-
нимается попытки собрать все в единую целостную систему. Существуют единые подходы к некоторым
подмножествам набора тем — например, многие разновидности “стрелочных типов” можно компактно
и изящно описать в единой нотации чистых систем типов, — но дисциплина в целом пока что растет
слишком быстро, чтобы можно было систематизировать ее целиком.
Книга построена так, чтобы облегчить ее использование, как в рамках университетских курсов, так
и при самостоятельном изучении. Для большинства упражнений прилагаются полные решения. Базо-
вые определения организованы в самодостаточные таблицы, чтобы их легко было найти. Зависимости
3
4
между понятиями и системами по возможности явно указываются. К тексту прилагается обширная
библиография и индекс.
Последним организующим принципом при написании книги была честность. Все обсуждаемые в
книге системы (кроме некоторых, лишь упомянутых мельком) реализованы. Для каждой главы суще-
ствует программа проверки типов и интерпретатор, и все примеры механически проверены с их по-
мощью. Эти программы доступны на веб-сайте книги, их можно использовать при программировании
упражнений, для экспериментов по дальнейшему расширению и в учебных проектах.
Для того, чтобы достичь поставленных целей, пришлось отказаться от желания придать книге
некоторые желательные свойства. Наиболее важное из них — полнота рассмотрения. Полный обзор
дисциплины языков программирования и систем типов, вероятно, невозможен в рамках одного текста
– уж точно не в рамках учебника. Я сосредоточился на тщательном рассмотрении базовых понятий;
многочисленные отсылки на научную литературу служат как отправные точки для дальнейшего иссле-
дования. Также не была целью практическая эффективность алгоритмов проверки типов: эта книга
не является пособием по реализации компиляторов промышленного качества.
Структура книги
В Части I обсуждаются бестиповые системы. Основные понятия абстрактного синтаксиса, индук-
тивные определения и доказательства, правила вывода и операционная семантика сначала вводятся в
контексте чрезвычайно простого языка для работы с числами и логическими значениями, затем по-
вторяются для бестипового лямбда-исчисления. В Части II рассматривается простое типизированное
лямбда-исчисление, а также набор базовых языковых конструкций: произведение, сумма, записи, вари-
анты, ссылки и исключения. Предварительная глава о типизированных арифметических выражениях
плавно подводит к ключевой идее типовой безопасности. В промежуточной главе (которую можно про-
пустить) методом Тейта доказывается теорема о нормализации для простого типизированного лямбда-
исчисления. Часть III посвящена основополагающему механизму наследования; она содержит подроб-
ное обсуждение метатеории и два расширенных примера. В Части IV рассматриваются рекурсивные
типы, как в простой изорекурсивной формулировке, так и в более хитроумной эквирекурсивной. Вторая
из двух глав этой части развивает метатеорию системы с эквирекурсивными типами и наследованием
в рамках математической конструкции с коиндукцией. Темой Части V является полиморфизм. Она
содержит главы по реконструкции типов в стиле ML, по более мощному импредикативному полимор-
физму Системы F, по экзистенциальной квантификации и ее связям с абстрактными типами данных,
а также по комбинации полиморфизма и наследования в системах с ограниченной квантификацией. В
Части VI речь идет об операторах над типами. В одной главе вводятся основные понятия; в следую-
щей разрабатывается Система F
ω
и ее метатеория; в третьей операторы над типами скрещиваются с
ограниченной квантификацией, давая в результате Систему F
ω
; последняя глава представляет собой
расширенный пример.
Основные зависимости между главами изображены на рис. 1. Серые стрелки означают, что только
часть более поздней главы зависит от более ранней.
Обсуждение каждой языковой конструкции, представленной в книге, следует общей схеме. Сна-
чала идут мотивирующие примеры; затем формальные определения; затем доказательства основных
свойств, таких как типовая безопасность; затем (обычно в отдельной главе) более глубокое исследование
метатеории, которое ведет к алгоритмам проверки типов и доказательству их корректности, полноты и
гарантии завершения; наконец (опять же, в отдельной главе) конкретная реализация этих алгоритмов
в виде программы на языке OCaml.
На протяжении всей книги важным источником примеров служит анализ и проектирование язы-
ковых свойств для объектно-ориентированного программирования. В четырех главах с расширенными
примерами детально развиваются различные подходы — простая модель с обыкновенными импера-
тивными объектами и классами (Глава 18), базовое исчисление, основанное на Java (Глава 19), более
изысканный подход к императивным объектам с использованием ограниченной квантификации (Гла-
ва 27) и рассмотрение объектов и классов в рамках чисто функциональной Системы F
ω
, при помощи
экзистенциальных типов (Глава 32).
Для того, чтобы удержать размер книги в рамках необходимого для односеместрового продвинутого
курса — а вес ее в рамках подъемного для среднего аспиранта, — пришлось исключить из рассмотрения
rev. 104
5
1 2 3
oo
4
>>
}
}
}
}
}
}
}
}
5
OO
8
``
A
A
A
A
A
A
A
A
6
OO
9
``
A
A
A
A
A
A
A
A
OO
7
OO
>>
}
}
}
}
}
}
}
}
11
OO
12
``
A
A
A
A
A
A
A
A
23
jj
U
U
U
U
U
U
U
U
U
U
U
U
U
U
U
U
U
U
U
U
U
U
U
U
U
U
10
>>
}
}
}
}
}
}
}
}
99
s
s
s
s
s
s
s
s
s
s
s
s
s
s
s
s
s
s
s
s
s
s
s
s
s
s
s
s
s
13
66
n
n
n
n
n
n
n
n
n
n
n
n
n
n
n
n
14
>>
}
}
}
}
}
}
}
}
15
OO
22
``
A
A
A
A
A
A
A
A
24
OO
16
44
i
i
i
i
i
i
i
i
i
i
i
i
i
i
i
i
i
i
i
i
i
i
i
i
i
18
OO
66
n
n
n
n
n
n
n
n
n
n
n
n
n
n
n
n
25
hh
P
P
P
P
P
P
P
P
P
P
P
P
P
P
P
P
33
f
f
f
f
f
f
f
f
f
f
f
f
f
f
f
f
f
f
f
f
f
f
f
f
f
f
f
f
f
f
f
f
f
f
19
OO
20
hh
[[6
6
6
6
6
6
6
6
6
6
6
6
6
6
6
6
6
6
6
6
6
6
6
6
6
6
6
6
26
jj
U
U
U
U
U
U
U
U
U
U
U
U
U
U
U
U
U
U
U
U
U
U
U
U
U
OO
VV
17
HH
OO
28
hh
P
P
P
P
P
P
P
P
P
P
P
P
P
P
P
P
55
21
XX0
0
0
0
0
0
0
0
0
0
0
0
0
0
0
0
>>
}
}
}
}
}
}
}
}
27
hh
>>
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
29
>>
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
}
30
oo
OO
31
oo
CC
32
oo
``
A
A
A
A
A
A
A
A
Рис. 1. Зависимости между главами
многие интересные и важные темы. Денотационный и аксиоматический подходы к семантике опущены
полностью; по этим направлениям уже существуют замечательные книги, и эти темы отвлекали бы
от строго прагматической, ориентированной на реализацию перспективы, принятой в этой книге. В
нескольких местах делаются намеки на богатые связи между системами типов и логикой, но в детали
я не вдаюсь; эти связи важны, но они увели бы нас слишком далеко в сторону. Многие продвину-
тые черты языков программирования и систем типов лишь кратко упомянуты, например, зависимые
типы, типы-пересечения, а также соответствие Карри-Ховарда; краткие разделы по этим вопросам
служат как отправные пункты для дальнейшего чтения. Наконец, за исключением краткого экскурса
в Java-подобный базовый язык (Глава 19), в книге рассматриваются исключительно языки на основе
лямбда-исчисления; однако понятия и механизмы, исследованные в этих рамках, могут напрямую быть
перенесены в родственные области, такие как типизированные параллельные языки, типизированные
ассемблеры и специализированные исчисления объектов.
Требуемая подготовка
Текст не предполагает никаких знаний по теории языков программирования, однако читатели долж-
ны в известной степени обладать математической зрелостью — а именно, иметь опыт строгой учебной
работы в таких областях, как дискретная математика, алгоритмы и элементарная логика.
Читатели должны быть знакомы по крайней мере с одним функциональным языком высокого уров-
rev. 104
6
ня (Scheme, ML, Haskell и т. п.) и с основными понятиями в теории языков программирования и ком-
пиляторов (абстрактный синтаксис, грамматики BNF, вычисление, абстрактные машины и т. п.). Этот
материал доступен для изучения во множестве замечательных учебников; я особенно ценю “Основ-
ные понятия языков программирования” Фридмана, Ванда и Хейнса (Friedman, Wand, and Haynes,
Essentials of Programming Languages, 2001), а также “Прагматику языков программирования” Скотта
(Scott, Programming Language Pragmatics, 1999). В нескольких главах полезен будет опыт работы с
объектно-ориентированным языком, например, с Java (Arnold and Gosling, 1996).
Главы, посвященные конкретным реализациям программ проверки типов, содержат большие фраг-
менты кода на OCaml (он же Objective Caml), популярном диалекте языка ML. Для чтения этих глав
будет полезно знать OCaml заранее, но это не абсолютно необходимо; используется только небольшое
подмножество языка, и его конструкции объясняются при первом использовании. Эти главы образуют
отдельную нить в ткани книги, и при желании их можно полностью пропустить.
В настоящее время лучший учебник по OCaml — Кузино и Мони (Cousineau and Mauny, 1998).
Кроме того, вполне читабельны и учебные материалы, поставляемые с дистрибутивом OCaml (http:
//caml.inria.fr или http://www.ocaml.org).
Для читателей, знакомых с другим крупным диалектом ML, Стандартным ML, фрагменты кода на
OCaml не должны представлять трудности. Срели популярных учебников по Стандартному ML можно
назвать книги Поульсона (Paulson 1996) и Ульмана (Ullman 1997).
Примерный план курса
В рамках аспирантского курса среднего или продинутого уровня должно быть возможно пройти
большую часть материала книги за семестр. На рис 2 показана примерная схема продвинутого курса
для аспирантов Пенсильванского университета (две лекции по 90 минут в неделю; предполагается нали-
чие минимальной подготовки в теории языков программирования, однако продвижение очень быстрое).
При составлении курса для студентов или начинающих аспирантов можно выбрать несколько спо-
собов подачи материала. Курс по системам типов в программировании будет сосредоточен на главах,
где вводятся различные особенности типовых систем и показывается их использование; большая часть
метатеории и главы, где строятся реализации, будут пропущены. Курс по основам теории и реализации
систем типов, с другой стороны, может использовать все ранние главы, возможно, за исключением
Главы 12 (еще, может быть, 19 и 21), принося в жертву более сложный материал в конце книги. Воз-
можно также построить более короткие курсы, выбирая отдельные главы и следуя диаграмме на Рис. 1.
Книгу можно также использовать как основной текст в более широко организованном аспирант-
ском курсе по теории языков программирования. Такой курс может потратить половину или две трети
семестра на прохождение большей части книги, а остаток времени посвятить, скажем, рассмотрению
теории параллелизма на основе книги Милнера по пи-исчислению (Milner 1999), введению в логику
Хоара и аксиоматическую семантику (напр., Winskel 1993) или обзору продвинутых языковых кон-
струкций вроде продолжений или модульных систем.
Если существенная роль отводится курсовым проектам, может оказаться полезным отложить часть
теоретического материала (скажем, нормализацию, и, возможно, некоторые главы по метатеории), что-
бы продемонстрировать широкий спектр примеров, прежде чем студенты выберут себе курсовые.
Упражнения
Большинство глав снабжено многочисленными примерами — некоторые рассчитаны на решение с
помощью карандаша и бумаги, некоторые требуют программирования в обсуждаемых исчислениях, а
некоторые рассматривают расширения для реализаций этих исчислений на ML. Ожидаемая сложность
упражнений указывается по следующей шкале:
Контрольный вопрос от 30 секунд до 5 минут
Простое 1 час
Средней сложности 3 часа
Тяжелое 3 часов
Упражения, отмеченные знаком , предназначены для быстрой проверки, насколько усвоен смысл
какого-либо важного понятия. Я советую читателю останавливаться и отвечать на них, прежде чем
rev. 104
7
Лекция Тема Материал
1. Обзор курса; история; административные формальности 1, (2)
2. Предварительная информация: синтаксис, операционная семантика 3, 4
3. Введение в лямбда-исчисление 5.1, 5.2
4. Формализация лямбда-исчисления 5.3, 6.7
5. Типы; простое типизированное лямбда-исчисление 8, 9, 10
6. Простые расширения; производные формы 11
7. Дальнейшие расширения 11
8. Нормализация 12
9. Ссылки; исключения 13, 14
10. Наследование 15
11. Метатеория наследования 16, 17
12. Императивные объекты 18
13. Облегченная Java 19
14. Рекурсивные типы 20
15. Метатеория рекурсивных типов 21
16. Метатеория рекурсивных типов 21
17. Реконструкция типов 22
18. Универсальный полиморфизм 23
19. Экзистенциональный полиморфизм; АТД 24, (25)
20. Ограниченная квантификация 26, 27
21. Метатеория ограниченной квантификации 28
22. Операторы над типами 29
23. Метатеория F
ω
30
24. Наследование высшего уровня 31
25. Чисто функциональные объекты 32
26. Лекция про запас
Рис. 2. Примерная схема продвинутого аспирантского курса
продолжать чтение. В каждой главе набор упражнений примерно размером с домашнее задание отмечен
знаком Рекомендуется.
В Приложении A для большинства упражнений приведены полные решения. Чтобы избавить чита-
теля от поиска, в тех немногих случаях, когда их нет, используется значок .
Типографские соглашения
Большинство глав книги построено так: сначала особенности некоторой системы типов описываются
в тексте, затем эта система определяется формально как набор правил вывода, сведенных в одну или
несколько таблиц. Для того, чтобы облегчить их использование в качестве справочника, обычно эти
определения приводятся полностью, включая не только новые правила для особенностей, обсуждаемых
в данный момент, но и остальные, сколько их требуется для построения полного исчисления. Новые
части системы печатаются на сером фоне, чтобы отличия от предыдущих систем были более заметны.
Необычным качеством этой книги является то, что все примеры были механически проверены при
верстке: с помощью особого скрипта из каждой главы извлекались примеры, строилась и компили-
ровалась специальная программа проверки типов, содержащая обсуждаемые в главе особенности, эта
программа прогонялась на примерах, и результаты проверки вставлялись в текст. Система, которая де-
лает при этом всю сложную работу, называется TinkerType и была написана Майклом Левином и мной
(Levin and Pierce 2001). Средства на ее разработку были получены от Национального Научного Фон-
да по грантам CCR-9701826 Принципиальные основы программирования с объектами и CCR-9912352
Модульные системы типов.
rev. 104
8
Электронные ресурсы
Веб-сайт, посвященный этой книге, можно найти по адресу
http://www.cis.upenn.edu/~bcpierce/tapl
На этом сайте расположены следующие ресурсы: список ошибок, найденных в тексте, предложения по
возможным курсовым проектам, ссылки на дополнительный материал, предоставленные читателями,
а также набор реализаций (программы проверки типов и простые интерпретаторы) для исчислений,
построенных в каждой из глав книги.
Эти реализации представляют собой среду для экспериментов с примерами, приведенными в книге,
и для проверки ответов на упражнения. Они написаны с упором на читабельность и расширяемость.
Студенты в моих курсах успешно использовали их в качестве основы как для простых упражнений, тре-
бующих реализации, так и для курсовых проектов более солидного размера. Эти реализации написаны
на OCaml. Компилятор OCaml доступен бесплатно по адресу http://caml.inria.fr, и на большинстве
платформ устанавливается безо всякого труда.
Читателям стоит также знать о существовании Types Forum, списка рассылки, посвященного всем
аспектам систем типов и их реализации. Список модерируется, так что в нем обеспечиваются отно-
сительно малый объем и высокая доля полезного сигнала по отношению к шуму в объявлениях и
дискуссиях. Архивы и инструкции для подписчиков можно найти по адресу http://www.cis.upenn.
edu/~bcpierce/types.
Благодарности
Читатели, которые найдут эту книгу полезной, должны прежде всего быть благодарны четырем
учителям — Луке Карделли, Бобу Харперу, Робину Милнеру и Джону Рейнольдсу, — которые научили
меня почти всему, что я знаю о языках программирования и типах.
Остаток своих знаний я приобрел в основном в совместных проектах; помимо Луки, Боба, Робина и
Джона, среди моих партнеров в этих проектах были Мартин Абади, Гордон Плоткин, Рэнди Поллак,
Дэвид Н. Тёрнер, Дидье Реми, Давиде Санджорджи, Адриана Компаньони, Мартин Хофман, Джузеппе
Кастанья, Мартин Стеффен, Ким Брюс, Наоки Кобаяси, Харуо Хосоя, Ацуси Игараси, Филип Уодлер,
Питер Бьюнеман, Владимир Гапеев, Майкл Левин, Питер Сьюэлл, Джером Вуийон и Эйдзиро Сумии.
Совместная работа послужила для меня не только источником понимания, но и удовольствия от работы
над этой темой.
Структура и организация этого текста стали лучше в результате консультаций по педагогике с
Торстеном Альтеркирхом, Бобом Харпером и Джоном Рейнольдсом, а сам текст выиграл от замечаний
и исправлений, авторами которых были Джим Александер, Джош Бердин, Тони Боннер, Джон Танг
Бойланд, Дэйв Кларк, Диего Дайнезе, Оливье Данви, Мэттью Дэвис, Владимир Гапеев, Боб Харпер,
Эрик Хилсдейл, Харуо Хосоя, Ацуси Игараси, Роберт Ирвин, Такаясу Ито, Асаф Кфури, Майкл Левин,
Василий Литвинов, Пабло Лопес Оливас, Дэйв Маккуин, Нарсисо Марти-Олиет, Филипп Менье, Робин
Милнер, Матти Нюкянен, Гордон Плоткин, Джон Превост, Фермин Рейг, Дидье Реми, Джон Рейнольдс,
Джеймс Рили, Охад Роде, Юрген Шлегельмильх, Алан Шмитт, Эндрю Схонмакер, Олин Шиверс,
Педрита Стивенс, Крис Стоун, Эйдзиро Сумии, Вэл Тэннен, Джером Вуийон и Филип Уодлер (я прошу
прощения, если кого-то случайно забыл включить в этот список). Лука Карделли, Роджер Хиндли, Дэйв
Маккуин, Джон Рейнольдс и Джонатан Селдин поделились исторической перспективой по отношению
к некоторым запутанным вопросам.
Участники моих аспирантских семинаров в Индианском университете в 1997 и 1998 годах и в Пен-
сильванском университете в 1999 и 2000 годах работали с ранними версиями этой книги; их реакции
и комментарии помогли мне придать ей окончательную форму. Боб Прайор и его сотрудники в из-
дательстве MIT Press весьма профессионально провели рукопись через все многочисленные стадии
публикации. Дизайн книги основан на макросах L
A
T
E
X, которые разработал для MIT Press Кристофер
Маннинг.
rev. 104
9
Доказательства программ
настолько скучны, что
социальные механизмы
математики на них не работают.
Ричард Де Милло, Ричард
Липтон и Алан Перлис, 1979
. . . Так что на социальные
механизмы при верификации
рассчитывать не стоит.
Дэвид Дилл, 1999
Формальные методы не будут
иметь существенного влияния
до тех пор, пока их не смогут
использовать люди, их не
понимающие.
приписывается Тому Мелхэму
rev. 104
10
rev. 104