Теория типов

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

Теория типов — математически формализованная база для проектирования, анализа и изучения систем типов данных в теории языков программирования (раздел информатики). Многие программисты используют это понятие для обозначения любого аналитического труда, изучающего системы типов в языках программирования. В научных кругах под теорией типов чаще всего понимают более узкий раздел дискретной математики, в частности λ-исчисление с типами.

Современная теория типов была частично разработана в процессе разрешения парадокса Рассела и во многом базируется на работе Бертрана Рассела и Альфреда Уайтхеда «Principia mathematica».

Доктрина типов

Доктрина типов восходит к Б. Расселу, согласно которому всякий тип рассматривается как диапазон значимости пропозициональной (высказывательной) функции. Помимо того, считается, что у всякой функции имеется тип (её домен, область определения). В доктрине типов соблюдается выполнимость принципа замены типа (высказывания) на дефинициально эквивалентный тип (высказывание).

Теория типов в логике

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

Некоторая теория типов

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

Разветвлённая теория типов

Разветвлённая теория типов (Ramified Theory of Types, RTT)

Интуиционистская теория типов

Интуиционистскую теорию типов (Intuitionistic Type Theory, ITT) построил Пер Мартин-Лёф.

Чистые системы типов

Теория чистых систем типов (англ. pure type systems, PTS) обобщает все исчисления лямбда-куба и формулирует правила, позволяющие вычислить их как частные случаи. Её независимо построили Берарди (Berardi) и Терлоу (Terlouw). Чистые системы типов оперируют только понятием типа, рассматривая все понятия других исчислений только в виде типов — потому они и называются «чистыми». Не производится разделения между термами и типами, между различными слоями (т.е. рода́ типов также называются типами, только относящимися к другой вселенной), и даже сами слои называются не сортами, а типами (точнее, вселенными типов). В общем виде, чистая система типов задаётся понятием спецификации, пятью жёсткими правилами и двумя гибкими (меняющимися от системы к системе). Спецификация чистой системы типов представляет собой тройку (S,A,R), где S — множество сортов (Sorts), A — множество аксиом (Axioms) над этими сортами и R — множество правил (Rules).

Многомерные теории типов

Теории типов высших размерностей (англ. higher-dimensional type theories или просто higher type theories, HTT) обобщают традиционные теории типов, разрешая устанавливать нетривиальные отношения равенства между типами. Например, если взять множество пар (декартовых произведений) натуральных чисел nat × nat и множество функций, возвращающих натуральное число nat -> nat, то нельзя утверждать, что элементы этих множеств попарно равны, но можно утверждать, что эти множества эквивалентны. Изоморфизмы между типами и изучаются в двухмерной, трёхмерной и т.д. теориях типов. Весь необходимый базис для формулировки этих теорий был заложен ещё Жираром — Рейнольдсом, но сами теории были сформулированы много позже.

Гомотопическая теория типов

Гомотопическая теория типов (англ. homotopy type theory, HoTT) обобщает многомерные теории, устанавливая равенства типов на уровне топологий.

См. также

• Система типов
• Типобезопасность
• Логицизм
• Many-sorted logic

Литература

• Jean-Yves Girard. Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur ( (фр.)). — Université Paris 7, 1972.

• Robin Milner. A Theory of Type Polymorphism in Programming. — Journal of Computer and System Sciences, 1978. — Т. 17, вып. 3. — С. 348—375. — DOI:10.1016/0022-0000(78)90014-4.

• John C. Reynolds. [booksee.org/book/696403 Theories of programming languages]. — Cambridge University Press, 1998. — ISBN 978-0-521-59414-1 (hardback), 978-0-521-10697-9 (paperback).

• Henk Barendregt. Introduction to Generalized Type Systems. — 1991.

• Henk Barendregt. Lambda Calculi with Types. — Oxford University Press, 1992. — Т. Handbook of Logic in Computer Science, vol.2. — С. 117—309.

• Benjamin Pierce. [www.cis.upenn.edu/~bcpierce/tapl/ Types and Programming Languages]. — MIT Press, 2002. — ISBN 0-262-16209-1.
  • Перевод на русский язык: Бенджамин Пирс. Типы в языках программирования. — Добросвет, 2012. — 680 с. — ISBN 978-5-7913-0082-9.

