依賴類型

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

基本介紹

• 中文名：依賴類型
• 外文名：dependent type
• 學科：計算機科學

簡介

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

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

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

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

Lambda 立方

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

一階依賴類型

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

二階依賴類型

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

高階依賴類型多態 lambda 演算

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