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

Интуиционистская теория типов (также известная как конструктивная теория типов или теория типов Мартина-Лёфа ( MLTT )) — это теория типов и альтернативная основа математики . Интуиционистская теория типов была создана Пером Мартином-Лёфом , шведским математиком и философом , который впервые опубликовал её в 1972 году. Существует несколько версий теории типов: Мартин-Лёф предложил как интенсиональные , так и экстенсиональные варианты теории, а ранние импредикативные версии, несовместимые с парадоксом Жирара , уступили место предикативным версиям. Однако все версии сохраняют основную конструкцию конструктивной логики, использующей зависимые типы .

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

Конструкторы типов интуиционистской теории типов были построены так, чтобы следовать взаимно-однозначному соответствию с логическими связками. Например, логическая связка, называемая импликацией ( ), соответствует типу функции ( ). Это соответствие называется изоморфизмом Карри–Ховарда . Предшествующие теории типов также следовали этому изоморфизму, но теория Мартина-Лёфа была первой, кто расширил его до логики предикатов , введя зависимые типы.${\displaystyle A\подразумевает B}$${\displaystyle A\to B}$

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

Если вы не знакомы с теорией типов и знаете теорию множеств, краткое резюме таково: типы содержат термины, как множества содержат элементы. Термины принадлежат одному и только одному типу. Термины, такие как и вычисляются («редуцируются») до канонических терминов, таких как 4. Подробнее см. статью о теории типов .${\displaystyle 2+2}$${\displaystyle 2\cdot 2}$

Существует три конечных типа: Тип 0 содержит 0 терминов. Тип 1 содержит 1 канонический термин. И тип 2 содержит 2 канонических термина.

Поскольку тип 0 содержит 0 терминов, его также называют пустым типом . Он используется для представления чего-либо, что не может существовать. Он также записывается и представляет что-либо недоказуемое. (То есть доказательство того, что не может существовать.) В результате отрицание определяется как функция к нему: .${\displaystyle \bot}$${\displaystyle \neg A:=A\to \bot }$

Аналогично, тип 1 содержит 1 канонический термин и представляет существование. Он также называется типом единицы .

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

Вместо этого предложения представлены определенными типами. Например, истинное предложение может быть представлено типом 1 , тогда как ложное предложение может быть представлено типом 0. Но мы не можем утверждать, что это единственные предложения, т. е. закон исключенного третьего не выполняется для предложений в интуиционистской теории типов.

Σ-типы содержат упорядоченные пары. Как и в случае с типичными упорядоченными парными (или 2-кортежными) типами, Σ-тип может описывать декартово произведение , , двух других типов и . Логически такая упорядоченная пара будет содержать доказательство и доказательство , поэтому такой тип можно увидеть записанным как .${\displaystyle A\times B}$${\displaystyle А}$${\displaystyle Б}$${\displaystyle А}$${\displaystyle Б}$${\displaystyle A\клин B}$

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

${\displaystyle \sum _{n{\mathbin {:}}{\mathbb {N} }}\operatorname {Vec} ({\mathbb {R} },n)}$

Используя терминологию теории множеств, это похоже на индексированное непересекающееся объединение множеств. В случае обычного декартова произведения тип второго члена не зависит от значения первого члена. Таким образом, тип, описывающий декартово произведение, записывается так:${\displaystyle {\mathbb {N} }\times {\mathbb {R} }}$

${\displaystyle \sum _{n{\mathbin {:}}{\mathbb {N} }}{\mathbb {R} }}$

Здесь важно отметить, что значение первого члена, , не зависит от типа второго члена, .${\displaystyle n}$${\displaystyle {\mathbb {R} }}$

Σ-типы могут использоваться для построения более длинных зависимо-типизированных кортежей, используемых в математике, а также записей или структур, используемых в большинстве языков программирования. Примером зависимо-типизированного 3-кортежа являются два целых числа и доказательство того, что первое целое число меньше второго целого числа, описываемое типом:

${\displaystyle \sum _{m{\mathbin {:}}{\mathbb {Z} }}{\sum _{n{\mathbin {:}}{\mathbb {Z} }}((m<n)={\text{Истина}})}}$

