依賴類型

在計算機科學和邏輯中，依賴類型（或依值類型，dependent type）是指依賴於值的類型，其理論同時包含了數學基礎中的類型論和計算機編程中用以減少程序錯誤的類型系統兩方面。在 Per Martin-Löf 的直覺類型論中，依賴類型可對應於謂詞邏輯中的全稱量詞和存在量詞；在依賴類型函數式編程語言如ATS、Agda、Dependent ML、Epigram、F*和Idris中，依賴類型系統通過極其豐富的類型表達能力使得程序規範得以藉助類型的形式被檢查，從而有效減少程序錯誤。

依賴類型的兩個常見實例是依賴函數類型（又稱依賴乘積類型、Π-類型）和依賴值對類型（又稱依賴總和類型、Σ-類型）。一個依賴類型函數的返回值類型可以依賴於某個參數的具體值，而非僅僅參數的類型，例如，一個輸入參數為整型值n的函數可能返回一個長度為n的數組；一個依賴類型值對中的第二個值可以依賴於第一個值，例如，依賴類型可表示這樣的類型：它由一對整數組成，其中的第二個數總是大於第一個數。

依賴類型增加了類型系統的複雜度。由於確定兩個依賴於值的類型的等價性需要涉及具體的計算，若允許在依賴類型中使用任意值的話，其類型檢查將會成為不可判定問題；換言之，無法確保程序的類型檢查一定會停機。

由於Curry-Howard同構揭示了程序語言的類型論與證明論的直覺邏輯之間的緊密關聯性，以依賴類型系統為基礎的編程語言大多同時也作為構造證明與可驗證程序的輔助工具而存在，如 Coq 和 Agda（但並非所有證明輔助工具都以類型論為基礎）；近年來，一些以通用和系統編程為目的的編程語言被設計出來，如 Idris。

一些以證明輔助為主要目的的編程語言採用強函數式編程（total functional programming），這消除了停機問題，同時也意味着通過它們自身的核心語言無法實現任意無限遞歸，不是圖靈完全的，如 Coq 和 Agda；另外一些依賴類型編程語言則是圖靈完全的，如 Idris、由 ML 衍生而來的 ATS 和 由 F# 衍生而來的 F*。

形式化定義

Π-類型

在全類（論域中全部類型構成的類型） ${\mathcal {U}}$ 中給定一個類型 $A:{\mathcal {U}}$，存在着類型族 $B:A\to {\mathcal {U}}$ 為每一項 $a:A$ 賦予一個類型 $B(a):{\mathcal {U}}$。一個值域依賴於其參數的函數，稱之為一個依賴類型函數，該函數的類型則稱之為依賴類型、依賴乘積類型或Π-類型。在此例子中，依賴類型可以寫作

$\Pi _{(x:A)}B(x)$

或

$\Pi (x:A),B(x)$

若B為常數，則依賴類型退化成一般形態的函數 $A\to B$。即 $\Pi _{(x:A)}B$ 等價於函數類型 $A\to B$。

被稱之為「Π-類型」的原因是它可以被看作是類型的笛卡爾積。Π-類型同時也可被看作是全稱量詞的模型。

例如，${\mbox{Vec}}({\mathbb {R} },n)$表示實數的$n$-元組類型，則 $\Pi _{(n:{\mathbb {N} })}{\mbox{Vec}}({\mathbb {R} },n)$ 表示這樣的函數類型：給定一個自然數n，該函數返回一個大小為n的實數元組。一般的函數空間可以看作依賴型函數的一個特例，當函數返回值類型實質上並不依賴於輸入時，如 $\Pi _{(n:{\mathbb {N} })}\;{\mathbb {R} }$ 即為從自然數到實數的函數類型，它可以在簡單類型lambda演算中被寫作 ${\mathbb {N} }\to {\mathbb {R} }$。

多態是依賴類型函數的一個重要實例。給定一個類型，函數作用於該類型的元素之上。一個返回元素類型為C的多態函數可能擁有如下的多態類型：

$\Pi _{(A:{\mathcal {U}})}A\to C$

Σ-類型

依賴函數類型的對偶是依賴值對類型（或依賴總和類型、Σ-類型）。它與余積或不交並的概念相類似。Σ-類型可以被理解成存在量詞的模型。寫作：

$\Sigma _{(x:A)}B(x)$

依賴值對類型表示一個值對，其中第二項的類型依賴於第一項的值。若

$(a,b):\Sigma _{(x:A)}B(x)$

則 $a:A$ 且 $b:B(a)$。若B為常數，則依賴值對類型退化為一般的乘積類型，即笛卡爾積 $A\times B$。

Lambda 立方

Henk Barendregt 提出了 Lambda 立方模型，用於對不同的類型系統的表達能力加以區分。Lambda 立方的八個頂點分別對應各自的類型系統，簡單類型lambda演算位於表達能力最低的頂點上，而構造演算（calculus of constructions）則位於表達能力最強的頂點上。

一階依賴類型

一階依賴類型 $\lambda \Pi$，對應於邏輯框架 LF，是通過把簡單類型lambda演算的函數空間一般化為依賴乘積類型而獲得的。

二階依賴類型

二階依賴類型 $\lambda \Pi 2$，通過允許對 $\lambda \Pi$ 類型構造子的量化得到。此時，依賴乘積類型涵括了簡單類型lambda演算中的$\to$與 系統F 中的$\forall$。

高階依賴類型多態 lambda 演算

高階類型系統 $\lambda \Pi \omega$ 擴充了 $\lambda \Pi 2$，使之支持 Lambda 立方中的全部四種表達形式：從項到項的函數、從類型到類型的函數、從項到類型的函數、以及從類型到項的函數。這對應於構造演算（calculus of constructions），而構造演算則是證明輔助器 Coq 所基於的構造歸納演算理論的基礎。

依賴類型編程語言

語言	是否活躍開發中	範式	策略（tactics）	證明項	終止檢查	類型允許依賴於	全類	證明無關性	是否支持程序抽取	程序抽取是否消除無關項
Agda	是	純函數式	少且有限	是	是（可選）	任意項	是（可選）	證明無關性參數	Haskell、JavaScript	是
ATS	是	函數式 / 命令式	否	是	是	?	?	?	是	?
Cayenne	否	純函數式	否	是	否	任意項	否	否	?	?
Gallina（Coq）	是	純函數式	是	是	是	任意項	是	否	Haskell、Scheme、OCaml	是
Dependent ML	否	?	?	是	?	自然數	?	?	?	?
Guru	否	純函數式	hypjoin	是	是	任意項	否	是	Carraway	是
Idris	是	純函數式	是	是	是（可選）	任意項	是	否	是	是
Matita	是	純函數式	是	是	是	任意項	是	是	OCaml	是
Nuprl	是	純函數式	是	是	是	任意項	是	?	是	?
F*	是	函數式 / 命令式	?	?	?	?	?	?	?	?
PVS	是	?	是	?	?	?	?	?	?	?
Sage	?	混合類型檢查	?	?	?	?	?	?	?	?
Twelf	是	邏輯式	?	是	是（可選）	任意（LF）項	否	否	?	?

參見

• Lambda立方體
• 有類型lambda演算
• 直覺類型論

延伸閱讀

• Why Dependent Types Matter （頁面存檔備份，存於網際網路檔案館） T. Altenkirch, C. McBride, J. McKinna