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

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

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

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

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

形式化定義

編輯

Π-類型

編輯

在全類(論域中全部類型構成的類型)   中給定一個類型  ,存在着類型族   為每一項   賦予一個類型  。一個值域依賴於其參數的函數,稱之為一個依賴類型函數,該函數的類型則稱之為依賴類型依賴乘積類型Π-類型。在此例子中,依賴類型可以寫作

 

 

B為常數,則依賴類型退化成一般形態的函數  。即   等價於函數類型  

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

例如, 表示實數 -元組類型,則   表示這樣的函數類型:給定一個自然數n,該函數返回一個大小為n的實數元組。一般的函數空間可以看作依賴型函數的一個特例,當函數返回值類型實質上並不依賴於輸入時,如   即為從自然數到實數的函數類型,它可以在簡單類型lambda演算中被寫作  

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

 

Σ-類型

編輯

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

 

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

 

  。若B為常數,則依賴值對類型退化為一般的乘積類型,即笛卡爾積  

Lambda 立方

編輯

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

一階依賴類型

編輯

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

二階依賴類型

編輯

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

高階依賴類型多態 lambda 演算

編輯

高階類型系統   擴充了  ,使之支持 Lambda 立方中的全部四種表達形式:從項到項的函數、從類型到類型的函數、從項到類型的函數、以及從類型到項的函數。這對應於構造演算(calculus of constructions),而構造演算則是證明輔助器 Coq 所基於的構造歸納演算[1]理論的基礎。

依賴類型編程語言

編輯
語言 是否活躍開發中 範式[腳註 1] 策略(tactics) 證明項 終止檢查 類型允許依賴於[腳註 2] 全類 證明無關性 是否支持程序抽取 程序抽取是否消除無關項
Agda [2] 純函數式 少且有限[腳註 3] 是(可選) 任意項 是(可選)[腳註 4] 證明無關性參數[4] HaskellJavaScript [4]
ATS英語ATS (programming language) [5] 函數式 / 命令式 [6] ? ? ? ?
Cayenne[7] 純函數式 任意項 ? ?
Gallina(Coq [8] 純函數式 任意項 [腳註 5] Haskell、SchemeOCaml
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 取代。

參見

編輯

參考文獻

編輯
  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. ^ 4.0 4.1 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. ^ 11.0 11.1 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. ^ 15.0 15.1 Edwin Brady. How does Idris compare to other dependently-typed programming languages?. 
  16. ^ Matita SVN. [2014-08-24]. (原始內容存檔於2006-05-08). 
  17. ^ Sage頁面存檔備份,存於網際網路檔案館

延伸閱讀

編輯