Зависимая типизация позволяет Σ-типам выполнять роль квантификатора существования . Утверждение «существует тип , такой что доказано» становится типом упорядоченных пар, где первый элемент является значением типа , а второй элемент является доказательством . Обратите внимание, что тип второго элемента (доказательства ) зависит от значения в первой части упорядоченной пары ( ). Его тип будет:${\displaystyle n}$${\displaystyle {\mathbb {N}}}$${\displaystyle P(n)}$${\displaystyle n}$${\displaystyle {\mathbb {N}}}$${\displaystyle P(n)}$${\displaystyle P(n)}$${\displaystyle n}$

${\ displaystyle \ sum _ {n {\ mathbin {:} {\ mathbb {N} }} P (n)}$

Π-типы содержат функции. Как и типичные типы функций, они состоят из входного типа и выходного типа. Однако они мощнее типичных типов функций, поскольку возвращаемый тип может зависеть от входного значения. Функции в теории типов отличаются от теории множеств. В теории множеств вы ищете значение аргумента в наборе упорядоченных пар. В теории типов аргумент подставляется в терм, а затем к терму применяется вычисление («редукция»).

В качестве примера, тип функции, которая, учитывая натуральное число , возвращает вектор, содержащий действительные числа, записывается так:${\displaystyle n}$${\displaystyle n}$

${\displaystyle \prod _{n{\mathbin {:}}{\mathbb {N} }}\operatorname {Vec} ({\mathbb {R} },n)}$

Когда тип вывода не зависит от входного значения, тип функции часто просто записывается с помощью . Таким образом, — это тип функций от натуральных чисел до действительных чисел. Такие Π-типы соответствуют логической импликации. Логическое предложение соответствует типу , содержащему функции, которые принимают доказательства A и возвращают доказательства B. Этот тип можно было бы записать более последовательно как:${\displaystyle \to}$${\displaystyle {\mathbb {N} }\to {\mathbb {R} }}$${\displaystyle A\подразумевает B}$${\displaystyle A\to B}$

${\displaystyle \prod _{a{\mathbin {:}}A}B}$

Π-типы также используются в логике для всеобщей квантификации . Утверждение «для каждого типа , доказано» становится функцией от типа до доказательств . Таким образом, учитывая значение для функции, генерирует доказательство, которое справедливо для этого значения. Тип будет${\displaystyle n}$${\displaystyle {\mathbb {N}}}$${\displaystyle P(n)}$${\displaystyle n}$${\displaystyle {\mathbb {N}}}$${\displaystyle P(n)}$${\displaystyle n}$${\displaystyle P(\,\cdot \,)}$

${\displaystyle \prod _{n{\mathbin {:}}{\mathbb {N} }}P(n)}$

=-типы создаются из двух терминов. Учитывая два термина, например и , вы можете создать новый тип . Термины этого нового типа представляют доказательства того, что пара сводится к одному и тому же каноническому термину. Таким образом, поскольку и и вычисляются к каноническому термину , будет термин типа . В интуиционистской теории типов существует единственный способ ввести =-типы, и это рефлексивность :${\displaystyle 2+2}$${\displaystyle 2\cdot 2}$${\displaystyle 2+2=2\cdot 2}$${\displaystyle 2+2}$${\displaystyle 2\cdot 2}$${\displaystyle 4}$${\displaystyle 2+2=2\cdot 2}$

${\displaystyle \operatorname {refl} {\mathbin {:}}\prod _{a{\mathbin {:}}A}(a=a).}$

Можно создать =-типы, например , когда термины не сводятся к одному и тому же каноническому термину, но вы не сможете создать термины этого нового типа. Фактически, если бы вы могли создать термин , вы могли бы создать термин . Помещение этого в функцию сгенерировало бы функцию типа . Поскольку интуиционистская теория типов определяет отрицание именно так, вы бы получили или, наконец, .${\displaystyle 1=2}$${\displaystyle 1=2}$${\displaystyle \bot}$${\displaystyle 1=2\to \bot }$${\displaystyle \ldots \to \bot }$${\displaystyle \отрицательный (1=2)}$${\displaystyle 1\neq 2}$

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

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

Индуктивные типы определяют новые константы, такие как ноль и функция-последователь . Поскольку не имеет определения и не может быть оценена с помощью подстановки, термины типа и становятся каноническими терминами натуральных чисел.${\displaystyle 0{\mathbin {:}}{\mathbb {N} }}$${\displaystyle S{\mathbin {:}}{\mathbb {N} }\to {\mathbb {N} }}$${\displaystyle S}$${\displaystyle S0}$${\displaystyle SSS0}$

Доказательства индуктивных типов возможны благодаря индукции . Каждый новый индуктивный тип имеет свое собственное индуктивное правило. Чтобы доказать предикат для каждого натурального числа, вы используете следующее правило:${\displaystyle P(\,\cdot \,)}$

${\displaystyle {\operatorname {{\mathbb {N} }-elim} }\,{\mathbin {:}}P(0)\,\to \left(\prod _{n{\mathbin {:}}{\mathbb {N} }}P(n)\to P(S(n))\right)\to \prod _{n{\mathbin {:}}{\mathbb {N} }}P(n)}$

Индуктивные типы в интуиционистской теории типов определяются в терминах W-типов, типа хорошо обоснованных деревьев. Более поздние работы в теории типов породили коиндуктивные типы, индукцию-рекурсию и индукцию-индукцию для работы с типами с более неясными видами самореферентности. Высшие индуктивные типы позволяют определять равенство между терминами.

Типы юниверса позволяют записывать доказательства для всех типов, созданных с помощью других конструкторов типов. Каждый термин в типе юниверса может быть отображен в тип, созданный с помощью любой комбинации и конструктора индуктивного типа. Однако, чтобы избежать парадоксов, в нет термина, который отображается в для любого . ^[1]${\displaystyle {\mathcal {U}}_{0}}$${\ displaystyle 0,1,2, \ Sigma, \ Pi, =,}$${\displaystyle {\mathcal {U}}_{n}}$${\displaystyle {\mathcal {U}}_{n}}$${\displaystyle {\mathcal {n}}\in \mathbb {N} }$

Чтобы написать доказательства для всех "малых типов" и , вы должны использовать , который содержит термин для , но не для себя . Аналогично, для . Существует предикативная иерархия вселенных, поэтому для количественной оценки доказательства по любым фиксированным постоянным вселенным вы можете использовать .${\displaystyle {\mathcal {U}}_{0}}$${\displaystyle {\mathcal {U}}_{1}}$${\displaystyle {\mathcal {U}}_{0}}$${\displaystyle {\mathcal {U}}_{1}}$${\displaystyle {\mathcal {U}}_{2}}$${\displaystyle к}$${\displaystyle {\mathcal {U}}_{k+1}}$

Типы вселенной — сложная особенность теорий типов. Первоначальную теорию типов Мартина-Лёфа пришлось изменить, чтобы учесть парадокс Жирара . Более поздние исследования охватывали такие темы, как «супервселенные», « вселенные Мало » и непредикативные вселенные.

Формальное определение интуиционистской теории типов записывается с использованием суждений. Например, в утверждении «если есть тип и есть тип, то есть тип» есть суждения «есть тип», «и» и «если ..., то ...». Выражение не является суждением; это определяемый тип.${\displaystyle А}$${\displaystyle Б}$${\displaystyle \textstyle \sum _{a:A}B}$${\displaystyle \textstyle \sum _{a:A}B}$

Этот второй уровень теории типов может сбивать с толку, особенно когда речь идет о равенстве. Существует суждение о равенстве терминов, которое может сказать . Это утверждение, что два термина сводятся к одному и тому же каноническому термину. Существует также суждение о равенстве типов, скажем, что , что означает, что каждый элемент является элементом типа и наоборот. На уровне типов есть тип и он содержит термины, если есть доказательство того, что и сводятся к одному и тому же значению. (Термины этого типа генерируются с использованием суждения о равенстве терминов.) Наконец, существует англоязычный уровень равенства, потому что мы используем слово «четыре» и символ « » для обозначения канонического термина . Такие синонимы Мартин-Лёф называет «определенно равными».${\displaystyle 4=2+2}$${\displaystyle А=Б}$${\displaystyle А}$${\displaystyle Б}$${\displaystyle 4=2+2}$${\displaystyle 4}$${\displaystyle 2+2}$${\displaystyle 4}$${\displaystyle SSSS0}$

Описание судебных решений ниже основано на обсуждении в деле Нордстрема, Петерссона и Смита.

Формальная теория работает с типами и объектами .

Тип объявляется следующим образом:

• ${\displaystyle A\ {\mathsf {Тип}}}$

Объект существует и принадлежит к типу, если:

• ${\displaystyle а{\mathbin {:}}А}$

Объекты могут быть равны

• ${\displaystyle а=б}$

и типы могут быть равны

• ${\displaystyle А=Б}$

Тип, который зависит от объекта другого типа, объявляется

• ${\displaystyle (x{\mathbin {:}}A)B}$

и удалено путем замены

• ${\displaystyle B[x/a]}$, заменив переменную объектом в .${\displaystyle x}$${\displaystyle а}$${\displaystyle Б}$

Объект, который зависит от объекта другого типа, может быть сделан двумя способами. Если объект «абстрагирован», то он записывается

• ${\displaystyle [x]b}$

и удалено путем замены

• ${\displaystyle b[x/a]}$, заменив переменную объектом в .${\displaystyle x}$${\displaystyle а}$${\displaystyle б}$

Объект-зависимый-от-объекта также может быть объявлен как константа как часть рекурсивного типа. Пример рекурсивного типа:

• ${\displaystyle 0{\mathbin {:}}\mathbb {N} }$
• ${\displaystyle S{\mathbin {:}}\mathbb {N} \to \mathbb {N} }$

Здесь, является константой, зависящей от объекта. Она не связана с абстракцией. Константы типа могут быть удалены путем определения равенства. Здесь связь с добавлением определяется с помощью равенства и сопоставления с образцом для обработки рекурсивного аспекта :${\displaystyle S}$${\displaystyle S}$${\displaystyle S}$

${\displaystyle {\begin{aligned}\operatorname {add} &{\mathbin {:}}\ (\mathbb {N} \times \mathbb {N} )\to \mathbb {N} \\\operatorname {add} (0,b)&=b\\\operatorname {add} (S(a),b)&=S(\operatorname {add} (a,b)))\end{aligned}}}$

