Системы типизации

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

Обычно при изложении вопросов, связанных с представлением о типе, рассматриваются не теории типов вообще, а одна довольно специальная система, формализующая приписывание типа. В ее рамках типы строятся исключительно из типовых переменных и стрелок, а термы строятся исключительно из лямбда-абстракций и/или комбинаторных термов и аппликаций^[1].

Полиморфная типизация

Рассматриваемое приписывание типов полиморфно в том смысле, что у произвольно взятого терма может быть более одного типа, по сути бесконечное множество типов. Вместе с тем такая система не содержит $\forall$-типов, являясь, таким образом, более слабой, чем сильные полиморфные теории, которые в настоящее время используются в логике и программировании. Эта система лежит в основе всех прочих систем типов, а ее свойства играют самостоятельную роль, так что она вполне заслуживает самостоятельного изучения.

Базовая роль техники приписывания типов

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

Разновидности теорий типов

Теории типов восходят к Б. Расселу (B. Russel). В начале 1900-х гг. теории типов строились для довольно специальных целей разрешения парадоксов, которые в то время нарушали построение оснований математики. С течением времени теории типов нашли более широкое применение, став частью обязательных логических средств, в особенности в теории доказательств. Использование теорий типов в комбинаторной логике восходит к работе Х. Карри 1934-го г. (H. Curry), а в $\lambda$-исчислении — к работе А. Черча 1940-го г. (A. Church). Однако вплоть до 1970-х гг. теории типов оставались относительно узко используемыми только специалистами

Языки программирования, реализующие теории типов

К тому времени возникла потребность в языках программирования с большими выразительными возможностями, и теории типов стали привлекать внимание специалистов в области компьютерных наук. В 1970-х и 1980-х гг. было разработано несколько новых языков, основанных на теории типов. Эти языки хорошо себя зарекомендовали при построении различных приложений и стали известными как в среде специалистов, так и вне этой среды. Основным среди этих языков стал ML, разработанный в Эдинбургском университете группой исследователей под руководством Робина Милнера. Помимо него появились языки HOL (Кембриджский университет), Miranda (Research Software Ltd.) и Nuprl (Корнелльский университет).

Развитие систем типизации

Во всех этих языках содержится компонента приписывания типов, а еще не так давно приписывание типов служило введением к изучению более сильных систем типизации, как, например, в работе Х. Карри и Р. Фейса 1958-го г. (H. Curry and R. Feys). Однако со временем система приписывания типов перестала казаться тривиальной, а стала рассматриваться как вполне самостоятельная система, которая к тому же оказалась более сложной, чем это ожидалось. Эволюции взглядов на систему приписывания типов посвящена не одна работа. В этой связи можно указать, например работу Д. Скотта (D. Scott). Как оказалось, на многие вопросы все еще не имеется завершенных ответов, а попытки их поиска приводят к интересным приемам и методам, имеющим практические применения, например, при построении алгоритмов проверки типов.

На самом деле к настоящему времени о приписывании типов известно намного больше, чем можно уместить в одной статье. Те разделы, которые здесь нашли отражение, позволяют только понять суть дела. Для дальнейшего чтения можно порекомендовать, например, работу Р. Хиндли (R. Hindley).

См. также

• Комбинаторная логика
• Лямбда-исчисление
• Теория типов

Примечания

1. ↑ Hindley J.R. Basic simple type theory. — Cambridge University Press, 1995.

Литература

• Вольфенгаген В. Э. Методы и средства вычислений с объектами. Аппликативные вычислительные системы. — М.: JurInfoR Ltd., АО «Центр ЮрИнфоР», 2004. — xvi+789 с ISBN 5-89158-100-0.
• Hindley J.R. Basic simple type theory. — Cambridge University Press, 1995.