相關類型

Question

前一段時間，我遇到了「獨特賣點」似乎是依賴類型的編程語言Idris。有人可以解釋什麼是從屬類型，他們正在處理什麼樣的問題？

Answer 1

那麼，依賴類型允許表達在編譯期間檢查的數據類型不變量。依賴類型的規範示例是長度索引列表，也稱爲向量。載體的伊德里斯定義是：

data Vec (A : Type) : Nat -> Type where 
    Nil : Vec A 0 
    Cons : A -> Vec A n -> Vec A (S n) 

其中type Nat對應於自然數在皮亞諾的符號：

data Nat = Z | S Nat 

需要注意的是，Vec A類型就是我們所說的家庭類型：每個值n : Nat我們有一個類型Vec A n，向量的長度爲n。

具有其類型的長度允許一些列表函數通過構造來正確。一個簡單的例子是一個安全的表頭功能：

head : Vec a (S n) -> a 
head (x :: xs) = x 

因爲我們要求只有非空載體傳遞給head功能 - 注意指數S n要求的非零值 - 伊德里斯編譯器保證磁頭永遠不會應用於空列表。

其他例子，是矢量的級聯，其確保其結果有長度等於它的參數長度的總和：

(++) : Vec a n -> Vec a m -> Vec a (n + m) 
[] ++ ys = ys 
(x :: xs) ++ ys = x :: (xs ++ ys) 

注意，級聯長度特性由級聯函數類型保證。其他應用是爲了證明對矢量傳統的地圖功能保留其長度：

map : (a -> b) -> Vec a n -> Vec b n 
map f [] = [] 
map f (x :: xs) = f x :: map f xs 

同樣，矢量長度保存由map類型的註釋確保。這些都是非常簡單的示例，說明依賴類型如何通過構建軟件確保正確。

在The Power of Pi中可找到更令人信服的依賴型編程（使用Agda編程語言）的示例。我沒有這樣做，但我相信這篇論文的所有例子都可以毫無困難地移植到伊德里斯身上。