• Fariouz Kamareddine, Twan Laan, Rob Nederpelt. A Modern Perspective on Type Theory. From its Origins until Today. — Kluwer Academic Publishers, 2004. — ISBN 1-4020-2334-0 (print), 1-4020-2335-9 (eBook).

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

• Robert Harper. [existentialtype.wordpress.com/2011/05/30/higher-dimensional-type-theory/ Higher-Dimensional Type Theory]. — 2011.

• Robert Harper. [bookfi.org/book/1076504 Practical Foundations for Programming Languages]. — version 1.37 (revised 01.11.2014). — licensed under the Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 United States License., 2012. — 544 с.

Ссылки

• [www.intuit.ru/department/se/tppfunc/7/ Лекция: Теория типов и комбинаторная логика]

Отрывок, характеризующий Теория типов

Денисов не отвечал; он подъехал к Пете, слез с лошади и дрожащими руками повернул к себе запачканное кровью и грязью, уже побледневшее лицо Пети.
«Я привык что нибудь сладкое. Отличный изюм, берите весь», – вспомнилось ему. И казаки с удивлением оглянулись на звуки, похожие на собачий лай, с которыми Денисов быстро отвернулся, подошел к плетню и схватился за него.
В числе отбитых Денисовым и Долоховым русских пленных был Пьер Безухов.


