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

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

Глава 1

Введение

1.1. Типы в информатике

Современная технология программного обеспечения располагает широким репертуаром формаль-

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

цификацией ее поведения, явной или неявной. На одном конце шкалы находятся мощные конструкции,

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

тационная семантика. Все они способны выразить требования к корректности программ чрезвычайно

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

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

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

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

на которых они основаны. Примером такого облегченного формального метода могут служить про-

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

схем или коммуникационных протоколов. Другой пример — приобретающий сейчас популярность мо-

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

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

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

Подобно многим другим терминам, используемым в больших сообществах, «систему типов» трудно

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

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

ным для работы с ним. Одно из возможных определений такое:

Система типов — это разрешимый синтаксический метод доказательства, что в програм-

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

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

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

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

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

системы типов (или теория типов) относится к намного более обширной области исследований в

логике, математике и философии. В этом смысле слова типы были впервые формально описаны в на-

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

например, парадокса Рассела (Russell 1902). В течение двадцатого века типы превратились в один из

стандартных инструментов логики, особенно в теории доказательств (см. Gandy 1976 и Hindley 1997),

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

Расселовская ветвящаяся теория типов (Whitehead and Russell, 1910), простая теория типов Рэм-

сея (Ramsey 1925) — основа для простого типизированного лямбда-исчисления Чёрча (Church 1940),

— конструктивная теория типов Мартина-Лёфа (Martin-L¨of 1973, 1984) и чистые системы типов

Бенарди, Терлоу и Барендрегта (Benardi 1988, Terlouw 1989 и Barendregt 1992).

12 1.1. Типы в информатике

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

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

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

зированными лямбда-исчислениями» и разновидностями логики, через соответствие Карри-Ховарда

(§9.4). В этих сообществах используются похожие понятия, системы записи и методы, однако имеют-

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

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

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

чтобы иметь возможность работать с инструментами вроде рекурсивных функций.

Еще одним важным свойством предложенного определения является упоминание классификации

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

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

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

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

Иногда слово «статический» добавляется явным образом — например, говорят о «языках програм-

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

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

(Sussman and Steele 1975; Kelsey, Clinger and Rees, 1998; Dybvig 1996), где при помощи тегов типов

во время выполнения различаются различные виды структур в куче. Термин «динамическая типиза-

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

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

Будучи статическими, системы типов по необходимости консервативны: они способны однозначно

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

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

ведут себя подобающим образом. Например, программа

if <сложная проверка> then S else <ошибка типа>

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

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

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

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

типов их выражениям служит основной движущей силой в нашей научной дисциплине.

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

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

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

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

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

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

обращениях к массиву не выходят за границы.

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

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

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

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

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

по отношению к её собственному набору ошибок времени выполнения.

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

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

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

телем. Нарушения сокрытия информации, например, прямое обращение к полям объекта, чья реали-

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

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

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

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

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

rev. 104

1.2. Для чего годятся типы 13

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

аннотаций типов в программах. Обычно эти аннотации остаются достаточно простыми, чтобы про-

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

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

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

ях, как Расширенная Статическая Проверка (Extended Static Checking; Detlefs, Leino, Nelson and Saxe,

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

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

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

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

томатизации, но к которым прилагаются эффективные алгоритмы проверки типов. Впрочем, можно

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

пов, вроде ML (Damas and Milner, 1982), время проверки в некоторых патологических случаях может

быть громадным (Henglein and Marison 1991). Имеются даже языки, где задача проверки или рекон-

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

большинстве случаев, представляющих практический интерес» (напр., Pierce and Turner 2000; Nadathur

and Miller 1988; Pfenning 1994).

1.2. Для чего годятся типы

1.2.1. Выявление ошибок

Самое очевидное достоинство статической проверки типов — это то, что она помогает раньше обна-

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

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

совершенно другим — или даже после того, как программа выпущена для потребителей. Более того,

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

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

с правильного пути.

На практике статическая проверка типов обнаруживает удивительно широкий спектр ошибок. Про-

граммисты, работающие в языках с богатой системой типов, часто замечают, что их программы имеют

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

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

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

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

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

проявляются как несоответствия на уровне типов. Сила этого эффекта зависит от выразительности си-

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

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

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

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

типов, поддерживающие анализ размерностей (Kennedy 1994)).

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

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

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

