Теория типов

Понятие в математической логике

В математике и теоретической информатике теория типов — это формальное представление конкретной системы типов . ^[a] Теория типов — это академическое изучение систем типов.

Некоторые теории типов служат альтернативами теории множеств как фундамента математики . Две влиятельные теории типов, которые были предложены в качестве фундамента:

• Типизированное λ-исчисление Алонзо Чёрча
• Интуиционистская теория типов Пера Мартина-Лёфа

Большинство компьютеризированных систем корректуры используют в своей основе теорию типов . Распространенной является «Исчисление индуктивных конструкций» Тьерри Коканда .

История

Теория типов была создана, чтобы избежать парадокса в математическом уравнении, основанном на наивной теории множеств и формальной логике . Парадокс Рассела (впервые описанный в работе Готтлоба Фреге « Основания арифметики ») заключается в том, что без надлежащих аксиом можно определить множество всех множеств, которые не являются членами самих себя; это множество как содержит себя, так и не содержит себя. В период с 1902 по 1908 год Бертран Рассел предложил различные решения этой проблемы.

К 1908 году Рассел пришел к разветвленной теории типов вместе с аксиомой сводимости , обе из которых появились в Principia Mathematica Уайтхеда и Рассела , опубликованных в 1910, 1912 и 1913 годах. Эта система избежала противоречий, предложенных в парадоксе Рассела, создав иерархию типов, а затем присвоив каждую конкретную математическую сущность определенному типу. Сущности данного типа были построены исключительно из подтипов этого типа, ^[b] таким образом предотвращая определение сущности с использованием самой себя. Это разрешение парадокса Рассела похоже на подходы, принятые в других формальных системах, таких как теория множеств Цермело-Френкеля . ^[3]

Теория типов особенно популярна в сочетании с лямбда-исчислением Алонзо Чёрча . Одним из примечательных ранних примеров теории типов является просто типизированное лямбда-исчисление Чёрча . Теория типов Чёрча ^[4] помогла формальной системе избежать парадокса Клини–Россера , который поразил исходное нетипизированное лямбда-исчисление. Чёрч продемонстрировал ^[c] , что оно может служить основой математики , и его называли логикой высшего порядка .

В современной литературе «теория типов» относится к типизированной системе, основанной на лямбда-исчислении. Одной из влиятельных систем является интуиционистская теория типов Пера Мартина-Лёфа , которая была предложена в качестве основы для конструктивной математики . Другой — исчисление конструкций Тьерри Коканда , которое используется в качестве основы Коком , Лином и другими помощниками по компьютерному доказательству . Теория типов является активной областью исследований, одним из направлений которых является разработка теории гомотопических типов .

Приложения

Математические основы

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

Математики, работающие в области теории категорий , уже испытывали трудности при работе с общепринятой основой теории множеств Цермело–Френкеля . Это привело к таким предложениям, как «Элементарная теория категории множеств» Ловера (ETCS). ^[6] Теория гомотопических типов продолжает эту линию, используя теорию типов. Исследователи изучают связи между зависимыми типами (особенно типом тождества) и алгебраической топологией (в частности, гомотопией ).

Помощники по проверке

Большая часть современных исследований в области теории типов основана на контролерах доказательств , интерактивных помощниках по доказательству и автоматизированных доказывателях теорем . Большинство этих систем используют теорию типов в качестве математической основы для кодирования доказательств, что неудивительно, учитывая тесную связь между теорией типов и языками программирования:

• LF используется Twelf , часто для определения других теорий типов;
• многие теории типов, которые подпадают под логику высшего порядка, используются семейством доказывающих устройств HOL и PVS ;
• Теория вычислительного типа используется в NuPRL ;
• исчисление конструкций и его производные используются Coq , Matita и Lean ;
• UTT (Единая теория зависимых типов Луо) используется в Agda , которая является как языком программирования, так и помощником по доказательству.

Многие теории типов поддерживаются LEGO и Isabelle . Isabelle также поддерживает фундаменты помимо теорий типов, такие как ZFC . Mizar является примером системы доказательств, которая поддерживает только теорию множеств.

Языки программирования

