形式驗證、依賴型別與動態型別
aka 依賴型別傳教文
推薦閱讀我的部落格的版本，你可以點選網頁的程式碼塊裡面的變數名，可以跳轉到定義。
前排提醒：你或許 不 需要一個遊標卡尺。
本文面向一切有任何形式程式設計經驗的讀者，將會使用 Agda 和極少量其他語言展示程式碼例子。 讀不懂的程式碼可以藉助附近的文字描述理解它的含義，所以不用擔心語言問題。
一切規矩照舊，這篇文章是一個 Agda 模組，我們匯入一些基本庫：
{-# OPTIONS --no-unicode #-}
{-# OPTIONS --without-K#-}
{-# OPTIONS --safe#-}
module DependentFunctionsVersusDynamicTyping where
open import lib.Basics
這次，我們需要使用 ofollow,noindex">HoTT-Agda 中的自然數型別的相關定義：
open import lib.types.Nat
泛化階：
variable i : ULevel
本人承諾不會在這種面向非 Agda 專業人士的文章裡使用 Unicode 。
在這個沒有 null 的語言裡，我們有時還是需要使用 null 的：
data Nullable {i} (A : Type i) : Type i where
nullptr : Nullable A
new_: A -> Nullable A
這樣， nullptr 和 new 1 都是 Nullable Nat 型別的例項了（這些符號馬上就介紹）：
_ = nullptr :> Nullable Nat _ = (new 1) :> Nullable Nat
依賴型別的陣列
定義一個數組型別，陣列長度是型別的一部分：
infixr 5 _cat_
data Vec {i} (A : Type i) : Nat -> Type i where
[]: Vec A O
_cat_ : forall {n} -> A -> Vec A n -> Vec A (S n)
這樣，我們可以有空陣列，以自然數型別為例：
_ = [] :> Vec Nat 0
其中， :> 左邊是一個表示式（在這裡是 [] ），右邊是它的型別。 _ = 表示把這個表示式賦值給一個無法被使用的變數，也就是丟掉這個表示式。 以這種形式寫出來，我就可以在編譯我的部落格的時候讓 Agda 編譯器檢查我的這些程式碼片段是否在型別上是正確的。
把程式碼編譯成網頁是 Agda 編譯器的一個功能，我目前正在著手改善它的這個功能。 也就是說，如果我給我的部落格寫一個 main 函式，我就可以執行我的部落格了……
先不說這個，一個元素的陣列，也就是一個元素和一個空陣列連線的結果：
_ = (233 cat []) :> Vec Nat 1
兩個元素：
_ = (666 cat 233 cat []) :> Vec Nat 2
觀察發現，陣列的型別 Vec 有兩個引數，第一個引數是元素的型別 Nat ，也就是自然數，第二個是長度，這兩個引數都是編譯期已知的。 這個陣列的定義常常被 Idris 語言的粉絲用於佈道——因為它很安全，可以在編譯的時候防止越界的情況發生，就像 C++ 程式員會推薦 std::array 一樣。 而由於 Agda 語言人氣不足，別人佈道的時間 Agda 程式設計師都寫論文去了。
我們來嘗試一下 Agda 的『小於』型別。小於關係是一個型別，如果我們有一個型別為 a < b 的變數，那麼我們就『證明』了 a < b 。 也就是說，我們可以弄出一個型別為 3 < 4 的變數：
_ = ltS :> (3 < 4)
也可以有 114514 < 114516 型別的變數：
_ = ltSR ltS :> (114514 < 114516)
但是我們無論如何也弄不出 1 < 1 型別的物件——這是由 < 的定義決定的，這裡就不展開說了（涉及的東西有點多）。
因此，我們可以寫出這樣一個函式：它『從長度為 m 陣列中獲取第 n 個元素』，並要求呼叫這個函式的人額外傳入一個 型別為 n < m 的變數。
module GetAtIndex where
_!!_<[_]> : {A : Type i} -> forall {l} -> Vec A l
-> (n : Nat) -> n < l -> A
(x cat _) !! O <[ _ ]> = x
(_ cat a) !! S n <[ p ]> = a !! n <[ <-cancel-S p ]>
這樣，有了 n < m 的證明，我們無論如何都能安全地從數組裡拿出一個元素了。 舉一個簡單的呼叫的例子。這是一個測試用的陣列：
sampleList : Vec Nat 4 sampleList = 0 cat 1 cat 2 cat 3 cat []
我們試圖取它的第 2 項，沒有問題（下面的程式碼是讓編譯器試圖驗證『從剛才那個陣列中取第 2 項得到的是 2』）：
_ = idp :> ((sampleList !! 2 <[ ltSR ltS ]>) == 2)
試試第一項？
_ = idp :> ((sampleList !! 1 <[ ltSR (ltSR ltS) ]>) == 1)
執行時錯誤
module RuntimeErrors where open GetAtIndex
一個老生常談（我在兩個群裡被問過了）的問題：如果下標和陣列都是執行時獲取的，編譯器的驗證不就涼了嗎？
解決方法：在執行時進行判斷——如果下標小於陣列長度，那麼在這樣的條件下可以得到一個小於關係的證明， 就可以安全地進行函式呼叫。否則，你將不能呼叫這個函式，請自行處理非法輸入。
給出一個簡單的實現（庫裡面其實有一個 Decidable 的版本，但是它裡面用了 Unicode ，我不想用，所以就自己寫了一個）。 首先，我們需要判斷兩個自然數的大小，並在小於的時候返回小於的證明，其他時候返回 nullptr ：
lessThan : forall a b -> Nullable (a < b) lessThan O O = nullptr lessThan O (S b) = new O<S b lessThan (S a) O = nullptr lessThan (S a) (S b) with lessThan a b ... | nullptr = nullptr ... | new x= new <-ap-S x
然後，我們就可以在不模式匹配、直接把引數拿來用的情況下，對 _!!_<[_]> 進行呼叫了。 這個函式通過接收任意的自然數和任意的陣列來模擬執行時無法保證的輸入，並返回可能不存在的輸出：
runtimeInput : forall {m} -> Vec Nat m -> Nat -> Nullable Nat
runtimeInput [] _ = nullptr
runtimeInput{m}vn with lessThan n m
... | nullptr = nullptr
... | new x= new (v !! n <[ x ]>)
這個函式和 Java、JavaScript 函式就沒什麼可見的區別了，這也體現出了形式驗證的一個小小的侷限性。
但在執行時的情況下，我們還是能看出形式驗證的好處的——型別簽名裡函式對引數需要滿足的關係以非常清晰的形式呈現了（比如， a > b 這種表示式），表達的也很簡潔， 函式的呼叫者無需閱讀文件即可安全地進行 API 呼叫，執行時不需要任何錯誤處理——編譯的時候就能保證所有的錯誤得到處理，執行時當然是把這些東西全部都擦除掉了。
稍微弱一點的型別系統
看到這裡，我們會想起，像 Java 和 JavaScript 裡類似的函式都會在引數不合法的時候丟擲一個異常。 因此，如果我們的程式要足夠健壯，我們會選擇：
- 處理這個異常
- 判斷下標是否小於長度，提前避免錯誤
具有證明命題能力的程式語言一般會強制程式設計師進行後者的操作，具有責任心的程式設計師會主動進行後者的操作， 絕大多數時間我們是忽略了這件事的——編譯器、程式設計師、使用者都沒有去證明輸入資料對程式來說一定合法。 當輸入不合法時（儘管這很少發生），我們的程式會崩潰掉（ 執行時錯誤 ），否則將正常執行。
執行時錯誤，從動態型別到靜態型別的過程中已經大幅減少了。但這裡可以看出，它還是存在的。
不知道 C++ 程式設計師有沒有想到 SFINAE 呢？（笑）
但總而言之，把證明傳來傳去是一件很麻煩的事情，光是閱讀命題本來就是額外工作，證明就更麻煩了。 像 C++ 的 SFINAE，在引數不合法的時候，如果不手動讓編譯器丟擲一些可讀的異常，編譯器會產生大量的錯誤資訊， 印在廁紙上都能用一年。
但是呢，會把程式寫成這樣的形式驗證研究員都是垃圾（憑空製造複雜度），他們的思維都被限制了。
我們首先來看看大家覺得雖然邪惡但是寫起來爽的『動態型別』。
更淺顯的話題
程式設計師們常常對『動態型別和靜態型別哪個更好』這一話題產生激烈的討論。 這其實是一個完全沒有意義的討論，因為這首先是一個羅卜白菜的問題——兩者都有能稱得上是『優點』的地方； 其次不同的人對程式有不同的追求，有人想寫出健壯可擴充套件的程式，有人只是想快速交付收錢； 再其次同一個人也有不同的需求，有時只是想批量處理一些檔案，有時需要構建長期維護的大型專案。
對於簡單的批處理需求，我們甚至會完全不考慮任何的可讀性、可維護性、可擴充套件性、安全性、魯棒性， 寫出類似這樣的程式碼（已經整理過了，再看不懂就是語言的問題）：
while (my $line = <$imguiHeader>) {
chomp $line;
$_ = $line;
if (m!^// dear imgui, (.*)$!) {
my $commandPrefix = 'cd ../imgui && git rev-parse';
print "--- Generating for dear-imgui version $1\n", "--- Revision ", `$commandPrefix --verify HEAD`;
print "--- Branch ", `$commandPrefix --abbrev-ref HEAD`, "---\n\n", "local $moduleName = { _version = '@{[ $1 =~ s/[^∙↓]//gr ]}' }\n";
}
elsif (/^\s*enum\s(\w+)_/) {
$currentEnum = $1;
$currentEnumMangled = $currentEnum =~ s/^Im(Gui)?(.)([^\s]*)$/@{[ lc $2 ]}$3/r =~ s/Flags$//gr;
# =~ s/([a-z])([A-Z])/$1.@{[ lc $2 ]}/gr;
print "\n", '--{', '{', "{ $currentEnumMangled\n", "---\@type _$currentEnumMangled\n", "local $currentEnumMangled = {}\n"
}
elsif (length $currentEnum) {
if (/\}/) {
print "$moduleName.$currentEnumMangled = $currentEnumMangled\n";
print "$currentEnumMangled = nil\n", '--}', '}' "} $currentEnumMangled\n";
$currentEnum = ''; $previousDefault = 0;
}
elsif (m!^\s*${currentEnum}_(\w+)((\s*=\s*([^,/]+))?),?\s*(//\s*(.*))?!) {
print "\n--- $6\n" if $5 and length $6;
$mangledName = length $1 == 1 ? "_$1" : $1;
$value = $2 ? calculate $4 : $previousDefault++;
print "$currentEnumMangled.$mangledName = ", $value, "\n";
}
elsif (m!^\s*//(.*)!) { print "---$1\n" }
}
}
這樣的程式碼完全是一個精雕細琢的藝術品——它的每一個字元都是我（沒錯這是我寫的……用來提取一段 C++ 程式碼中的一部分定義並翻譯成 Lua） 小心翼翼寫出來的，稍微改一點就會出錯，輸入資料有一點點變化也可能出錯，靜態分析工具對這個程式碼的正確性完全沒有保障（Perl 的直譯器在執行你的程式碼的時候也不知道你的程式的目的，只是一行一行地執行而已）。
動態型別往往因為其靈活性被一些程式設計師（不是我）喜歡。比如我們可以寫出這樣的 JavaScript 程式：
const Error = {}
const getAtIndex = (a, n) => n < a.length ? a[n] : Error;
簡單地執行：
> getAtIndex([1, 2, 3], 2)
< 3
> GetAtIndex([], 1)
< {}
這個 getAtIndex 接收一個數組和一個整數，返回『有時是一個數組元素，有時是 Error 』。 用 TypeScript 描述一下它的型別，就是：
<a>(a[], number): a|Error
而我們呼叫這個函式，它到底會返回什麼型別，我們也必須看它的實現才能知道。 返回 Error 只是方便起見，我們大可使用異常來代替返回一個表達異常的物件。 但它做到了一點——在我們不想處理錯誤的時候，我們可以不處理錯誤，讓執行時炸。 在我們想處理錯誤的時候，我們可以處理錯誤。
但這給了我們一個啟發。或許我們可以實現這樣的函式：在很明顯沒有錯誤的時候，我們可以不處理錯誤。 在有可能錯誤的時候，我們需要處理錯誤。
或許有人會說，我們不還有異常嗎？但首先異常這一概念首先本身就足夠『執行時』， 我們對什麼樣的函式會丟擲什麼樣的異常都一無所知。Java 的 Checked Exception 作為一個例外，是靜態的異常， 但是這種語法結構和返回帶有錯誤資訊的型別 （可以理解為 Haskell 的 Either ， Rust 的 Result ） 是同構 的 （這篇文章本身說的很有道理，但請不要看它所引用的《給 Java 說句公道話》）。
首先，寫 C# 程式碼時最讓我頭痛的事情之一，就是 C# 沒有 CE。每呼叫一個函式（不管是標準庫函式，第三方庫函式，還是隊友寫的函式，甚至我自己寫的函式），我都會疑惑這個函式是否會丟擲異常。由於 C# 的函式型別上不需要標記它可能丟擲的異常，為了確保一個函式不會丟擲異常，你就需要檢查這個函式的原始碼，以及它呼叫的那些函式的原始碼……
在靜態型別中，我們要麼使用靜態的帶錯誤資訊的返回型別（強制檢查錯誤，即使很明顯的正確的程式碼也必須處理錯誤）、要麼使用異常（靜態變動態，你幹啥不去用 Python）。
而且，剛才那段 JavaScript 根本不可能在靜態型別語言裡實現（當然，這裡沒有考慮支援和型別的語言。但是要考慮到 支援和型別的程式語言大部分都是漸進型別或者以動態型別程式語言為目標語言的程式語言）——我們寫不出一個同時有兩種可能的返回型別的語言。
也就是說，動態型別能做（即使做的不完美，比如那個 getAtIndex 並不會強制你處理異常，即使可能異常）的事靜態型別做不到； 靜態型別能做動態型別做不到的事就多了去了，在絕大多數情況下使用靜態型別還是能帶來遠高於動態型別的程式設計體驗的（ 包括 IDE 補全重構跳轉、儘可能減少了型別錯誤等），這裡就略過不提了。
難道魚和熊掌真的不可兼得嗎？
不，小孩才做選擇。
我全都要
module IQuanDouWant where open RuntimeErrors
這時我們就需要用到依賴型別了。
我們除了傳入證明作為引數之外，還可以使用依賴函式！
我們的 getAtIndex 函式，在下標越界的時候返回 Error ，其他時候返回正常的值。 我們先定義一個表達錯誤的型別：
data ???? : Type0 where ??? : ????
我們的函式 getAtIndex ，返回的型別，是根據兩個引數決定的。 所以，我們需要先寫一個函式，接收兩個自然數，返回『我們的 getAtIndex 的返回型別』， 也就是說如果左邊大於右邊，就返回『自然數』這個型別，否則返回表達錯誤的型別。 請注意，只有帶有較好的依賴型別支援的型別系統才能做到這種事。如果一個語言聲稱自己支援依賴型別， 你可以問問他能不能寫出這樣的程式碼。
returnType : (_ _ : Nat) -> Type0 returnType O _ = ???? returnType (S _) O = Nat returnType (S n) (S m) = returnType n m
然後，我們的 getAtIndex 需要返回的，就是這個型別。
getAtIndex : forall {m} -> (v : Vec Nat m) -> (n : Nat) -> returnType m n
getAtIndex [] _ = ???
getAtIndex (x cat _) O = x
getAtIndex (_ cat v) (S n) = getAtIndex v n
看看看！這個函式的實現真的好簡單啊！
我們試試證明它的性質？我們先傳入合法的引數，看看是不是就直接返回了陣列的元素：
open GetAtIndex using (sampleList) _ = idp :> (getAtIndex sampleList 2 == 2) _ = idp :> (getAtIndex sampleList 1 == 1)
真的耶！那如果是超過長度上限的下標，是不是就會返回那個錯誤型別呢？
_ = idp :> (getAtIndex sampleList 233 == ???)
是的！
這個函式的返回型別真的在變耶！而且這是非常非常純正的靜態型別程式設計哦！
你看，靜態型別做不到的事，依賴型別做到了。動態型別沒法編譯期進行型別檢查，依賴型別可以。
實際應用
module FSharpLang where -- ...
就懶得寫了，畢竟本來就是我的另一篇部落格。這是一個依賴函式的經典應用—— printf 。 它的型別是： String -> ?? ，其中 ?? 具體的值，取決於 String 引數中有多少個 %d , %c 等。
啊，今泉影狼真可愛啊。