О той партии пленных, в которой был Пьер, во время всего своего движения от Москвы, не было от французского начальства никакого нового распоряжения. Партия эта 22 го октября находилась уже не с теми войсками и обозами, с которыми она вышла из Москвы. Половина обоза с сухарями, который шел за ними первые переходы, была отбита казаками, другая половина уехала вперед; пеших кавалеристов, которые шли впереди, не было ни одного больше; они все исчезли. Артиллерия, которая первые переходы виднелась впереди, заменилась теперь огромным обозом маршала Жюно, конвоируемого вестфальцами. Сзади пленных ехал обоз кавалерийских вещей.
От Вязьмы французские войска, прежде шедшие тремя колоннами, шли теперь одной кучей. Те признаки беспорядка, которые заметил Пьер на первом привале из Москвы, теперь дошли до последней степени.
Дорога, по которой они шли, с обеих сторон была уложена мертвыми лошадьми; оборванные люди, отсталые от разных команд, беспрестанно переменяясь, то присоединялись, то опять отставали от шедшей колонны.
Несколько раз во время похода бывали фальшивые тревоги, и солдаты конвоя поднимали ружья, стреляли и бежали стремглав, давя друг друга, но потом опять собирались и бранили друг друга за напрасный страх.
Эти три сборища, шедшие вместе, – кавалерийское депо, депо пленных и обоз Жюно, – все еще составляли что то отдельное и цельное, хотя и то, и другое, и третье быстро таяло.
В депо, в котором было сто двадцать повозок сначала, теперь оставалось не больше шестидесяти; остальные были отбиты или брошены. Из обоза Жюно тоже было оставлено и отбито несколько повозок. Три повозки были разграблены набежавшими отсталыми солдатами из корпуса Даву. Из разговоров немцев Пьер слышал, что к этому обозу ставили караул больше, чем к пленным, и что один из их товарищей, солдат немец, был расстрелян по приказанию самого маршала за то, что у солдата нашли серебряную ложку, принадлежавшую маршалу.
Больше же всего из этих трех сборищ растаяло депо пленных. Из трехсот тридцати человек, вышедших из Москвы, теперь оставалось меньше ста. Пленные еще более, чем седла кавалерийского депо и чем обоз Жюно, тяготили конвоирующих солдат. Седла и ложки Жюно, они понимали, что могли для чего нибудь пригодиться, но для чего было голодным и холодным солдатам конвоя стоять на карауле и стеречь таких же холодных и голодных русских, которые мерли и отставали дорогой, которых было велено пристреливать, – это было не только непонятно, но и противно. И конвойные, как бы боясь в том горестном положении, в котором они сами находились, не отдаться бывшему в них чувству жалости к пленным и тем ухудшить свое положение, особенно мрачно и строго обращались с ними.
В Дорогобуже, в то время как, заперев пленных в конюшню, конвойные солдаты ушли грабить свои же магазины, несколько человек пленных солдат подкопались под стену и убежали, но были захвачены французами и расстреляны.
Прежний, введенный при выходе из Москвы, порядок, чтобы пленные офицеры шли отдельно от солдат, уже давно был уничтожен; все те, которые могли идти, шли вместе, и Пьер с третьего перехода уже соединился опять с Каратаевым и лиловой кривоногой собакой, которая избрала себе хозяином Каратаева.
С Каратаевым, на третий день выхода из Москвы, сделалась та лихорадка, от которой он лежал в московском гошпитале, и по мере того как Каратаев ослабевал, Пьер отдалялся от него. Пьер не знал отчего, но, с тех пор как Каратаев стал слабеть, Пьер должен был делать усилие над собой, чтобы подойти к нему. И подходя к нему и слушая те тихие стоны, с которыми Каратаев обыкновенно на привалах ложился, и чувствуя усилившийся теперь запах, который издавал от себя Каратаев, Пьер отходил от него подальше и не думал о нем.
В плену, в балагане, Пьер узнал не умом, а всем существом своим, жизнью, что человек сотворен для счастья, что счастье в нем самом, в удовлетворении естественных человеческих потребностей, и что все несчастье происходит не от недостатка, а от излишка; но теперь, в эти последние три недели похода, он узнал еще новую, утешительную истину – он узнал, что на свете нет ничего страшного. Он узнал, что так как нет положения, в котором бы человек был счастлив и вполне свободен, так и нет положения, в котором бы он был бы несчастлив и несвободен. Он узнал, что есть граница страданий и граница свободы и что эта граница очень близка; что тот человек, который страдал оттого, что в розовой постели его завернулся один листок, точно так же страдал, как страдал он теперь, засыпая на голой, сырой земле, остужая одну сторону и пригревая другую; что, когда он, бывало, надевал свои бальные узкие башмаки, он точно так же страдал, как теперь, когда он шел уже босой совсем (обувь его давно растрепалась), ногами, покрытыми болячками. Он узнал, что, когда он, как ему казалось, по собственной своей воле женился на своей жене, он был не более свободен, чем теперь, когда его запирали на ночь в конюшню. Из всего того, что потом и он называл страданием, но которое он тогда почти не чувствовал, главное были босые, стертые, заструпелые ноги. (Лошадиное мясо было вкусно и питательно, селитренный букет пороха, употребляемого вместо соли, был даже приятен, холода большого не было, и днем на ходу всегда бывало жарко, а ночью были костры; вши, евшие тело, приятно согревали.) Одно было тяжело в первое время – это ноги.
Во второй день перехода, осмотрев у костра свои болячки, Пьер думал невозможным ступить на них; но когда все поднялись, он пошел, прихрамывая, и потом, когда разогрелся, пошел без боли, хотя к вечеру страшнее еще было смотреть на ноги. Но он не смотрел на них и думал о другом.
Теперь только Пьер понял всю силу жизненности человека и спасительную силу перемещения внимания, вложенную в человека, подобную тому спасительному клапану в паровиках, который выпускает лишний пар, как только плотность его превышает известную норму.
Он не видал и не слыхал, как пристреливали отсталых пленных, хотя более сотни из них уже погибли таким образом. Он не думал о Каратаеве, который слабел с каждым днем и, очевидно, скоро должен был подвергнуться той же участи. Еще менее Пьер думал о себе. Чем труднее становилось его положение, чем страшнее была будущность, тем независимее от того положения, в котором он находился, приходили ему радостные и успокоительные мысли, воспоминания и представления.


22 го числа, в полдень, Пьер шел в гору по грязной, скользкой дороге, глядя на свои ноги и на неровности пути. Изредка он взглядывал на знакомую толпу, окружающую его, и опять на свои ноги. И то и другое было одинаково свое и знакомое ему. Лиловый кривоногий Серый весело бежал стороной дороги, изредка, в доказательство своей ловкости и довольства, поджимая заднюю лапу и прыгая на трех и потом опять на всех четырех бросаясь с лаем на вороньев, которые сидели на падали. Серый был веселее и глаже, чем в Москве. Со всех сторон лежало мясо различных животных – от человеческого до лошадиного, в различных степенях разложения; и волков не подпускали шедшие люди, так что Серый мог наедаться сколько угодно.