Любой статический анализ программы , например, алгоритмы проверки типов в фазе семантического анализа компилятора , имеет связь с теорией типов. Ярким примером является Agda , язык программирования, который использует UTT (Luo's Unified Theory of dependible Types) для своей системы типов.

Язык программирования ML был разработан для манипулирования теориями типов (см. LCF ), и его собственная система типов находилась под их сильным влиянием.

Лингвистика

Теория типов также широко используется в формальных теориях семантики естественных языков , ^{[7] [8]} особенно грамматика Монтегю ^[9] и ее потомки. В частности, категориальные грамматики и предгрупповые грамматики широко используют конструкторы типов для определения типов ( существительное , глагол и т. д.) слов.

Наиболее распространенная конструкция берет базовые типы и для индивидов и истинностных значений соответственно и определяет набор типов рекурсивно следующим образом: ${\displaystyle e}$ ${\displaystyle t}$

• если и являются типами, то также является ; ${\displaystyle a}$ ${\displaystyle b}$ ${\displaystyle \langle a,b\rangle }$
• ничего, кроме основных типов, и то, что может быть построено из них с помощью предыдущего предложения, является типами.

Сложный тип — это тип функций от сущностей типа к сущностям типа . Таким образом, есть типы, подобные которым интерпретируются как элементы множества функций от сущностей к истинностным значениям, т. е. индикаторные функции множеств сущностей. Выражение типа — это функция от множеств сущностей к истинностным значениям, т. е. (индикаторная функция) множества множеств. Этот последний тип стандартно принимается за тип квантификаторов естественного языка , как everyone или nobody ( Montague 1973, Barwise and Cooper 1981). ^[10] ${\displaystyle \langle a,b\rangle }$ ${\displaystyle a}$ ${\displaystyle b}$ ${\displaystyle \langle e,t\rangle }$ ${\displaystyle \langle \langle e,t\rangle ,t\rangle }$

Теория типов с записями — это формальная структура представления семантики , использующая записи для выражения типов теории типов . Она использовалась в обработке естественного языка , в основном в вычислительной семантике и диалоговых системах . ^{[11] [12]}

Социальные науки

Грегори Бейтсон ввел теорию логических типов в социальные науки; его представления о двойном послании и логических уровнях основаны на теории типов Рассела.

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

Теория типов — это математическая логика , то есть набор правил вывода , которые приводят к суждениям . Большинство логик имеют суждения, утверждающие « Предложение истинно» или « Формула является правильно сформированной формулой ». ^[13] Теория типов имеет суждения, которые определяют типы и назначают их набору формальных объектов, известных как термины. Термин и его тип часто записываются вместе как . ${\displaystyle \varphi }$ ${\displaystyle \varphi }$ ${\displaystyle \mathrm {term} :{\mathsf {type}}}$

Условия

Термин в логике рекурсивно определяется как константный символ , переменная или применение функции , где термин применяется к другому термину. Константные символы могут включать натуральное число , логическое значение и функции, такие как функция-преемник и условный оператор . Таким образом, некоторые термины могут быть , , , и . ${\displaystyle 0}$ ${\displaystyle \mathrm {true} }$ ${\displaystyle \mathrm {S} }$ ${\displaystyle \mathrm {if} }$ ${\displaystyle 0}$ ${\displaystyle (\mathrm {S} \,0)}$ ${\displaystyle (\mathrm {S} \,(\mathrm {S} \,0))}$ ${\displaystyle (\mathrm {if} \,\mathrm {true} \,0\,(\mathrm {S} \,0))}$

Суждения

Большинство теорий типов содержат 4 суждения:

• " это тип" ${\displaystyle T}$
• " является термином типа " ${\displaystyle t}$ ${\displaystyle T}$
• "Тип равен типу " ${\displaystyle T_{1}}$ ${\displaystyle T_{2}}$
• «Условия и оба типа равны» ${\displaystyle t_{1}}$ ${\displaystyle t_{2}}$ ${\displaystyle T}$

Суждения могут следовать из предположений. Например, можно сказать «предполагая, что является термином типа и является термином типа , следует, что является термином типа ». Такие суждения формально записываются с символом турникета . ${\displaystyle x}$ ${\displaystyle {\mathsf {bool}}}$ ${\displaystyle y}$ ${\displaystyle {\mathsf {nat}}}$ ${\displaystyle (\mathrm {if} \,x\,y\,y)}$ ${\displaystyle {\mathsf {nat}}}$ ${\displaystyle \vdash }$

${\displaystyle x:{\mathsf {bool}},y:{\mathsf {nat}}\vdash ({\textrm {if}}\,x\,y\,y):{\mathsf {nat}}}$

Если нет никаких предположений, то слева от турникета ничего не будет.

${\displaystyle \vdash \mathrm {S} :{\mathsf {nat}}\to {\mathsf {nat}}}$

Список предположений слева — это контекст суждения. Заглавные греческие буквы, такие как и , являются обычным выбором для представления некоторых или всех предположений. Таким образом, 4 различных суждения обычно записываются следующим образом. ${\displaystyle \Gamma }$ ${\displaystyle \Delta }$

В некоторых учебниках используется тройной знак равенства, чтобы подчеркнуть, что это оценочное равенство и, таким образом, внешнее понятие равенства. ^[14] Суждения навязывают, что каждый термин имеет тип. Тип будет ограничивать, какие правила могут быть применены к термину. ${\displaystyle \equiv }$

Правила вывода

Правила вывода теории типов говорят, какие суждения могут быть сделаны на основе существования других суждений. Правила выражаются как вывод в стиле Генцена с использованием горизонтальной линии, с требуемыми входными суждениями над линией и результирующим суждением под линией. ^[15] Например, следующее правило вывода устанавливает правило подстановки для суждения равенства. Правила являются синтаксическими и работают путем переписывания . Метапеременные , , , , и могут фактически состоять из сложных терминов и типов, которые содержат множество применений функций, а не только отдельные символы. $${\displaystyle {\begin{array}{c}\Gamma \vdash t:T_{1}\qquad \Delta \vdash T_{1}=T_{2}\\\hline \Gamma ,\Delta \vdash t:T_{2}\end{array}}}$$ ${\displaystyle \Gamma }$ ${\displaystyle \Delta }$ ${\displaystyle t}$ ${\displaystyle T_{1}}$ ${\displaystyle T_{2}}$

Чтобы сгенерировать определенное суждение в теории типов, должно быть правило для его генерации, а также правила для генерации всех требуемых входных данных этого правила и т. д. Применяемые правила образуют дерево доказательств , где самые верхние правила не нуждаются в предположениях. Одним из примеров правила, которое не требует никаких входных данных, является правило, которое устанавливает тип постоянного термина. Например, чтобы утверждать, что существует термин типа , можно написать следующее. ${\displaystyle 0}$ ${\displaystyle {\mathsf {nat}}}$ $${\displaystyle {\begin{array}{c}\hline \vdash 0:nat\\\end{array}}}$$

Тип обитания

Как правило, желаемым заключением доказательства в теории типов является заключение о заселении типа . ^[16] Проблема принятия решения о заселении типа (сокращенно ) такова: ${\displaystyle \exists t.\Gamma \vdash t:\tau ?}$

Учитывая контекст и тип , решите, существует ли термин , которому можно присвоить тип в среде типа . ${\displaystyle \Gamma }$ ${\displaystyle \tau }$ ${\displaystyle t}$ ${\displaystyle \tau }$ ${\displaystyle \Gamma }$

Парадокс Жирара показывает, что обитаемость типа тесно связана с согласованностью системы типов с соответствием Карри–Ховарда. Чтобы быть надежной, такая система должна иметь необитаемые типы.

Теория типов обычно имеет несколько правил, включая следующие:

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

Также для каждого типа «по правилу» существует 4 различных вида правил

• Правила «формирования типа» говорят, как создать тип
• Правила «введения терминов» определяют канонические термины и функции-конструкторы, такие как «пара» и «S».
• Правила «исключения терминов» определяют другие функции, такие как «первая», «вторая» и «R».
• Правила «вычислений» определяют, как выполняются вычисления с использованием функций, специфичных для конкретного типа.

Заинтересованный читатель может ознакомиться с примерами правил в Приложении А.2 книги « Теория гомотопических типов» ^[14] или прочитать «Интуиционистскую теорию типов» Мартина-Лёфа ^{[17] .}

Подключения к фундаментам

Логическая структура теории типов имеет сходство с интуиционистской или конструктивной логикой. Формально теория типов часто упоминается как реализация интерпретации интуиционистской логики Брауэра–Гейтинга–Колмогорова . ^[17] Кроме того, можно установить связи с теорией категорий и компьютерными программами .

Интуиционистская логика

При использовании в качестве основы определенные типы интерпретируются как предложения (утверждения, которые могут быть доказаны), а термины, населяющие тип, интерпретируются как доказательства этого предложения. Когда некоторые типы интерпретируются как предложения, существует набор общих типов, которые могут быть использованы для их соединения с целью создания булевой алгебры из типов. Однако логика является не классической, а интуиционистской логикой , то есть в ней нет закона исключенного третьего или двойного отрицания .

В рамках этой интуиционистской интерпретации существуют общие типы, которые действуют как логические операторы:

Поскольку закон исключенного третьего не выполняется, то нет термина типа . Аналогично, двойное отрицание не выполняется, поэтому нет термина типа . ${\displaystyle \Pi a.A+(A\to \bot )}$ ${\displaystyle \Pi A.((A\to \bot )\to \bot )\to A}$

Можно включить закон исключенного третьего и двойного отрицания в теорию типов, по правилу или предположению. Однако термины могут не вычисляться до канонических терминов, и это будет мешать возможности определения, являются ли два термина оценочно равными друг другу. ^{[ необходима цитата ]}

Конструктивная математика

Пер Мартин-Лёф предложил свою интуиционистскую теорию типов в качестве основы для конструктивной математики . ^[13] Конструктивная математика требует, чтобы при доказательстве «существует со свойством » было построено частное и доказательство того, что оно имеет свойство . В теории типов существование достигается с помощью зависимого типа произведения, а его доказательство требует термина этого типа. ${\displaystyle x}$ ${\displaystyle P(x)}$ ${\displaystyle x}$ ${\displaystyle P}$

Примером неконструктивного доказательства является доказательство от противного . Первый шаг — предположение, что не существует, и опровержение этого от противного. Вывод из этого шага — «не существует того, что не существует». Последний шаг — это вывод с помощью двойного отрицания о существовании. Конструктивная математика не допускает последнего шага — устранения двойного отрицания, чтобы сделать вывод о существовании. ^[18] ${\displaystyle x}$ ${\displaystyle x}$ ${\displaystyle x}$ ${\displaystyle x}$

Большинство теорий типов, предложенных в качестве основ, являются конструктивными, и это включает в себя большинство теорий, используемых помощниками по доказательству. ^{[ требуется ссылка ]} К теории типов можно добавлять неконструктивные функции по правилу или предположению. К ним относятся операторы продолжений, такие как вызов с текущим продолжением . Однако эти операторы имеют тенденцию нарушать желаемые свойства, такие как каноничность и параметричность .

Переписка Карри-Ховарда

Соответствие Карри–Ховарда — это наблюдаемое сходство между логиками и языками программирования. Импликация в логике «A B» напоминает функцию из типа «A» в тип «B». Для различных логик правила похожи на выражения в типах языка программирования. Сходство идет дальше, поскольку применение правил похоже на программы в языках программирования. Таким образом, соответствие часто обобщается как «доказательства как программы». ${\displaystyle \to }$

Противопоставление терминов и типов можно также рассматривать как одно из имплементации и спецификации . С помощью синтеза программ (вычислительный аналог) обитание типов может быть использовано для построения (всех или частей) программ из спецификации, заданной в форме информации о типах. ^[19]

Вывод типа

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

Области исследований

Теория категорий

Основная статья: Теория категорий

Хотя первоначальная мотивация теории категорий была далека от фундаментализма, эти две области оказались глубоко связанными. Как пишет Джон Лейн Белл : «На самом деле категории сами по себе могут рассматриваться как теории типов определенного рода; один этот факт указывает на то, что теория типов гораздо более тесно связана с теорией категорий, чем с теорией множеств». Короче говоря, категорию можно рассматривать как теорию типов, рассматривая ее объекты как типы (или сорта), т. е. «Грубо говоря, категорию можно рассматривать как теорию типов, лишенную ее синтаксиса». Ряд важных результатов следует из этого: ^[20]

• Декартовы замкнутые категории соответствуют типизированному λ-исчислению ( Ламбек , 1970);
• C-моноиды (категории с произведениями и экспонентами и одним нетерминальным объектом) соответствуют нетипизированному λ-исчислению (независимо обнаруженному Ламбеком и Даной Скотт около 1980 года);
• локально декартовы замкнутые категории соответствуют теориям типа Мартина-Лёфа (Seely, 1984).

С тех пор это взаимодействие, известное как категориальная логика , стало предметом активных исследований; см., например, монографию Джейкобса (1999).

Теория гомотопического типа

Теория гомотопических типов пытается объединить теорию типов и теорию категорий. Она фокусируется на равенствах, особенно на равенствах между типами. Теория гомотопических типов отличается от интуиционистской теории типов в основном тем, как она обрабатывает тип равенства. В 2016 году была предложена кубическая теория типов, которая является теорией гомотопических типов с нормализацией. ^{[21] [22]}

Определения

Термины и типы

Атомарные термины

Самые основные типы называются атомами, а термин, тип которого является атомом, известен как атомный термин. Обычные атомные термины, включенные в теории типов, — это натуральные числа , часто обозначаемые типом , булевы логические значения ( / ), обозначаемые типом , и формальные переменные , тип которых может варьироваться. ^[16] Например, следующие могут быть атомарными терминами. ${\displaystyle {\mathsf {nat}}}$ ${\displaystyle \mathrm {true} }$ ${\displaystyle \mathrm {false} }$ ${\displaystyle {\mathsf {bool}}}$

• ${\displaystyle 42:{\mathsf {nat}}}$
• ${\displaystyle \mathrm {true} :{\mathsf {bool}}}$
• ${\displaystyle x:{\mathsf {nat}}}$
• ${\displaystyle y:{\mathsf {bool}}}$

Термины функции

В дополнение к атомарным термам большинство современных теорий типов также допускают функции . Типы функций вводят символ стрелки и определяются индуктивно : если и являются типами, то нотация представляет собой тип функции, которая принимает параметр типа и возвращает терм типа . Типы этой формы известны как простые типы . ^[16] ${\displaystyle \sigma }$ ${\displaystyle \tau }$ ${\displaystyle \sigma \to \tau }$ ${\displaystyle \sigma }$ ${\displaystyle \tau }$

Некоторые термины могут быть объявлены непосредственно как имеющие простой тип, например, следующий термин, который принимает два натуральных числа подряд и возвращает одно натуральное число. ${\displaystyle \mathrm {add} }$

${\displaystyle \mathrm {add} :{\mathsf {nat}}\to ({\mathsf {nat}}\to {\mathsf {nat}})}$

Строго говоря, простой тип допускает только один вход и один выход, поэтому более точным прочтением указанного выше типа будет то, что это функция, которая принимает натуральное число и возвращает функцию вида . Скобки поясняют, что не имеет типа , который был бы функцией, которая принимает функцию натуральных чисел и возвращает натуральное число. Соглашение заключается в том, что стрелка имеет правую ассоциативность , поэтому скобки можно опустить из типа . ^[16] ${\displaystyle \mathrm {add} }$ ${\displaystyle {\mathsf {nat}}\to {\mathsf {nat}}}$ ${\displaystyle \mathrm {add} }$ ${\displaystyle ({\mathsf {nat}}\to {\mathsf {nat}})\to {\mathsf {nat}}}$ ${\displaystyle \mathrm {add} }$

Лямбда-термины

Новые функциональные термы могут быть построены с использованием лямбда-выражений и называются лямбда-термами. Эти термы также определяются индуктивно: лямбда-терм имеет форму , где — формальная переменная, а — терм, а его тип обозначается как , где — тип , а — тип . ^[16] Следующий лямбда-терм представляет функцию, которая удваивает входное натуральное число. ${\displaystyle (\lambda v.t)}$ ${\displaystyle v}$ ${\displaystyle t}$ ${\displaystyle \sigma \to \tau }$ ${\displaystyle \sigma }$ ${\displaystyle v}$ ${\displaystyle \tau }$ ${\displaystyle t}$

${\displaystyle (\lambda x.\mathrm {add} \,x\,x):{\mathsf {nat}}\to {\mathsf {nat}}}$

Переменная есть и (подразумевается из типа лямбда-терма) должна иметь тип . Терм имеет тип , что видно из применения правила вывода применения функции дважды. Таким образом, лямбда-терм имеет тип , что означает, что это функция, принимающая натуральное число в качестве аргумента и возвращающая натуральное число. ${\displaystyle x}$ ${\displaystyle {\mathsf {nat}}}$ ${\displaystyle \mathrm {add} \,x\,x}$ ${\displaystyle {\mathsf {nat}}}$ ${\displaystyle {\mathsf {nat}}\to {\mathsf {nat}}}$

Лямбда-терм часто называют ^[d] анонимной функцией, поскольку у него нет имени. Концепция анонимных функций появляется во многих языках программирования.

Правила вывода

Применение функции

Сила теорий типов заключается в определении того, как термины могут быть объединены посредством правил вывода . ^[4] Теории типов, которые имеют функции, также имеют правило вывода применения функции : если является термином типа , и является термином типа , то применение к , часто записываемое , имеет тип . Например, если известны обозначения типов , , и , то из применения функции можно вывести следующие обозначения типов . ^[16] ${\displaystyle t}$ ${\displaystyle \sigma \to \tau }$ ${\displaystyle s}$ ${\displaystyle \sigma }$ ${\displaystyle t}$ ${\displaystyle s}$ ${\displaystyle (t\,s)}$ ${\displaystyle \tau }$ ${\displaystyle 0:{\textsf {nat}}}$ ${\displaystyle 1:{\textsf {nat}}}$ ${\displaystyle 2:{\textsf {nat}}}$

• ${\displaystyle (\mathrm {add} \,1):{\textsf {nat}}\to {\textsf {nat}}}$
• ${\displaystyle ((\mathrm {add} \,2)\,0):{\textsf {nat}}}$
• ${\displaystyle ((\mathrm {add} \,1)((\mathrm {add} \,2)\,0)):{\textsf {nat}}}$

Скобки указывают порядок операций ; однако, по соглашению, применение функции является левоассоциативным , поэтому скобки можно опустить, где это уместно. ^[16] В случае трех приведенных выше примеров все скобки можно опустить в первых двух, а третий можно упростить до . ${\displaystyle \mathrm {add} \,1\,(\mathrm {add} \,2\,0):{\textsf {nat}}}$

Скидки

Теории типов, которые допускают лямбда-термины, также включают правила вывода, известные как -редукция и -редукция. Они обобщают понятие применения функции к лямбда-терминам. Символически они записываются ${\displaystyle \beta }$ ${\displaystyle \eta }$

• ${\displaystyle (\lambda v.t)\,s\rightarrow t[v\colon =s]}$( -снижение). ${\displaystyle \beta }$
• ${\displaystyle (\lambda v.t\,v)\rightarrow t}$, если не является свободной переменной в ( -редукции). ${\displaystyle v}$ ${\displaystyle t}$ ${\displaystyle \eta }$

Первая редукция описывает, как вычислить лямбда-терм: если лямбда-выражение применяется к терму , то каждое вхождение в заменяется на . Вторая редукция делает явной связь между лямбда-выражениями и типами функций: если является лямбда-термом, то должно быть , что является функциональным термом, поскольку он применяется к . Таким образом, лямбда-выражение эквивалентно просто , так как оба принимают один аргумент и применяются к нему. ^[4] ${\displaystyle (\lambda v.t)}$ ${\displaystyle s}$ ${\displaystyle v}$ ${\displaystyle t}$ ${\displaystyle s}$ ${\displaystyle (\lambda v.t\,v)}$ ${\displaystyle t}$ ${\displaystyle v}$ ${\displaystyle t}$ ${\displaystyle t}$

Например, следующий термин может быть сокращен. ${\displaystyle \beta }$

${\displaystyle (\lambda x.\mathrm {add} \,x\,x)\,2\rightarrow \mathrm {add} \,2\,2}$

В теориях типов, которые также устанавливают понятия равенства для типов и терминов, существуют соответствующие правила вывода -равенства и -равенства. ^[16] ${\displaystyle \beta }$ ${\displaystyle \eta }$

Общие термины и типы

Пустой тип

Пустой тип не имеет терминов. Тип обычно записывается или . Одним из применений пустого типа является доказательство обитаемости типа . Если для типа непротиворечиво вывести функцию типа , то является необитаемым , то есть он не имеет терминов. ${\displaystyle \bot }$ ${\displaystyle \mathbb {0} }$ ${\displaystyle a}$ ${\displaystyle a\to \bot }$ ${\displaystyle a}$

Тип устройства

Тип единицы имеет ровно 1 канонический терм. Тип записывается или и единственный канонический терм записывается . Тип единицы также используется в доказательствах типа inhabitation. Если для типа , последовательно вывести функцию типа , то inhabited , то есть он должен иметь один или несколько термов. ${\displaystyle \top }$ ${\displaystyle \mathbb {1} }$ ${\displaystyle \ast }$ ${\displaystyle a}$ ${\displaystyle \top \to a}$ ${\displaystyle a}$

Булев тип

Тип Boolean имеет ровно 2 канонических термина. Тип обычно записывается как или или . Канонические термины обычно и . ${\displaystyle {\textsf {bool}}}$ ${\displaystyle \mathbb {B} }$ ${\displaystyle \mathbb {2} }$ ${\displaystyle \mathrm {true} }$ ${\displaystyle \mathrm {false} }$

Натуральные числа

Натуральные числа обычно реализуются в стиле арифметики Пеано . Существует канонический термин для нуля. Канонические значения больше нуля используют итеративные применения функции- последователя . ${\displaystyle 0:{\mathsf {nat}}}$ ${\displaystyle \mathrm {S} :{\mathsf {nat}}\to {\mathsf {nat}}}$

Зависимая типизация

Некоторые теории типов допускают зависимость типов сложных терминов, таких как функции или списки, от типов их аргументов. Например, теория типов может иметь зависимый тип , который должен соответствовать спискам терминов, где каждый термин должен иметь тип . В этом случае имеет тип , где обозначает универсум всех типов в теории. ${\displaystyle {\mathsf {list}}\,a}$ ${\displaystyle a}$ ${\displaystyle {\mathsf {list}}}$ ${\displaystyle U\to U}$ ${\displaystyle U}$

Некоторые теории также позволяют типам зависеть от терминов вместо типов. Например, теория может иметь тип , где — термин типа, кодирующий длину вектора . Это обеспечивает большую специфичность и безопасность типов : функции с ограничениями длины вектора или требованиями соответствия длины, такие как скалярное произведение , могут кодировать это требование как часть типа. ^[24] ${\displaystyle {\mathsf {vector}}\,n}$ ${\displaystyle n}$ ${\displaystyle {\mathsf {nat}}}$

Существуют фундаментальные проблемы, которые могут возникнуть из-за зависимых типов, если теория не осторожна с тем, какие зависимости разрешены, например, парадокс Жирара . Логик Хенк Барендегт представил лямбда-куб как основу для изучения различных ограничений и уровней зависимой типизации. ^[25]

Тип продукта

Тип продукта зависит от двух типов, и его термины обычно записываются в виде упорядоченных пар или с символом . Пара имеет тип продукта , где — тип , а — тип . Тип продукта обычно определяется с помощью функций исключения и . ${\displaystyle (s,t)}$ ${\displaystyle \times }$ ${\displaystyle (s,t)}$ ${\displaystyle \sigma \times \tau }$ ${\displaystyle \sigma }$ ${\displaystyle s}$ ${\displaystyle \tau }$ ${\displaystyle t}$ ${\displaystyle \mathrm {first} :(\Pi \,\sigma \,\tau .\sigma \times \tau \to \sigma )}$ ${\displaystyle \mathrm {second} :(\Pi \,\sigma \,\tau .\sigma \times \tau \to \tau )}$

• ${\displaystyle \mathrm {first} \,(s,t)}$возвращается , и ${\displaystyle s}$
• ${\displaystyle \mathrm {second} \,(s,t)}$возвращается . ${\displaystyle t}$

Помимо упорядоченных пар, этот тип используется для понятий логического соединения и пересечения .

Тип суммы

Тип суммы зависит от двух типов и обычно обозначается символом или . В языках программирования типы суммы могут называться помеченными объединениями . Тип обычно определяется с помощью конструкторов и , которые являются инъективными , и функции элиминатора, такой что ${\displaystyle +}$ ${\displaystyle \sqcup }$ ${\displaystyle \sigma \sqcup \tau }$ ${\displaystyle \mathrm {left} :\sigma \to (\sigma \sqcup \tau )}$ ${\displaystyle \mathrm {right} :\tau \to (\sigma \sqcup \tau )}$ ${\displaystyle \mathrm {match} :(\Pi \,\rho .(\sigma \to \rho )\to (\tau \to \rho )\to (\sigma \sqcup \tau )\to \rho )}$

• ${\displaystyle \mathrm {match} \,f\,g\,(\mathrm {left} \,x)}$возвращается , и ${\displaystyle f\,x}$
• ${\displaystyle \mathrm {match} \,f\,g\,(\mathrm {right} \,y)}$возвращается . ${\displaystyle g\,y}$

Тип суммы используется для понятий логической дизъюнкции и объединения .

Зависимые произведения и суммы

Два общих типа зависимости , типы зависимого произведения и зависимой суммы, позволяют теории кодировать интуиционистскую логику BHK , действуя как эквиваленты универсальной и экзистенциальной квантификации ; это формализовано соответствием Карри–Ховарда . ^[24] Поскольку они также связаны с произведениями и суммами в теории множеств , они часто записываются с помощью символов и , соответственно. ^[17] Типы зависимого произведения и суммы обычно появляются в типах функций и часто включаются в языки программирования. ^[26] ${\displaystyle \Pi }$ ${\displaystyle \Sigma }$

Например, рассмотрим функцию , которая принимает a и терм типа и возвращает список с элементом в конце. Аннотацией типа такой функции будет , что можно прочитать как «для любого типа , передать a и an , и вернуть a ». ${\displaystyle \mathrm {append} }$ ${\displaystyle {\mathsf {list}}\,a}$ ${\displaystyle a}$ ${\displaystyle \mathrm {append} :(\Pi \,a.{\mathsf {list}}\,a\to a\to {\mathsf {list}}\,a)}$ ${\displaystyle a}$ ${\displaystyle {\mathsf {list}}\,a}$ ${\displaystyle a}$ ${\displaystyle {\mathsf {list}}\,a}$

Типы сумм встречаются в зависимых парах , где второй тип зависит от значения первого члена. Это естественным образом возникает в информатике, где функции могут возвращать различные типы выходных данных в зависимости от входных данных. Например, тип Boolean обычно определяется с помощью функции-элиминатора , которая принимает три аргумента и ведет себя следующим образом. ${\displaystyle \mathrm {if} }$

• ${\displaystyle \mathrm {if} \,\mathrm {true} \,x\,y}$возвращается , и ${\displaystyle x}$
• ${\displaystyle \mathrm {if} \,\mathrm {false} \,x\,y}$возвращается . ${\displaystyle y}$

Возвращаемый тип этой функции зависит от ее ввода. Если теория типов допускает зависимые типы, то можно определить функцию так, что ${\displaystyle {\mathsf {bool}}}$ ${\displaystyle \mathrm {TF} \colon {\mathsf {bool}}\to U\to U\to U}$

• ${\displaystyle \mathrm {TF} \,\mathrm {true} \,\sigma \,\tau }$возвращается , и ${\displaystyle \sigma }$
• ${\displaystyle \mathrm {TF} \,\mathrm {false} \,\sigma \,\tau }$возвращается . ${\displaystyle \tau }$

Тогда тип может быть записан как . ${\displaystyle \mathrm {if} }$ ${\displaystyle (\Pi \,\sigma \,\tau .{\mathsf {bool}}\to \sigma \to \tau \to (\Sigma \,x:{\textsf {bool}}.\mathrm {TF} \,x\,\sigma \,\tau ))}$

Тип личности

Следуя идее соответствия Карри-Ховарда, тип тождества — это тип, введенный для отражения пропозициональной эквивалентности , в отличие от оценочной (синтаксической) эквивалентности , которую уже обеспечивает теория типов.

Тип идентичности требует двух терминов одного типа и записывается с помощью символа . Например, если и являются терминами, то является возможным типом. Канонические термины создаются с помощью функции рефлексивности, . Для термина вызов возвращает канонический термин, населяющий тип . ${\displaystyle =}$ ${\displaystyle x+1}$ ${\displaystyle 1+x}$ ${\displaystyle x+1=1+x}$ ${\displaystyle \mathrm {refl} }$ ${\displaystyle t}$ ${\displaystyle \mathrm {refl} \,t}$ ${\displaystyle t=t}$

Сложность равенства в теории типов делает его активной темой исследований; гомотопическая теория типов является заметной областью исследований, которая в основном занимается равенством в теории типов.

Индуктивные типы

Индуктивные типы являются общим шаблоном для создания большого разнообразия типов. Фактически, все типы, описанные выше, и другие могут быть определены с использованием правил индуктивных типов. Два метода создания индуктивных типов — это индукция-рекурсия и индукция-индукция . Метод, который использует только лямбда-термины — это кодирование Скотта .

Некоторые помощники доказательства , такие как Coq и Lean , основаны на исчислении индуктивных конструкций, которое представляет собой исчисление конструкций с индуктивными типами.

Отличия от теории множеств

Наиболее общепринятой основой математики является логика первого порядка с языком и аксиомами теории множеств Цермело–Френкеля с аксиомой выбора , сокращенно ZFC. Теории типов, имеющие достаточную выразительность , также могут выступать в качестве основы математики. Между этими двумя подходами есть ряд различий.

• Теория множеств имеет как правила , так и аксиомы , тогда как теории типов имеют только правила. Теории типов, в общем, не имеют аксиом и определяются своими правилами вывода. ^[14]
• Классическая теория множеств и логика имеют закон исключенного третьего . Когда теория типов кодирует понятия «и» и «или» как типы, это приводит к интуиционистской логике и не обязательно имеет закон исключенного третьего. ^[17]
• В теории множеств элемент не ограничен одним множеством. Элемент может появляться в подмножествах и объединениях с другими множествами. В теории типов термины (как правило) принадлежат только одному типу. Там, где будет использоваться подмножество, теория типов может использовать функцию предиката или использовать зависимо типизированный тип продукта, где каждый элемент сопряжен с доказательством того, что свойство подмножества выполняется для . Там, где будет использоваться объединение, теория типов использует тип суммы, который содержит новые канонические термины. ${\displaystyle x}$ ${\displaystyle x}$
• Теория типов имеет встроенное понятие вычисления. Таким образом, «1+1» и «2» являются разными терминами в теории типов, но они вычисляются с одним и тем же значением. Более того, функции вычислительно определяются как лямбда-термины. В теории множеств «1+1=2» означает, что «1+1» — это просто другой способ сослаться на значение «2». Вычисление теории типов требует сложной концепции равенства.
• Теория множеств кодирует числа как множества . Теория типов может кодировать числа как функции, используя кодировку Чёрча , или, что более естественно, как индуктивные типы , и эта конструкция очень напоминает аксиомы Пеано .
• В теории типов доказательства являются типами, тогда как в теории множеств доказательства являются частью базовой логики первого порядка. ^[14]

Сторонники теории типов также укажут на ее связь с конструктивной математикой через интерпретацию BHK , на ее связь с логикой посредством изоморфизма Карри–Ховарда и на ее связь с теорией категорий .

Свойства теорий типов

Термины обычно принадлежат к одному типу. Однако существуют теории множеств, определяющие «подтипирование».

Вычисление происходит путем повторного применения правил. Многие типы теорий являются строго нормализующими , что означает, что любой порядок применения правил всегда приведет к одному и тому же результату. Однако некоторые — нет. В теории нормализующего типа однонаправленные правила вычисления называются «правилами редукции», а применение правил «редуцирует» термин. Если правило не является однонаправленным, оно называется «правилом преобразования».

Некоторые комбинации типов эквивалентны другим комбинациям типов. Когда функции рассматриваются как «возведение в степень», комбинации типов могут быть записаны аналогично алгебраическим тождествам. ^[26] Таким образом, , , , , . ${\displaystyle {\mathbb {0} }+A\cong A}$ ${\displaystyle {\mathbb {1} }\times A\cong A}$ ${\displaystyle {\mathbb {1} }+{\mathbb {1} }\cong {\mathbb {2} }}$ ${\displaystyle A^{B+C}\cong A^{B}\times A^{C}}$ ${\displaystyle A^{B\times C}\cong (A^{B})^{C}}$

Аксиомы

Большинство теорий типов не имеют аксиом . Это происходит потому, что теория типов определяется своими правилами вывода. Это источник путаницы для людей, знакомых с теорией множеств, где теория определяется как правилами вывода для логики (например, логики первого порядка ), так и аксиомами о множествах.

Иногда теория типов добавляет несколько аксиом. Аксиома — это суждение, которое принимается без вывода с использованием правил вывода. Они часто добавляются для обеспечения свойств, которые не могут быть добавлены чисто через правила.

Аксиомы могут вызывать проблемы, если они вводят термины без способа вычисления этих терминов. То есть, аксиомы могут мешать нормализующему свойству теории типов. ^[27]

Вот некоторые часто встречающиеся аксиомы:

• «Аксиома К» обеспечивает «единственность доказательств тождества». То есть, каждый член типа тождества равен рефлексивности. ^[28]
• "Аксиома унивалентности" утверждает, что эквивалентность типов есть равенство типов. Исследование этого свойства привело к кубической теории типов, где свойство выполняется без необходимости в аксиоме. ^[22]
• «Закон исключенного третьего» часто добавляется для того, чтобы удовлетворить пользователей, которым нужна классическая логика вместо интуиционистской.

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

Список теорий типов

Главный

• Простое типизированное лямбда-исчисление , представляющее собой логику высшего порядка
• интуиционистская теория типа
• система F
• LF часто используется для определения других теорий типов.
• исчисление конструкций и его производные

Незначительный

• Автомат
• теория типа ST
• UTT (Единая теория зависимых типов Луо)
• некоторые формы комбинаторной логики
• другие, определенные в лямбда-кубе (также известные как системы чистого типа )
• другие под названием типизированное лямбда-исчисление

Активные исследования

• Теория гомотопических типов исследует равенство типов
• Теория кубических типов — это реализация теории гомотопических типов.

Смотрите также

• Класс (теория множеств)
• Логика
• Различие типа и токена

Дальнейшее чтение

• Аартс, К.; Бэкхаус, Р.; Хугендейк, П.; Верманс, Э.; ван дер Вауде, Дж. (декабрь 1992 г.). «Реляционная теория типов данных». Технический университет Эйндховена.
• Эндрюс Б., Питер (2002). Введение в математическую логику и теорию типов: к истине через доказательство (2-е изд.). Kluwer. ISBN 978-1-4020-0763-7.
• Якобс, Барт (1999). Категориальная логика и теория типов. Исследования по логике и основаниям математики. Т. 141. Elsevier. ISBN 978-0-444-50170-7. Архивировано из оригинала 2023-08-10 . Получено 2020-07-19 .Подробно рассматривает теорию типов, включая полиморфные и зависимые расширения типов. Дает категориальную семантику .
• Cardelli, Luca (1996). «Системы типов». В Tucker, Allen B. (ред.). The Computer Science and Engineering Handbook . CRC Press. стр. 2208–36. ISBN 9780849329098. Архивировано из оригинала 2008-04-10 . Получено 2004-06-26 .
• Коллинз, Джордан Э. (2012). История теории типов: развитие после второго издания «Principia Mathematica». Lambert Academic Publishing. hdl :11375/12315. ISBN 978-3-8473-2963-3.Содержит исторический обзор развития теории типов с акцентом на упадок этой теории как основы математики за четыре десятилетия после публикации второго издания «Principia Mathematica».
• Констебль, Роберт Л. (2012) [2002]. "Наивная вычислительная теория типов" (PDF) . В Швихтенберг, Х.; Штайнбрюгген, Р. (ред.). Доказательство и надежность системы . Серия научных трудов НАТО II. Том 62. Springer. С. 213–259. ISBN 9789401004138. Архивировано (PDF) из оригинала 2022-10-09.Задуман как аналог теории типов наивной теории множеств Пола Халмоша (1960).
• Кокванд, Тьерри (2018) [2006]. «Теория типов». Стэнфордская энциклопедия философии .
• Томпсон, Саймон (1991). Теория типов и функциональное программирование. Эддисон–Уэсли. ISBN 0-201-41667-0. Архивировано из оригинала 2021-03-23 ​​. Получено 2006-04-03 .
• Hindley, J. Roger (2008) [1995]. Базовая теория простых типов . Cambridge University Press. ISBN 978-0-521-05422-5.Хорошее введение в простую теорию типов для компьютерных специалистов; хотя описанная система не совсем STT Чёрча. Обзор книги Архивировано 2011-06-07 в Wayback Machine
• Камареддин, Файруз Д.; Лаан, Тван; Недерпелт, Роб П. (2004). Современный взгляд на теорию типов: от истоков до наших дней . Springer. ISBN 1-4020-2334-0.
• Феррейрос, Хосе; Домингес, Хосе Феррейрос (2007). «X. Логика и теория типов в межвоенный период». Лабиринт мысли: история теории множеств и ее роль в современной математике (2-е изд.). Спрингер. ISBN 978-3-7643-8349-7.
• Laan, TDL (1997). Эволюция теории типов в логике и математике (PDF) (PhD). Технический университет Эйндховена. doi :10.6100/IR498552. ISBN 90-386-0531-5. Архивировано (PDF) из оригинала 2022-10-09.
• Монтегю, Р. (1973) «Правильная обработка квантификации в обычном английском языке». В KJJ Hintikka, JME Moravcsik и P. Suppes (ред.), Approaches to Natural Language (Synthese Library, 49), Dordrecht: Reidel, 221–242; перепечатано в Portner and Partee (ред.) 2002, стр. 17–35. См.: Montague Semantics, Stanford Encyclopedia of Philosophy.

Примечания

1. См. § Термины и типы
2. В системе типов Julia , например, абстрактные типы не имеют экземпляров, но могут иметь подтип, ^{[1] : 110,} тогда как конкретные типы не имеют подтипов, но могут иметь экземпляры, для « документирования, оптимизации и диспетчеризации ». ^[2]
3. Чёрч продемонстрировал свой логистический метод с помощью своей простой теории типов ^[4] и объяснил свой метод в 1956 году ^[5] на страницах 47-68.
4. В Julia , например, функция без имени, но с двумя параметрами в некотором кортеже (x,y) может быть обозначена, скажем, (x,y) -> x^5+yкак анонимная функция. ^[23]

Ссылки

1. Балберт, Иво (2015) Начало работы с программированием Julia ISBN 978-1-78328-479-5
2. docs.julialang.org v.1 Типы Архивировано 24.03.2022 на Wayback Machine
3. Стэнфордская энциклопедия философии (ред. Пн., 12 октября 2020 г.) Парадокс Рассела Архивировано 18 декабря 2021 г. на Wayback Machine 3. Ранние ответы на парадокс
4. Чёрч, Алонзо (1940). «Формулировка простой теории типов». Журнал символической логики . 5 (2): 56–68. doi :10.2307/2266170. JSTOR  2266170. S2CID  15889861.
5. Алонзо Чёрч (1956) Введение в математическую логику Том 1
6. ETCS в n Lab
7. Chatzikyriakidis, Stergios; Luo, Zhaohui (2017-02-07). Современные перспективы в теоретико-типовой семантике. Springer. ISBN 978-3-319-50422-3. Архивировано из оригинала 2023-08-10 . Получено 2022-07-29 .
8. Винтер, Йоад (2016-04-08). Элементы формальной семантики: Введение в математическую теорию значения естественного языка. Издательство Эдинбургского университета. ISBN 978-0-7486-7777-1. Архивировано из оригинала 2023-08-10 . Получено 2022-07-29 .
9. Купер, Робин. «Теория типов и семантика в движении. Архивировано 10 мая 2022 г. в Wayback Machine ». Справочник по философии науки 14 (2012): 271-323.
10. Барвайз, Джон; Купер, Робин (1981) Обобщенные квантификаторы и естественный язык Лингвистика и философия 4 (2):159--219 (1981)
11. Купер, Робин (2005). «Записи и типы записей в семантической теории». Журнал логики и вычислений . 15 (2): 99–112. doi :10.1093/logcom/exi004.
12. Купер, Робин (2010). Теория типов и семантика в движении . Справочник по философии науки. Том 14: Философия лингвистики . Elsevier.
13. Martin-Löf, Per (1 декабря 1987 г.). «Истина предложения, очевидность суждения, действительность доказательства». Synthese . 73 (3): 407–420. doi :10.1007/BF00484985. ISSN  1573-0964.
14. Программа унивалентных оснований (2013). Теория гомотопических типов: унивалентные основания математики. Теория гомотопических типов.
15. Смит, Питер. "Типы систем доказательств" (PDF) . logicmatters.net . Архивировано (PDF) из оригинала 2022-10-09 . Получено 29 декабря 2021 .
16. Хенк Барендрегт; Уил Деккерс; Ричард Стэтман (20 июня 2013 г.). Лямбда-исчисление с типами. Издательство Кембриджского университета. стр. 1–66. ISBN 978-0-521-76614-2.
17. "Правила интуиционистской теории типов Мартина-Лёфа" (PDF) . Архивировано (PDF) из оригинала 2021-10-21 . Получено 2022-01-22 .
18. "доказательство от противного". nlab . Архивировано из оригинала 13 августа 2023 . Получено 29 декабря 2021 .
19. Хайнеман, Джордж Т.; Бессай, Ян; Дюддер, Борис; Рехоф, Якоб (2016). «Долгая и извилистая дорога к модульному синтезу». Использование формальных методов, верификации и валидации: основные методы . ISoLA 2016. Конспект лекций по информатике. Том 9952. Springer. С. 303–317. doi :10.1007/978-3-319-47166-2_21. ISBN 978-3-319-47165-5.
20. Белл, Джон Л. (2012). "Типы, множества и категории" (PDF) . В Канамори, Акихиро (ред.). Множества и расширения в двадцатом веке . Справочник по истории логики. Том 6. Elsevier. ISBN 978-0-08-093066-4. Архивировано (PDF) из оригинала 2018-04-17 . Получено 2012-11-03 .
21. Стерлинг, Джонатан; Анджиули, Карло (2021-06-29). «Нормализация для теории кубических типов». 36-й ежегодный симпозиум ACM/IEEE по логике в компьютерных науках (LICS) 2021 года . Рим, Италия: IEEE. стр. 1–15. arXiv : 2101.11479 . doi :10.1109/LICS52264.2021.9470719. ISBN 978-1-6654-4895-6. S2CID  231719089. Архивировано из оригинала 2023-08-13 . Получено 2022-06-21 .
22. Cohen, Cyril; Coquand, Thierry; Huber, Simon; Mörtberg, Anders (2016). "Cubical Type Theory: A constructive interpretation of the univalence axiom" (PDF) . 21st International Conference on Types for Proofs and Programs (TYPES 2015) . arXiv : 1611.02108 . doi : 10.4230/LIPIcs.CVIT.2016.23 (неактивен 1 ноября 2024 г.). Архивировано (PDF) из оригинала 2022-10-09.{{cite journal}}: CS1 maint: DOI inactive as of November 2024 (link)
23. Балберт, Иво (2015) Начало работы с Джулией
24. Bove, Ana; Dybjer, Peter (2009), Bove, Ana; Barbosa, Luís Soares; Pardo, Alberto; Pinto, Jorge Sousa (ред.), "Dependent Types at Work", Language Engineering and Rigorous Software Development: International LerNet ALFA Summer School 2008, Пириаполис, Уругвай, 24 февраля - 1 марта 2008 г., Revised Tutorial Lectures , Lecture Notes in Computer Science, Берлин, Гейдельберг: Springer, стр. 57–99, doi :10.1007/978-3-642-03153-3_2, ISBN 978-3-642-03153-3, получено 2024-01-18
25. Барендегт, Хенк (апрель 1991 г.). «Введение в обобщенные системы типов». Журнал функционального программирования . 1 (2): 125–154. doi :10.1017/S0956796800020025. hdl : 2066/17240 – через Cambridge Core.
26. Milewski, Bartosz. "Programming with Math (Exploring Type Theory)". YouTube . Архивировано из оригинала 2022-01-22 . Получено 2022-01-22 .
27. "Аксиомы и вычисления". Доказательство теорем в Lean . Архивировано из оригинала 22 декабря 2021 г. Получено 21 января 2022 г.
28. "Axiom K". nLab . Архивировано из оригинала 2022-01-19 . Получено 2022-01-21 .

Внешние ссылки

Вводный материал

• Теория типов в nLab, где есть статьи по многим темам.
• Статья об интуиционистской теории типов в Стэнфордской энциклопедии философии
• Книга Хенка Барендрегта «Лямбда-исчисление с типами»
• Исчисление конструкций / Типизированная статья в стиле учебника по лямбда-исчислению, автор Хельмут Брандл
• Заметки по интуиционистской теории типов Пера Мартина-Лёфа
• Программирование в книге Мартина-Лёфа «Теория типов»
• Книга «Теория гомотопических типов», в которой в качестве математической основы предложена теория гомотопических типов.

Расширенный материал

• Роберт Л. Констебл (ред.). "Теория вычислительных типов". Scholarpedia .
• Форум TYPES — модерируемый e-mail-форум, посвященный теории типов в информатике, действующий с 1987 года.
• Книга Nuprl: «Введение в теорию типов».
• Типы проектов Конспекты лекций летних школ 2005–2008 гг.
  • В летней школе 2005 года пройдут вводные лекции
• Летняя школа языков программирования в Орегоне, много лекций и несколько заметок.
  • Лекции лета 2013 года, включая выступления Роберта Харпера на YouTube
  • Лето 2015 г. Типы, логика, семантика и проверка
• Блог Андрея Бауэра