помощь, как если для каждой из них определяется тип данных или абстрактный тип. В системы ти-

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

структуре данных.

Для некоторых видов программ процедура проверки типов может служить инструментом сопро-

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

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

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

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

ломается проверка типов.

rev. 104

14 1.2. Для чего годятся типы

1.2.2. Абстракция

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

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

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

которых упаковываются и связываются компоненты больших систем. Типы появляются в интерфей-

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

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

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

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

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

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

проектов.

1.2.3. Документация

Типы полезны также при чтении программ. Объявления типов в заголовках процедур и интерфей-

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

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

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

существенна в сигнатурах модулей.

1.2.4. Безопасность языков

К сожалению, термин «безопасный язык» еще более расплывчат, чем «система типов». Несмотря на

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

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

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

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

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

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

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

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

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

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

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

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

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

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

ке с такими абстракциями можно обращаться абстрактно; в небезопасном нельзя: чтобы полностью

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

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

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

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

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

Безопасность языка — это не то же самое, что статическая безопасность типов. Можно достичь

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

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

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

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

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

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

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

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

rev. 104

1.2. Для чего годятся типы 15

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

ничего), но не доказать их отсутствие.

Статическая проверка динамическая проверка

Безопасные ML, Haskell, Java и т. п. Лисп, Scheme, Perl, Postscript и т. п.

Небезопасные C, C и т. п.

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

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

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

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

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

операций можно нарушить целостность среды выполнения.)

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

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

верку выхода за границы массивов.

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

предоставляют операции (скажем, нисходящее преобразование типов в Java — см. §15.5), чьи правила

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

каждого употребления такой конструкции.

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

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

языках. Иногда такие черные ходы даже содержатся в ограниченном виде внутри самого языка —

Obj.magic в OCaml (Leroy 2000), Unsafe.cast в Нью-Джерсийской реализации Стандартного ML, и т. п.

Языки Modula-3 (Cardelli et al. 1989; Nelson 1991) и C

(Wille 2000) идут еще дальше и включают в

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

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

отмеченных словом unsafe «небезопасный».

Карделли (Cardelli 1996) представляет несколько иную точку зрения на безопасность языка и про-

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

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

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

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

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

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

ния.

Еще одна точка зрения основана на понятии переносимости; ее можно выразить лозунгом «Безопас-

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

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

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

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

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

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

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

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

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

любой корректной реализации этих языков.

1.2.5. Эффективность

Первые системы типов в информатике, начиная с 50-х годов в таких языках, как Фортран (Backus

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

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

необходимые для этого механизмы (на основе зависимых типов — см. $30.5) хорошо изучены, однако такое их исполь-

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

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

можно прочитать у Си и Пфеннинга (Xi and Pfenning 1998, 1999).

rev. 104

16 1.2. Для чего годятся типы

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

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

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

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

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

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

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

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

информации о типах.

Выигрыш в эффективности на основе информации о типах может возникнуть в неожиданных ме-

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

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

рождаемой при проверке типов. Язык Titanium (Yelick et al. 1998) использует вывод типов для анализа

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

чем программисты, оптимизирующие программы вручную. Компилятор ML Kit с помощью мощного

алгоритма вывода регионов (Giﬀord, Jouvelot and Sheldon 1987; Jouvelot and Giﬀord 1991; Talpin and

Jouvelot 1992; Tofte and talpin 1994, 1997; Tofte and Birkedal 1998) заменяет большинство вызовов сбор-

щика мусора (в некоторых программах все вызовы) стековыми операциями управления памятью.

1.2.6. Другие приложения

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

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

способами. Мы упомянем кое-какие из них.

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

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

автоматического конфигурирования (plug and play) сетевых устройств JINI (Arnold et al. 1999), а также

играет ключевую роль в методике «кода, содержащего доказательство» (Proof Carrying Code, Necula

and Lee 1996, 1998; Necula 1997). В то же время, многие основополагаюшие идеи, появившиеся в среде

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

выглядят как разновидности анализа типов (напр., Abadi, Banerjee, Heintze and Riecke 1999; Abadi

1999; Leroy and Rouaix 1998; и т. п.). С другой стороны, растет интерес к прямому приложению теории

языков программирования в области компьютерной безопасности (напр., Abadi 1999; Sumii and Pierce

2001).

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

мо компиляторов. Например, AnnoDomini, утилита преобразования программ на Коболе с точки зрения

Проблемы 2000 года, построена на основе механизма вывода типов в стиле ML (Eidorﬀ et al. 1999). Ме-

тоды вывода типов использовались также в инструментах для анализа псевдонимов (O’Callahan and

Jackson 1997) и анализа исключений (Leroy and Passaux 2000).

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

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

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

включая Nuprl (Constable et al. 1986), Lego (Luo and Pollack 1992; Pollack 1994), Coq (Barras et al. 1997) и

Alf (Magnusson and Nordstr¨om 1994). Констебль (Constable 1994) и Пфеннинг (Pfenning 1999) содержат

обсуждение истории этих систем.

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

стью «сетевых метаданных» в форме Определений Типа Документов (Document Type Deﬁnitions, XML

1998) и других видов схем (таких, как новый стандарт XML-Schema, XS 2000) для описания структу-

рированных данных на XML. Новые языки для запросов к XML и обработки XML-данных обладают

мощными статическими системами типов, прямо основанными на этих языках схем (Hosoya and Pierce

2000; Hosoya, Vouillon and Pierce 2001; Hosoya and Pierce 2001; Relax 2000; Schields 2001).

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

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

Benthem 1995; van Benthem and Meulen 1997; Ranta 1995, и т. д.).

