Теория типов

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

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

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

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

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

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

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

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

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

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

Исторически первой предложенной теорией типов (период с 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 — множество сортов (Sorts), A — множество аксиом (Axioms) над этими сортами и R — множество правил (Rules).

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

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

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

Основная статья: Гомотопическая теория типов

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

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

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

См. также

• Система типов
• Типобезопасность
• Логицизм
• 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. 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. — Vol. Handbook of Logic in Computer Science, vol.2. — P. 117—309.

• Benjamin Pierce. 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. Higher-Dimensional Type Theory. — 2011. Архивировано 13 октября 2016 года.

• Robert Harper. 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 с. Архивная копия от 24 октября 2015 на Wayback Machine

Ссылки

• Лекция: Теория типов и комбинаторная логика