天天看點

沅有芷兮:類型系統的數學之美

昨天的文章删了,因為我的 vscode 把 markdown 裡的 * 自動替換成了 _,導緻一些公式的表述變得異常奇怪。另外,原創忘記打開了。

沅有芷兮:類型系統的數學之美

原文差別不大,看過的,點個看過就好了,多謝!

最近兩周在給 team 教育訓練 rust。雖然去年漢東給我們北京的 team 做過一次 rust 講座,我的好友旭東也跟我布道過不少 rust 的美妙之處,但我真正開始系統性學習 rust,也就是三周之前。對大多數人而言,rust 最令人興奮的是所有權的概念,零成本抽象的能力,以及通過合适的限制巧妙解決記憶體安全和線程安全兩大難題的優雅 —— 記得看過一個統計,linux kernel 裡面這兩類 bug 占據了 1/2 強。也就是說,你隻要學會了 rust,就躺着消弭了 50% 的難啃的讓 kernel developer 都聞之變色的 bug。

但對我來說,rust 的美妙之處在于其為如此底層的語言注入了如此進階的吸收了大量 Haskell 精髓的類型系統。如果你接觸過 Haskell / F# / Scala,你大概能了解我的興奮之處。我們所處的世界往往是魚與熊掌不可兼得 —— Haskell 長于類型系統,但讓程式員失去了對資料在記憶體中如何排布的控制;C 長于對資料在記憶體中的精确控制,但沒有一個像樣的類型系統。rust 幾乎做到了二者兼得。雖然我的 haskell 之旅最終從入門走向了放棄,但就像冰火島上對武功秘籍懵懵懂懂的無忌,那些 monad,monoid,semigroup,sum type,product type 等概念還是烙在我的腦海裡,它們塵封着,等待一個契機,讓自己重見天日。這個契機,便是 rust。

本文借用 rust,談談我對類型系統的一知半解。文章本身和 rust 并不太大,有其它程式設計語言經驗的朋友想必也能讀懂。

primitive type

primitive type,基本類型。基本上每種程式設計語言都有 —— integer,string,bool,array,list/vector 等。它們就像元素周期表裡的一個個元素,不多,但構成了我們這個花花世界。

基本類型沒有什麼好講的,不過在我們深入下面的話提前,我們需要問自己一個問題:什麼是類型?

對于 u8 來說,它是 [0, 255] 之間的一個整數,是一個集合,可以這麼表述:​

​{ x | x ∈ [0, 255]}​

​​。對于 String 來說,它是任意字元串的一個集合,​

​{x | x ∈ ["", "a", ..., "War and Pease", ...]}​

​。

是以,類型在數學上的意義是集合。

product type

product type 是幾乎我們所知道的程式設計語言都有的資料類型 —— 在某些語言中它被稱作 record (delphi, erlang),另一些語言中被稱作 struct (elixir, rust, go) 或者 object (javascript)。我們平時在軟體開發中,最離不開的資料類型就是 product type,就像分子把不同元素的原子組合起來一樣,product type 大大豐富了類型的可能性,進而很好地輔助我們做 DDD (Domain Driven Design)。

我們看 product type 數學上的意義。product type,顧名思義,是不同類型的乘積。類型的乘積究竟是什麼東西呢?假設 x 的定義域是集合 int,y 的定義域是集合 string,x * y 展開便是 (…, -2, -1, 0, 1, 2, …) * (“”, “a”, “ab”, “hello world”, …),也就是說對于 int 裡的任意一個值,都有 string 裡的任意一個值與其配對,看起來有些眼熟對不對?這就是笛卡爾積 (Cartesian product)。如圖所示:

沅有芷兮:類型系統的數學之美

比如在 rust 裡,我們可以這樣為一個 user 模組化:

struct User {
  username: String,
  nickname: String,
  email: String,
  email_verified: bool,
}      

這個 User 類型的集合的取值範圍,就是它内部的所有類型的笛卡爾積。

sum type

笛卡爾積固然能幫助我們建構各式各樣的複合類型,但它無法描述這樣的場景:我們想為 User 添加一個 payment 的類型,它可以是信用卡,現金,微信,以及 ABT 其中的一種。自然,我們可以這樣描述:

enum Payment {
  Creditcard,
  Cash,
  Wechat,
  Abt,
}      

但這樣的類型并不完備 —— 如果使用者選擇了信用卡,那麼需要信用卡号,過期時間,持卡人等資訊,而選擇 ABT,則需要錢包位址及其公鑰。這該怎麼辦?我們需要類似于這樣的類型:

Creditcard(CreditcardType) | 
Cash(f64) | 
... | 
Abt(WalletType)      

在集合論中,這被稱作 disjoint union(不相交集),表述為 A + B。如圖:

沅有芷兮:類型系統的數學之美

不相交集在資料類型中往往被稱作 tagged union (C++) 或者 sum type (haskell, rust)。和 product type 相反的是,大部分程式設計語言沒有 sum type。我們看 rust 是如何使用 sum type 來解決上面的問題的:

struct CreditcardInfo {
  number: String,
  expiration: chrono::NaiveDate,
  holder: String,
}


struct WalletType {
  address: String,
  pk: [u8; 32]
}


enum CreditcardType {
  Creditcard(CreditcardInfo),
  Cash(f64),
  Wechat(AccountInfo),
  Abt(WalletType)
}      

sum type 的美妙之處是它解決了類型系統中基本類型和複合類型潛在的不夠嚴謹的問題,比如說這樣一個函數:

fn div(x: f64, y: f64) -> f64 { x / y }      