${\displaystyle S}$манипулируется как непрозрачная константа — у нее нет внутренней структуры для подстановки.

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

${\displaystyle \Gamma \vdash \sigma \ {\mathsf {Type}}}$	σ — это правильно сформированный тип в контексте Γ.
${\displaystyle \Gamma \vdash t{\mathbin {:}}\sigma }$	t — правильно сформированный термин типа σ в контексте Γ.
${\displaystyle \Gamma \vdash \sigma \equiv \tau }$	σ и τ являются равными типами в контексте Γ.
${\displaystyle \Gamma \vdash t\equiv u{\mathbin {:}}\sigma }$	t и u являются оценочно равными терминами типа σ в контексте Γ.
${\displaystyle \vdash \Gamma \ {\mathsf {Context}}}$	Γ — это правильно сформированный контекст типизированных предположений.

По соглашению, есть тип, который представляет все другие типы. Он называется (или ). Поскольку является типом, его членами являются объекты. Есть зависимый тип , который отображает каждый объект в соответствующий ему тип. В большинстве текстов никогда не пишется. Из контекста утверждения читатель почти всегда может сказать, относится ли к типу или относится ли к объекту, который соответствует типу.${\displaystyle {\mathcal {U}}}$${\displaystyle \operatorname {Set} }$${\displaystyle {\mathcal {U}}}$${\displaystyle \operatorname {El} }$${\displaystyle \operatorname {El} }$${\displaystyle A}$${\displaystyle {\mathcal {U}}}$

