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

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

Дизайн

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

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

Теория типов

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

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

Тип 0, тип 1 и тип 2

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

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

Аналогично, тип 1 содержит 1 канонический термин и представляет существование. Его еще называют типом единицы . Он часто представляет собой предложения, которые можно доказать, и поэтому иногда его записывают . ^[^{нужна цитата}^] $\top$

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

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

Конструктор типа Σ

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

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

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

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

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

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

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

\sum _{m{\mathbin {:}}{\mathbb {Z} }}{\sum _{n{\mathbin {:}}{\mathbb {Z} }}((m<n) ={\text{True}})}

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

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

Конструктор типа Π

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

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

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

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

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

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

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

= конструктор типа

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

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

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

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

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

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

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

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

{\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] ${\mathcal {U}}_{0}$ ${\ displaystyle 0,1,2, \ Sigma, \ Pi, =,}$ ${\mathcal {U}}_{n}$ ${\mathcal {U}}_{n}$ ${\mathcal {n}}\in \mathbb {N}$

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

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

Суждения

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

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

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

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

Тип объявляется:

$A\ {\mathsf {Type}}$

Объект существует и находится в определенном типе, если:

$a{\mathbin {:}}A$

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

$a=b$

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

$A=B$

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

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

и удаляется заменой

$B[x/a]$ , заменяя переменную объектом в . $x$ $a$ $B$

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

$[x]b$

и удаляется заменой

$b[x/a]$ , заменяя переменную объектом в . $x$ $a$ $b$

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

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

Здесь — постоянный объект, зависящий от объекта. Это не связано с абстракцией. Константы вроде можно удалить, определив равенство. Здесь связь со сложением определяется с использованием равенства и сопоставления с образцом для обработки рекурсивного аспекта : $S$ $S$ $S$

{\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}}

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

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

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

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

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

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

Категориальные модели теории типов

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

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

Fam ( Set ) — категория семейств Множеств, в которой объектами являются пары «индексного множества» A и функции B : X → A , а морфизмами — пары функций f : A → A' и g : X → A. X' _, такой, что _B' _°g = f _°B — другими словами, f отображает Ba в Bg ₍_a₎ . $(A,B)$

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

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

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

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

Экстенсиональный и интенсиональный

Фундаментальное различие заключается в теории экстенсионального и интенсионального типов. В теории экстенсионального типа дефинициональное (т. е. вычислительное) равенство не отличается от пропозиционального равенства, которое требует доказательства. Как следствие, проверка типов становится неразрешимой в теории экстенсиональных типов, поскольку программы в этой теории могут не завершиться. Например, такая теория позволяет задать тип Y-комбинатору ; подробный пример этого можно найти в книге Нордстёма и Петерссона « Программирование в теории типов Мартина-Лёфа» . ^[3] Однако это не мешает теории экстенсиональных типов быть основой практического инструмента; например, Nuprl основан на теории экстенсиональных типов.

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

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

Реализации теории типов

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

Теории типа Мартина-Лёфа

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

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

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

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

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

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

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

Примечания

^ Берто, Ив; Кастеран, Пьер (2004). Интерактивное доказательство теорем и разработка программ: Coq'Art: исчисление индуктивных конструкций . Тексты по теоретической информатике. Берлин Гейдельберг: Springer. ISBN 978-3-540-20854-9.
^ Клерамбо, Пьер; Дюбьер, Питер (2014). «Биэквивалентность локально декартовых замкнутых категорий и теорий типа Мартина-Лёфа». Математические структуры в информатике . 24 (6). arXiv : 1112.3456 . дои : 10.1017/S0960129513000881. ISSN 0960-1295. S2CID 416274.
^ Бенгт Нордстрем; Кент Петерссон; Ян М. Смит (1990). Программирование в теории типов Мартина-Лёфа . Издательство Оксфордского университета, стр. 90.
^ Альтенкирх, Торстен, Томас Анберре и Нуо Ли. «Определимые факторы в теории типов».
^ Аллен, Сан-Франциско; Бикфорд, М.; Констебль, РЛ; Итон, Р.; Крейц, К.; Лориго, Л.; Моран, Э. (2006). «Инновации в теории вычислительных типов с использованием Nuprl». Журнал прикладной логики . 4 (4): 428–469. дои : 10.1016/j.jal.2005.10.005 .
^ Норелл, Ульф (2009). «Зависимо типизированное программирование в Agda». Материалы 4-го международного семинара «Типы в языковом проектировании и реализации» . ТЛДИ '09. Нью-Йорк, штат Нью-Йорк, США: ACM. стр. 1–2. CiteSeerX 10.1.1.163.7149 . дои : 10.1145/1481861.1481862. ISBN 9781605584201. S2CID 1777213.
^ Брэди, Эдвин (2013). «Идрис, зависимо типизированный язык программирования общего назначения: проектирование и реализация». Журнал функционального программирования . 23 (5): 552–593. дои : 10.1017/S095679681300018X . ISSN 0956-7968. S2CID 19895964.
^ Пер Мартин-Лёф, Интуиционистская теория типов, Двадцать пять лет конструктивной теории типов (Венеция, 1995), Oxford Logic Guides, т. 36, стр. 127–172, Oxford Univ. Пресс, Нью-Йорк, 1998 г.
^ Мартин-Лёф, Пер (1975). «Интуиционистская теория типов: предикативная часть». Исследования по логике и основам математики . Логический коллоквиум '73 (Бристоль, 1973). Том. 80. Амстердам: Северная Голландия. стр. 73–118.
^ Мартин-Лёф, Пер (1982). «Конструктивная математика и компьютерное программирование». Исследования по логике и основам математики . Логика, методология и философия науки, VI (Ганновер, 1979). Том. 104. Амстердам: Северная Голландия. стр. 153–175.
^ Пер Мартин-Лёф, «Интуиционистская теория типов», Исследования по теории доказательств (конспекты лекций Джованни Самбина), том. 1, стр. iv+91, 1984 г.

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

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

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

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