rev. 104

1.3. Системы типов и проектирование языков 17

1.3. Системы типов и проектирование языков

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

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

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

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

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

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

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

оценивается всякое другое решение разработчика.

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

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

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

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

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

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

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

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

считать чрезмерным. Создатели языков семейства ML тщательно старались свести аннотации к самому

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

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

1.4. Краткая история

Самые ранние системы типов в информатике использовались для отображения очень простых раз-

личий в представлении чисел с фиксированной и плавающей точкой (например, в Фортране). В конце

1950-х и начале 1960-х эта классификация была расширена на структурированные данные (массивы

записей и т. п.) и функции высшего порядка. В начале 1970-х появились еще более сложные поня-

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

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

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

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

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

На Рис. 1.1 представлена краткая (и чрезвычайно неполная!) хронология основных достижений в

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

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

библиографии.

1.5. Дополнительная литература

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

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

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

В обзорных статьях Карделли (Cardelli 1996) и Митчелла (Mitchell 1990b) содержится краткое

введение в дисциплину. Статья Барендрегта (Barendregt 1992) предназначена скорее для математи-

ков. Объемный учебник Митчелла «Основания языков программирования» (Mitchell, Foundations for

Programming Languages, 1996) описывает основы лямбда-исчисления, несколько систем типов и многие

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

Рейнольдса «Теории языков программирования» (Reynolds Theories of Programming Languages, 1998b)

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

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

программирования» Шмидта (Schmidt, The Structure of Typed Programming Languages, 1994) развива-

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

rev. 104

18 1.5. Дополнительная литература

1870-е истоки формальной логики Frege (1879)

1900-е формализация математики Whitehead and Russell (1910)

1930-е бестиповое лямбда-исчисление Church (1941)

1940-е простое типизированное лямбда-

исчисление

Church (1940), Curry and Feys (1958)

1950-е Фортран Backus (1981)

Алгол-60 Naur et al. (1963)

1960-е проект Automath de Bruijn (1980)

Симула Birtwistle et al. (1979)

соответствие Карри-Ховарда Howard (1980)

Алгол-68 van Wijngaarden et al. (1975)

1970-е Паскаль Wirth (1971)

Теория типов Мартина-Лёфа Martin-L¨of (1973, 1982)

Системы F , F

Girard (1972)

Полиморфное лямбда-исчисление Reynolds (1974)

CLU Liskov et al. (1981)

полиморфный вывод типов Milner (1978), Damas and Milner (1982)

ML Gordon, Milner and Wadsworth (1979)

типы-пересечения Coppo and Dezani (1978)

Coppo, Dezani and Sall´e (1979), Pottinger

(1980)

1980-е проект NuPRL Constable et al. (1986)

наследование Reynolds (1980), Cardelli (1984), Mitchell

(1984a)

АТД как экзистенциальные типы Mitchell and Plotkin (1988)

