直覺類型論

構造類型論為計算機科學家提供了一個框架，以一種優雅和靈活的方式把邏輯和程序設計語言結合起來：在同一形式系統中，可以同時表達規約和（函數式語言）程序，從證明規則可以導出正確的程序，並驗證程序具有某種性質，從而在同一系統內完成程序的開發和驗證。構造類型論的三大理論基石是：直覺類型論和構造數學、弄演算和函數式語言程序設計與實現、證明論和Curry-Howard同態。直覺類型論為構造數學提供直覺解釋。它是一個邏輯框架，可表達和解釋其它邏輯或理論 ^[1]  。從它的規範化證明立即得出其所表達理論的規範化。直覺類型論基於的是命題和類型的同一: 一個命題同一於它的證明的類型。這種同一通常叫做Curry-Howard同構，它最初公式化了命題邏輯和簡單類型 lambda演算。類型論通過介入包含着值的依賴類型把這種同一擴展到謂詞邏輯。類型論內在化了 Brouwer、Heyting 和 Kolmogorov 提議的叫做 BHK釋義的直覺邏輯釋義。類型論的類型扮演了類似於集合在集合論的角色，但是在類型論中的函數總是可計算的。

在直覺類型論的上下文中，連結詞是可能使用已給定的類型而構造類型的一種方式。類型論的基本連結詞有：

-類型，也叫做依賴函數類型，一般化了普通的函數空間，建模其結果的類型可以隨它們的輸入而變化的函數，比如，對實數的

-元組寫為

，則

表示對給定的自然數返回這個大小的實數元組的函數的類型。在值域類型實際上不依賴於輸入的時候，普通函數空間作為特殊情況出現，比如

是從自然數到實數的函數的類型，它也寫為

。使用 Curry-Howard同構，

-類型還充當建模藴涵和全稱量化：比如，居留於

的一個項，它對任何一對自然數的函數指派加法對這個數對是交換性的證明，並因此可以被當作加法對於所有自然數是交換性的一個證明。

-類型，也叫做依賴乘積類型，一般化了普通的笛卡爾積，建模第二個構件的類型依賴於第一個構件的有序對，比如類型

表示自然數和這個大小的實數的元組的有序對的類型，就是説，這個類型可以用來建模任意長度的序列(通常叫做列表)。在第二個構件的類型實際上不依賴於第一個構件的時候，常規的笛卡爾積類型作為特殊情況出現，比如

是自然數和實數的有序對的類型，它也寫為

。再次使用 Curry-Howard同構，

-類型也充當建模合取和存在量化。

特別重要的是

(空類型)、

(單位類型)和

(布爾值或真值)。再次用到 Curry-Howard同構，

表示假而

表示真。使用有限類型，我們可以定義否定為

，服從Curry-Howard同構，不相交併集也表示析取，它可以定義為

。

給定

，則

是

等於

的等式證明。只有一個(規範的)

的居留，並且這是自反性

的證明。

歸納類型的基本例子是自然數

的類型，它是通過

和

生成的。命題為類型原理的一個重要應用是通過對用

索引的給定類型

的一個消除常量：

來把(依賴的)原始遞歸和歸納同一起來的。在一般的歸納類型中可以被定義為 W-類型，它是良基的樹的類型。

一類重要的歸納類型是像上面提及的向量

的歸納類型家族，它們是歸納生成自構造子

和

。再次用到Curry-Howard同構，歸納類型家族對應于歸納定義的關係。

全集的一個例子是

，它是所有小類型的全集，它包含前面介紹的所有類型的名字。對於每個名字

我們關聯上一個類型

，這是它的外延或意義。標準上是假定全集的一個直謂性等級: 對於每個自然數

，這裏的全集

包含以前的全集的一個代碼，就是説，我們通過

而有

。這個等級經常被假定為是累積性的，就是説來自

的代碼被嵌入了

。已經研究了更強的全集原理，比如超全集和 Mahlo 全集。在 1992 年 Huet 和 Coquand 介入了構造演算，它是帶有非直謂性全集的類型論，從而把類型論同 Girard 的系統F 合併起來了。這個擴展不被直覺主義者所普遍接受，因為它允許非直謂性的，就是循環的構造，這經常用經典推理來識別。

一個基本區別是外延和內涵的類型論。在外延類型論中定義性(就是計算性)等式不區別於需要證明的命題性等式。作為結論類型檢查成為不可判定性的。相反的，在內涵類型論中，類型檢查是可判定性的，但是很多數學概念的表達是不標準的，因為缺乏外延推理。這是對這種折中是否是不可避免的和在內涵類型論中缺乏外延原理是一個特色還是一個缺陷的討論的一個主題。