Это полная основа теории. Все остальное — производное.

Для реализации логики каждому предложению присваивается свой тип. Объекты в этих типах представляют различные возможные способы доказательства предложения. Если для предложения нет доказательства, то тип не имеет объектов. Операторы типа «и» и «или», которые работают с предложениями, вводят новые типы и новые объекты. Таков тип, который зависит от типа и типа . Объекты в этом зависимом типе определены как существующие для каждой пары объектов в и . Если или не имеет доказательства и является пустым типом, то новый тип, представляющий также пуст.${\displaystyle A\times B}$${\displaystyle A}$${\displaystyle B}$${\displaystyle A}$${\displaystyle B}$${\displaystyle A}$${\displaystyle B}$${\displaystyle A\times B}$

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

Используя язык теории категорий , RAG Seely ввел понятие локально декартовой замкнутой категории (LCCC) как базовой модели теории типов. Это было уточнено Хофманном и Дибьером до категорий с семействами или категорий с атрибутами на основе более ранней работы Картмелла. ^[2]

Категория с семействами — это категория C контекстов (в которой объекты являются контекстами, а морфизмы контекстов — подстановками) вместе с функтором T  : C ^op → Fam ( Set ).

Fam ( Set ) — это категория семейств множеств, в которой объекты — это пары « индексного${\displaystyle (A,B)}$ множества» A и функции B : X → A , а морфизмы — это пары функций f  : A → A' и g  : X → X' , такие, что B' _° g = f _° B — другими словами, f отображает B _a в B _{g ( a )} .

