依值類型

在電腦科學和邏輯中，依值類型（舊譯依賴類型，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 所基於的構造歸納演算理論的基礎。

## 依值類型程式語言

語言｜是否活躍開發中｜範式這裡專指核心語言之編程範式，而非任何 tactic 或代碼生成子語言的範式。｜策略（tactics）｜證明項｜終止檢查｜類型允許依賴於受到語義約束，諸如全類（universe）的約束。｜全類｜證明無關性｜是否支持程序抽取｜程序抽取是否消除無關項

Agda｜是｜純函數式｜少且有限環求解器。｜是｜是（可選）｜任意項｜是（可選）可選的全類、可選的全類多態、可選的顯式全類指定。｜證明無關性參數｜Haskell、JavaScript｜是

ATS語言｜是｜函數式 / 命令式｜否｜是｜是｜未知｜未知｜未知｜是｜未知

Cayenne｜否｜純函數式｜否｜是｜否｜任意項｜否｜否｜未知｜未知

Gallina（Coq）｜是｜純函數式｜是｜是｜是｜任意項｜是全類，由全類約束自動推導（不同於 Agda 的全類多態）和可選的全類約束回顯。｜否｜Haskell、Scheme、OCaml｜是

Dependent ML｜否已由 ATS 取代。｜未知｜未知｜是｜未知｜自然數｜未知｜未知｜未知｜未知

Guru｜否｜純函數式｜hypjoin｜是｜是｜任意項｜否｜是｜Carraway｜是

Idris｜是｜純函數式｜是｜是｜是（可選）｜任意項｜是｜否｜是｜是

Matita｜是｜純函數式｜是｜是｜是｜任意項｜是｜是｜OCaml｜是

Nuprl｜是｜純函數式｜是｜是｜是｜任意項｜是｜未知｜是｜未知

F、｜是｜函數式 / 命令式｜未知｜未知｜未知｜未知｜未知｜未知｜未知｜未知

原型驗證系統｜是｜未知｜是｜未知｜未知｜未知｜未知｜未知｜未知｜未知

Sage｜未知｜混合類型檢查｜未知｜未知｜未知｜未知｜未知｜未知｜未知｜未知

Twelf｜是｜邏輯式｜未知｜是｜是（可選）｜任意（LF）項｜否｜否｜未知｜未知

## 延伸閱讀

- Why Dependent Types Matter T. Altenkirch, C. McBride, J. McKinna