Системы типизации
Материал из Seo Wiki - Поисковая Оптимизация и Программирование
Системы типизации в достаточной степени развиты в современных языках программирования и отражают общую технику использования объектов. При этом считается, что имеется две системы объектов, причем элементам одной из них ставятся в соответствие элементы другой. В зависимости от того, как это делается, возникает тот или иной подход к типизации, аггрегации или классификации объектов.
Обычно при изложении вопросов, связанных с представлением о типе, рассматриваются не теории типов вообще, а одна довольно специальная система, формализующая приписывание типа. В ее рамках типы строятся исключительно из типовых переменных и стрелок, а термы строятся исключительно из лямбда-абстракций и/или комбинаторных термов и аппликаций[1].
Содержание |
[править] Полиморфная типизация
Рассматриваемое приписывание типов полиморфно в том смысле, что у произвольно взятого терма может быть более одного типа, по сути бесконечное множество типов. Вместе с тем такая система не содержит <math>\forall</math>-типов, являясь, таким образом, более слабой, чем сильные полиморфные теории, которые в настоящее время используются в логике и программировании. Эта система лежит в основе всех прочих систем типов, а ее свойства играют самостоятельную роль, так что она вполне заслуживает самостоятельного изучения.
[править] Базовая роль техники приписывания типов
Овладение техникой приписывания типов является прекрасной базовой подготовкой для изучения подходов, характерных для теории типов в целом. Ее методы и алгоритмы нетривиальны, но их основные идеи становятся ясными, как только базовые понятия окажутся осмысленными и освоенными в достаточной мере. Многие из идей, которые при формулировании для сильных теорий типов выглядят достаточно громоздкими и сложными, а также ряд приемов анализа различных структур, применяемых в этих теориях, в системе приписывания типов принимают весьма ясную и наглядную форму.
[править] Разновидности теорий типов
Теории типов восходят к Б. Расселу (B. Russel). В начале 1900-х гг. теории типов строились для довольно специальных целей разрешения парадоксов, которые в то время нарушали построение оснований математики. С течением времени теории типов нашли более широкое применение, став частью обязательных логических средств, в особенности в теории доказательств. Использование теорий типов в комбинаторной логике восходит к работе Х. Карри 1934-го г. (H. Curry), а в <math>\lambda</math>-исчислении — к работе А. Черча 1940-го г. (A. Church). Однако вплоть до 1970-х гг. теории типов оставались относительно узко используемыми только специалистами
[править] Языки программирования, реализующие теории типов
К тому времени возникла потребность в языках программирования с большими выразительными возможностями, и теории типов стали привлекать внимание специалистов в области компьютерных наук. В 1970-х и 1980-х гг. было разработано несколько новых языков, основанных на теории типов. Эти языки хорошо себя зарекомендовали при построении различных приложений и стали известными как в среде специалистов, так и вне этой среды. Основным среди этих языков стал ML, разработанный в Эдинбургском университете группой исследователей под руководством Робина Милнера. Помимо него появились языки HOL (Кембриджский университет), Miranda (Research Software Ltd.) и Nuprl (Корнелльский университет).
[править] Развитие систем типизации
Во всех этих языках содержится компонента приписывания типов, а еще не так давно приписывание типов служило введением к изучению более сильных систем типизации, как, например, в работе Х. Карри и Р. Фейса 1958-го г. (H. Curry and R. Feys). Однако со временем система приписывания типов перестала казаться тривиальной, а стала рассматриваться как вполне самостоятельная система, которая к тому же оказалась более сложной, чем это ожидалось. Эволюции взглядов на систему приписывания типов посвящена не одна работа. В этой связи можно указать, например работу Д. Скотта (D. Scott). Как оказалось, на многие вопросы все еще не имеется завершенных ответов, а попытки их поиска приводят к интересным приемам и методам, имеющим практические применения, например, при построении алгоритмов проверки типов.
На самом деле к настоящему времени о приписывании типов известно намного больше, чем можно уместить в одной статье. Те разделы, которые здесь нашли отражение, позволяют только понять суть дела. Для дальнейшего чтения можно порекомендовать, например, работу Р. Хиндли (R. Hindley).
[править] См. также
[править] Примечания
- ↑ 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.en:Type system