Функтор T назначает контексту G набор ⁠ ⁠${\displaystyle Ty(G)}$ типов, а для каждого ⁠ ⁠${\displaystyle A:Ty(G)}$ — набор ⁠ ⁠${\displaystyle Tm(G,A)}$ терминов. Аксиомы для функтора требуют, чтобы они гармонично сочетались с подстановкой. Подстановка обычно записывается в форме Af или af , где A — тип в ⁠ ⁠ ,${\displaystyle Ty(G)}$ а a — терм в ⁠ ⁠${\displaystyle Tm(G,A)}$ , а f — подстановка из D в G . Здесь ⁠ ⁠${\displaystyle Af:Ty(D)}$ и ⁠ ⁠${\displaystyle af:Tm(D,Af)}$ .

Категория C должна содержать конечный объект (пустой контекст) и конечный объект для формы продукта, называемой пониманием или расширением контекста, в которой правый элемент является типом в контексте левого элемента. Если G является контекстом, и ⁠ ⁠${\displaystyle A:Ty(G)}$ , то должен быть объект ⁠ ⁠${\displaystyle (G,A)}$ final среди контекстов D с отображениями p  : D → G , q  : Tm ( D,Ap ).

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

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

Фундаментальное различие — это экстенсиональная и интенсиональная теории типов. В экстенсиональной теории типов дефиниционное (т. е. вычислительное) равенство не отличается от пропозиционального равенства, которое требует доказательства. Как следствие, проверка типов становится неразрешимой в экстенсиональной теории типов, поскольку программы в этой теории могут не завершаться. Например, такая теория позволяет задать тип Y-комбинатору ; подробный пример этого можно найти в Nordstöm and Petersson Programming in Martin-Löf's Type Theory . ^[3] Однако это не мешает экстенсиональной теории типов быть основой для практического инструмента; например, Nuprl основан на экстенсиональной теории типов.

Напротив, в теории интенсиональных типов проверка типов разрешима , но представление стандартных математических понятий несколько более громоздко, поскольку интенсиональное рассуждение требует использования сетоидов или подобных конструкций. Существует много общих математических объектов, с которыми трудно работать или которые невозможно представить без этого, например, целые числа , рациональные числа и действительные числа . Целые и рациональные числа можно представить без сетоидов, но с таким представлением трудно работать. Действительные числа Коши невозможно представить без этого. ^[4]

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

Различные формы теории типов были реализованы как формальные системы, лежащие в основе ряда помощников доказательства . Хотя многие из них основаны на идеях Пера Мартина-Лёфа, многие имеют дополнительные возможности, больше аксиом или иную философскую подоплеку. Например, система Nuprl основана на теории вычислительных типов ^[5] , а Coq основана на исчислении (ко)индуктивных конструкций . Зависимые типы также присутствуют в дизайне языков программирования , таких как ATS , Cayenne , Epigram , Agda , ^[6] и Idris . ^[7]

