Теория типов

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

Первая теория типов — разветвлённая теория типов — разработана в труде Рассела и Уайтхеда «Principia mathematica» для разрешения парадокса Рассела, в её основе лежит принцип ограничения числа случаев, когда объекты принадлежат единому типу. В ней явным образом объявляется восемь таких случаев и различаются две иерархии типов: (просто) «типы» и «порядки». При этом сама нотация «типа» не определена, и имеется ряд других неточностей, так как главным намерением было объявить неравными типы функций от разного числа аргументов или от аргументов разных типов. Существенную роль в развтвлённой теории типов играет аксиома сводимости (для каждого множества существует равнообъёмное ему множество первого порядка), которая критиковалась за неестественность. В 1920-х годах Рамсей разработал неразветвлённую простую теорию типов, которая сворачивает иерархию типов, устраняя необходимость в аксиоме сводимости.

Просто типизированное лямбда-исчисление (Чёрч, 1940) снабдило «стрелочными» типами (бестиповое) лябмда-исчисление, фактически заложило основу применения типов в языках программирования. Среди последующих построений наиболее широкое распространение получила интуиционистская теория типов Матрин-Лёфа (1972), применённая как в теории языков программирования, системах интерактивного доказательства, так и в целом в доказательной математике, задействующей соответствие Карри — Ховарда, став, в частности, основой гомотопической теории типов (Воеводский, 2009). Понятие зависимого типа, играющее центральную роль в интуиционитской теории типов, позволило получить классификацию вариантов типизированного лямбда-исчисления (лямбда-куб, Барендрегт, 1991) и, соответственно, структурировать системы типов в языках программирования и системах интерактивного доказательства.

Литература

• 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).
• 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 с.

Ссылки

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