исчисление конструкций Coquand (1985), Coquand and Huet (1988)

линейная логика Girard (1987), Girard et al. (1988)

ограниченная квантификация Cardelli and Wegner (1985)

Curien and Ghelli (1992), Cardelli et al. (1994)

Эдинбургская Логическая Конструкция Harper, Honsell and Plotkin (1992)

Forsythe Reynolds (1985)

чистые системы типов Terlouw (1989), Berardi (1988), Barendregt

(1991)

зависимые типы и модульность Burstall and Lampson (1984), MacQueen

(1986)

Quest Cardelli (1991)

системы эффектов Giﬀod et al. (1987), Talpin and Jouvelot

(1992)

переменные строк; расширяемые записи Wand (1987), R´emy (1989)

Cardelli and Mitchell (1991)

1990-е наследование высших порядков Cardelli (1990), Cardelli and Longo (1991)

типизированные промежуточные языки Tarditi, Morrisett et al. (1996)

исчисление объектов Abadi and Cardelli (1996)

полупрозрачные типы и модульность Harper and Lillibridge (1994), Leroy (1994)

типизированный язык ассемблера Morrisett et al. (1998)

Рис. 1.1. Краткая история типов в информатике и логике.

по обыкновенным императивным языкам программирования. Монография Хиндли «Основы теории

простых типов» (Hindley, Basic Simple Type Theory, 1997) представляет собой замечательное собрание

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

систем. Описание скорее глубокое, нежели широкое по охвату.

«Теория объектов» Абади и Карделли (Abadi and Cardelli, A Theory of Objects, 1996) развивает во

rev. 104

1.5. Дополнительная литература 19

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

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

ориентированного программирования. Книга Кима Брюса «Основания объектно-ориентированных язы-

ков: типы и семантика» (Kim Bruce, Foundations of Object-Oriented Languages: Types and Semantics, 2002)

покрывает приблизительно тот же материал. Введение в теорию объектно-ориентированных систем ти-

пов можно также найти в книгах Палсберга и Шварцбаха (Palsberg and Schwartzbach, 1994) и Кастаньи

(Castagna 1997).

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

учебниках Гантера (Gunter 1992), Уинскеля (Winskel 1993) и Митчелла (Mitchell 1996). Кроме того,

операционная семантика детально описана в книге Хеннесси (Hennessy 1990). Основания теории типов

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

Якобса (Jacobs 1999), Асперти и Лонго (Asperti and Longo 1997) и Кроула (Crole 1994); краткое введение

доступно в «Основах теории категоий для специалистов по информатике» (Pierce, Basic Category Theory

for Computer Scientists, 1991a).

Книга Жирара, Лафонта и Тейлора «Доказательства и типы» (Girard, Lafont and Taylor, Proofs and

Types, 1989) посвящена логическим вопросам теории типов (соответствие Карри-Ховарда и т. п.). Кроме

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

ке. Связи между типами и логикой исследуются также в книге «Вычисление и дедукция» Пфеннинга

(Pfenning, Computation and Deduction, 2001). «Теория типов и функциональное программирование»

Томпсона (Thompson, Type Theory and Functional Programming, 1991) и «Конструктивные основания

функциональных языков» Тёрнера (Turner, Constructive Foundations for Functional Languages, 1991)

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

программирования», как в языках Haskell и Miranda) и конструктивной теорий типов, рассматриваемой

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

рованию, рассмотрены в книге «Теория типов и автоматическая дедукция» Гобольт-Ларрека и Макки

(Goubault-Laurrecq and Mackie, Proof Theory and Automated Deduction, 1997). История типов в логике и

философии более подробно описана в статьях Констебля (Constable 1998), Уодлера (Wadler 2000), Юэ

(Huet 1990) и Пфеннинга (Pfenning 1999), в диссертации Лаана (Laan 1997) и в книгах Граттан-Гиннесса

(Grattan-Guinness 2001) и Соммаруги (Sommaruga 2000).

Как выясняется, чтобы

избежать досадных ошибочных

утверждений о корректности

типов в языках

программирования, требуется

немалая доля тщательного

анализа. В результате возникла

формальная дисциплина

классификации, описания и

исследования систем типов.

Лука Карделли (1996)

rev. 104

20 1.5. Дополнительная литература

rev. 104