Пер Мартин-Лёф построил несколько теорий типов, которые были опубликованы в разное время, некоторые из них намного позже, чем препринты с их описанием стали доступны специалистам (среди прочих Жан-Ив Жирар и Джованни Самбин). Список ниже пытается перечислить все теории, которые были описаны в печатной форме, и набросать ключевые особенности, которые отличали их друг от друга. Все эти теории имели зависимые произведения, зависимые суммы, непересекающиеся объединения, конечные типы и натуральные числа. Все теории имели одни и те же правила редукции, которые не включали η-редукцию ни для зависимых произведений, ни для зависимых сумм, за исключением MLTT79, где добавлена ​​η-редукция для зависимых произведений.

MLTT71 была первой теорией типов, созданной Пером Мартином-Лёфом. Она появилась в препринте в 1971 году. Она имела одну вселенную, но эта вселенная имела имя сама по себе, т. е. это была теория типов с, как это называется сегодня, «Тип в Типе». Жан-Ив Жирар показал, что эта система была непоследовательной, и препринт так и не был опубликован.

MLTT72 был представлен в препринте 1972 года, который сейчас опубликован. ^[8] Эта теория имела одну вселенную V и не имела типов идентичности (=-типов). Вселенная была « предикативной » в том смысле, что зависимое произведение семейства объектов из V на объект, который не был в V, например, сам V, не предполагалось находящимся в V. Вселенная была à la Principia Mathematica Рассела , т. е. можно было бы напрямую писать «T∈V» и «t∈T» (Мартин-Лёф использует знак «∈» вместо современного «:») без добавления конструктора, такого как «El».

MLTT73 было первым определением теории типов, опубликованным Пером Мартином-Лёфом (оно было представлено на Logic Colloquium '73 и опубликовано в 1975 году ^[9] ). Существуют типы тождества, которые он описывает как «предложения», но поскольку не вводится никакого реального различия между предложениями и остальными типами, смысл этого неясен. Есть то, что позже приобретает название J-элиминатора, но пока без названия (см. стр. 94–95). В этой теории существует бесконечная последовательность вселенных V ₀ , ..., V _n , ... . Вселенные являются предикативными, а-ля Рассел и некумулятивными . Фактически, следствие 3.10 на стр. 115 гласит, что если A∈V _m и B∈V _n таковы, что A и B являются обратимыми, то m  =  n . Это означает, например, что в этой теории будет трудно сформулировать аксиому однозначности — в каждом из V _i есть сжимаемые типы , но неясно, как объявить их равными, поскольку нет типов тождественности, связывающих V _i и V _j при i ≠ j .

MLTT79 был представлен в 1979 году и опубликован в 1982 году. ^[10] В этой статье Мартин-Лёф представил четыре основных типа суждения для теории зависимых типов, которая с тех пор стала фундаментальной в изучении метатеории таких систем. Он также ввел контексты как отдельное понятие в ней (см. стр. 161). Существуют типы идентичности с J-элиминатором (который уже появился в MLTT73, но не имел там этого названия), а также с правилом, которое делает теорию «экстенсиональной» (стр. 169). Существуют W-типы. Существует бесконечная последовательность предикативных вселенных, которые являются кумулятивными .

Библиополис : в книге «Библиополис» 1984 года ^[11] обсуждается теория типов , но она несколько открыта и, по-видимому, не представляет собой определенный набор вариантов, поэтому с ней не связана какая-либо конкретная теория типов.

• Интуиционистская логика
• Типизированное лямбда-исчисление

• Мартин-Лёф, Пер ; Самбин, Джованни (1984). Интуиционистская теория типов (PDF) . Неаполь: Библиополис. ISBN 978-8870881059. OCLC  12731401.

• Согласно заметкам Мартина-Лёфа, записанным Джованни Самбином (1980)
• Нордстрем, Бенгт; Петерссон, Кент; Смит, Ян М. (1990). Программирование в теории типов Мартина-Лёфа. Издательство Оксфордского университета. ISBN 9780198538141.
• Томпсон, Саймон (1991). Теория типов и функциональное программирование. Эддисон-Уэсли. ISBN 0-201-41667-0.
• Гранстрем, Йохан Г. (2011). Трактат по интуиционистской теории типов. Спрингер. ISBN 978-94-007-1735-0.

• Проект «Типы ЕС»: Учебные пособия – конспекты лекций и слайды из Летней школы по типам 2005 г.
• n-Categories - Sketch of a Definition – письмо Джона Баэза и Джеймса Долана Россу Стрит , 29 ноября 1995 г.