從 type signature 上看,似乎沒有問題,但在實作層面上,我們很快發現 ​

​x / y​

​ 有限制條件:y 不能是 0。我們要麼設計一種新的資料類型 non_zero_f64 把零從中排除出去(這在大多數語言裡都很困難),從輸入的角度讓這個函數的 type signature 完備;要麼讓傳回的結果是一種特殊的類型,它可能是 f64,可能為空。

由于大多數語言不支援 sum type,這種情況就隻好用兩種方式來解決:

  • 函數的傳回值可能是 f64,可能是 null。如果一門語言不支援異常,那麼就隻好檢查一下輸入,當為 0 時傳回 null。
  • 函數的傳回值依舊是 f64,但除零的時候會抛出異常。對于支援異常的語言,除了上一種方式,我們還可以抛出異常。

第一種方式損害了類型的完備性,因為 type signature 不再有權威 —— 調用者不敢肯定自己一定會拿回一個 f64,是以隻好也做相應的條件判斷,把這種對于類型的洩露一層層傳遞出去。第二種方式也是對類型完備性的一種損傷,因為調用者需要知道并且選擇處理或者不處理那些「意外」。因為意外不是傳回類型的一部分,是以,額外的邏輯是必不可少的。

上面 div 函數的問題隻是冰山的一角。我們除了學習寫代碼和寫 PoC 的代碼外,其餘的時刻都不可能隻為 happy ending 寫代碼,畢竟我們面對的不是童話世界。錯誤和意外幾乎伴随着任何一次互動 —— 和 IO 的互動,和類庫(别人的代碼)的互動,和系統調用的互動等。Scott Wlaschin 在他著名的 Railway Oriented Programming 裡把一個又一個這樣的情況拎出來尋求解決之道,而 sum type,就是最佳的選擇。

在 Rust 裡,我們有類似于 Maybe Monad 的 Option:

enum Option<T> {
  Some(T),
  None
}      

對于上面的函數,我們可以用 ​

​Option<f64>​

​ 來完善其 type signature:

fn div(x: f64, y: f64) -> Option<f64>;      

當 y 為零,傳回 None;不為零,傳回 Some(x / y)。表面上看它似乎和上面第一種方式沒有差別,但一個形式化完備的類型讓很多事情變成了可能。這個函數可以被 pipe,被 compose,調用者不必擔心類型的洩露 —— 所有資訊都已經在 type signature 裡面了,編譯器可以做更合适更嚴格的檢查,也可以适當優化 —— 更重要的是,圍繞着這個類型,我們可以把一堆原本不斷出現在使用者代碼中的對結果判斷的 if else / try catch 抽象出來,成為 Option 類型的一組 behavior,這樣讓使用者代碼變得清晰。

同樣的思路,在 Rust 裡,exception 被抛棄,取而代之的是是 Result,也是一個 sum type:

enum Result<T, E> {
  Ok(T),
  Err(E),
}      

和 IO 的互動,和别人家的代碼的互動,大家都可以通過 Result 來完成。圍繞着 Result,也有一組标準的 behavior 和宏,處理其結果。

圍繞着程式設計語言是否需要 exception,exception 是良藥還是毒藥,有諸多争議,java / python 是建制派,C++ / haskell 是騎牆派,rust / go 是反對派,erlang / elixir 是無政府主義者,這裡就不展開。你問我支援哪派?我當然是支援尤達大師啦(Do not 也蘊含着 Let it crash 的神韻):

沅有芷兮:類型系統的數學之美

generics type

Generics type,或者說泛型,是讓人又愛又恨的類型。它簡化了代碼,提升了抽象程度,但程式員為之付出的代價是陡升的學習曲線。抛開泛型的好壞不提,我們先看看泛型的數學意義是什麼。還是以 Option 類型來說事:

enum Option<T> {
  Some(T),
  None
}      

T 代表任意類型,Option是 T 映射到這個 enum 的結果。是以換個角度,我們可以認為泛型是作用在類型上的一種特殊的函數,它接受一種或者多種類型,傳回一種新的類型。我們知道,編譯器在處理具體的資料時會将泛型展開,比如說 ​

​Option<u8>​

​ 展開後就是:

enum Option {
  Some(u8),
  None
}      

這種展開可以無限制延伸下去,但彼此又并不想交,就好像 sum type:

enum Options {
  U8(enum { Some(u8), None }),
  U16(enum { Some(u16), None }),
  String(enum { Some(String), None }),
  ...
  VectorU8(enum { Some(Vec<u8>), None }),
  VectorU16(enum { Some(Vec<u16>), None }),
  ...
}      

這個結果就很有意思了。我們知道 sum type 的數學意義是類型之和,我們把 primitive type 記作 X,那麼這裡就有 n 個 X,​

​Vector<T>​

​​ 可以是 ​

​Option<T>​

​​ 的一種類型,因而 ​

​Vector<T>​

​​ 可以展開成 nX,類似 ​

​Vector<T>​

​ 這樣的類型也有 n 個,那麼到現在為止展開的 Options 可以記作 nX + n * nX,同理 HashMap<T, E> 是 n * nX,而 n 個類似 HashMap<T, E> 展開的選項為 n * n * nX,以此類推我們可以得出泛型代表着:

n + n^2 + n^3 + n^4 + ....      

種資料類型的集合。這是一個等比級數,其結果是 ​

​n(1 - n^n) / (1 - n)​

​。

以上。

我們 ArcBlock 還在招募 iOS 工程師和後端工程師,如果你對技術有熱情。想了解更多關于 ArcBlock 和區塊鍊的資訊,可以戳:

​​ArcBlock 一周年​​

繼續閱讀