依值型別
維基百科,自由的 encyclopedia
在電腦科學和邏輯中,依值型別(或依值型別,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*。