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

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

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

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

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

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

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

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

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

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

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

Исторически первой предложенной теорией типов (период с 1902 по 1913) является Разветвлённая теория типов ( Ramified Theory of Types , RTT ), построенная Уайтхедом и Расселом, и окончательно сформулированная в фундаментальной работе « Principia Mathematica ». В основе данной теории лежит принцип ограничения числа случаев, когда объекты принадлежат единому типу. Явным образом объявляется восемь таких случаев и различаются две иерархии типов: (просто) «типы» и «порядки». При этом сама нотация «типа» не определена, и имеется ряд других неточностей, т.к. главным намерением было объявить неравными типы функций от разного числа аргументов или от аргументов разных типов . Неотъемлемой составляющей теории является аксиома редуцируемости .

Простая теория типов

Этот раздел не завершён . Вы поможете проекту, исправив и дополнив его.

В 1920-х Чвистек и Рамси предложили неразветвлённую теорию типов, ныне известную как «Теория простых типов» или Простая теория типов ( Simple Type Theory ), которая сворачивает иерархию типов, устраняя необходимость в аксиоме редуцируемости.

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

Этот раздел не завершён . Вы поможете проекту, исправив и дополнив его.

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

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

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

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

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

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

Гомотопическая теория типов ( англ. homotopy type theory , HoTT ) обобщает многомерные теории, устанавливая равенства типов на уровне топологий . В многомерных теориях понятия «эквивалентности типов» и «равенства типов» считаются различными. Радикальным нововведением гомотопической теории является аксиома унивалентности , постулирующая, что если типы топологически эквивалентны, то они топологически равны.

Экономичная теория типов

Экономичная теория типов ( англ. Cost-Aware Type Theory, CATT ), сформулированная в 2020 году , расширяет функциональные типы простейшей информацией об алгоритмической сложности — количестве вычислительных шагов, требуемых для получения результата — позволяя верифицировать программы не только по смысловой корректности, но и по закладываемым ограничениям временной сложности. Это делается за счёт конструктора зависимых типов функций funtime . Формализация теории требует в том числе учёт проблемы остановки , для чего в правилах типизации требуется, чтобы рекурсивный вызов имел строго меньшую сложность, чем вызов с текущим значением аргумента. CATT позволяет при построении доказательства производить различие между «абстрактной стоимостью», включающей математические шаги (такие, как рекурсивный вызов) и «машинной стоимостью», учитывающей эффективность физически реализованных инструкций (например, что арифметические операции суммы и произведения на большинстве процессоров выполняются за одинаковое время), а также учитывать параллелизм .

См. также

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

Примечания

Литература

• 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. — , 1978. — Т. 17 , вып. 3 . — С. 348—375 . — doi : .

• John C. Reynolds. . — 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. — Vol. Handbook of Logic in Computer Science, vol.2. — P. 117—309.

• Benjamin Pierce. . — 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 .

• . . — 2011. 13 октября 2016 года.

• . . — version 1.37 (revised 01.11.2014). — licensed under the Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 United States License., 2012. — 544 с. от 24 октября 2015 на Wayback Machine

Ссылки