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