依值型別

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

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

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

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

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

形式化定義

Π-型別

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

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

或

${\displaystyle \Pi (x:A),B(x)}$

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

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

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

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

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

Σ-型別

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

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

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

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

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

Lambda 立方

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

一階依值型別

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

二階依值型別

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

高階依值型別多型 lambda 演算

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

依值型別程式語言

語言	是否活躍開發中	範式[註腳 1]	策略（tactics）	證明項	終止檢查	型別允許依賴於[註腳 2]	全類	證明無關性	是否支援程式抽取	程式抽取是否消除無關項
Agda	是[2]	純函數式	少且有限[註腳 3]	是	是（可選）	任意項	是（可選）[註腳 4]	證明無關性參數[4]	Haskell、JavaScript	是[4]
ATS（英語：ATS (programming language)）	是[5]	函數式 / 命令式	否[6]	是	是	?	?	?	是	?
Cayenne[7]	否	純函數式	否	是	否	任意項	否	否	?	?
Gallina（Coq）	是[8]	純函數式	是	是	是	任意項	是[註腳 5]	否	Haskell、Scheme、OCaml	是
Dependent ML（英語：Dependent ML）	否[註腳 6]	?	?	是	?	自然數	?	?	?	?
Guru[9]	否[10]	純函數式[11]	hypjoin[12]	是[11]	是	任意項	否	是	Carraway	是
Idris	是[13]	純函數式[14]	是[15]	是	是（可選）	任意項	是	否	是	是[15]
Matita（英語：Matita）	是[16]	純函數式	是	是	是	任意項	是	是	OCaml	是
Nuprl（英語：Nuprl）	是	純函數式	是	是	是	任意項	是	?	是	?
F*	是	函數式 / 命令式	?	?	?	?	?	?	?	?
PVS（英語：Prototype Verification System）	是	?	是	?	?	?	?	?	?	?
Sage[17]	?	混合型別檢查	?	?	?	?	?	?	?	?
Twelf（英語：Twelf）	是	邏輯式	?	是	是（可選）	任意（LF）項	否	否	?	?

註腳

1. 這裡專指核心語言之編程範式，而非任何 tactic 或代碼生成子語言的範式。
2. 受到語意約束，諸如全類（universe）的約束。
3. 環求解器。^[3]
4. 可選的全類、可選的全類多型、可選的顯式全類指定。
5. 全類，由全類約束自動推導（不同於 Agda 的全類多型）和可選的全類約束回顯。
6. 已由 ATS 取代。

參見

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

參考文獻

1. Announce:Calculus of Inductive Constructions. [2019-04-12]. （原始內容存檔於2020-11-11）.
2. Agda download page. [2014-08-24]. （原始內容存檔於2019-06-27）.
3. Agda Ring Solver. [2014-08-24]. （原始內容存檔於2009-04-17）.
4. Announce: Agda 2.2.8. [2014-08-24]. （原始內容存檔於2011-07-18）.
5. ATS Changelog. [2014-08-24]. （原始內容存檔於2012-03-02）.
6. email from ATS inventor Hongwei Xi. [2014-08-24]. （原始內容存檔於2013-02-04）.
7. Augustsson, Lennart. Cayenne – a language with dependent types. ICFP '98. Proceedings of the third ACM SIGPLAN international conference on Functional programming. 1998: 239–250. CiteSeerX 10.1.1.47.155 . S2CID 18331937. doi:10.1145/289423.289451 .
8. Coq CHANGES in Subversion repository. [2014-08-24]. （原始內容存檔於2018-09-29）.
9. Guru （頁面存檔備份，存於網際網路檔案館）
10. Guru SVN. [2014-08-24]. （原始內容存檔於2015-11-18）.
11. Aaron Stump. Verified Programming in Guru (PDF). 6 April 2009 [28 September 2010]. （原始內容 (PDF)存檔於2009年12月29日）.
12. Adam Petcher. Deciding Joinability Modulo Ground Equations in Operational Type Theory (PDF). 1 April 2008 [14 October 2010]. （原始內容存檔 (PDF)於2010-07-19）.
13. Idris git repository.^{[永久失效連結]}
14. Idris, a language with dependent types - extended abstract (PDF). [2014-08-24]. （原始內容 (PDF)存檔於2011-07-16）.
15. Edwin Brady. How does Idris compare to other dependently-typed programming languages?.
16. Matita SVN. [2014-08-24]. （原始內容存檔於2006-05-08）.
17. Sage （頁面存檔備份，存於網際網路檔案館）

延伸閱讀

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