標籤：

關於Type Driven Development with Idris的粗略總結

04-28

去年4月買來Type Driven Development with Idris這本書，斷斷續續直到今天才看完，可以說是非常龜速了。當然了，看這麼慢肯定是因為慢工出細活啦，才不是因為什麼BOTW什麼MHW的呢(光速逃

這本書看下來還是有不少收穫的，趁著感觸還熱乎，我決定趕緊動(ma)筆(zi)記下來點東西。

兩個核心

這本書看下來，有兩個貫穿全書的核心主題：

  1. type driven development
  2. type driven development with idris

這本書從開始就告訴讀者什麼是type driven development(後文姑且就縮寫為TDD了)，並隨著章節的推進一步步讓你在實際操作中感受TDD到底是什麼。同時這本書也是一本idris教學書，在實踐TDD的過程中逐漸掌握如何使用Idris，以及如何讓Idris幫助開發者實現TDD。

這篇文章也會按著這個思路，從TDD和Idris兩方面來記錄一些我自己的感受。

Idris

作為一個菜雞了多年的Haskell初學者，Idris這樣語法近似Haskell、加入了完整的dependent type、有著感動的互動式開發工具的語言無疑是深得我心的。同時作為一個菜雞Coq初學者，拿Idris刷Software Fundations也是非常因缺斯挺的。

這段時間寫了一些簡短的Idris練手代碼，開發體驗還是非常舒服的。Idris編譯器自帶的互動式開發支持對於配置開發環境來說不要太友好，無論是Atom/VSCode還是Vim/Emacs都可以輕易的配置出一個好用的開發環境。我先後在VSCode和Emacs上配置了idris的開發環境，而兩者加起來大概也就花了10分鐘的時間，還包括了修改鍵位綁定的時間，可以說是非常舒適了。而且由於主要的互動式開發的功能都是由編譯器留出的介面提供的，因此不同編輯器的開發體驗也是十分類似的，比較適合經常在多個不同環境下擼代碼的人。我在Windows上用VSCode和Mac上用Emacs上寫Idris體驗並沒有明顯差異，可以說是非常和諧了。

目前的話Idris已成為我的業餘時間自娛自樂唯一指定語言233，之後應該還會寫一點有趣的東西放出來，這個到時再發文自吹吧(逃

總的來說，個人認為無論是想了解一下函數式編程還是想了解一下dependent type，Idris都是一個很好的選擇。有著純粹的函數式風格、強大的類型系統、和諧的開發環境支持，感覺還是非常適合新人入門的。

Type Driven Development

Type driven development其實就是一套使用類型系統的輔助開發方法。通過這樣的使用方式可以讓類型系統幫助我們避免非常多的麻煩，進而寫出正確的、靠譜的程序。

基本思想

依我個人之見，TDD最基本的思想，同時也是第一步要做的事情就是：用更精確的類型去描述問題。更精確的類型就可以表達更精確的信息、更精準的約束，在類型系統的幫助下就更容易避免某些問題。

舉個例子，假如熊孩子A和熊孩子B鬧矛盾了，準備寫一個兩個數加減乘除的算術測試程序去蹂躪熊孩子B。但你又擔心熊孩子A通過這個測試程序做出種種奇怪的事情，比如偷偷刪掉你珍藏多年的影視學習資料，於是你就得限制熊孩子A可以使用的操作。

這樣一個程序需要的操作其實很簡單，只有：

  1. 生成隨機數
  2. 讀取用戶輸入
  3. 顯示信息
  4. 判斷用戶輸入是否正確

為了防止熊孩子損壞你珍貴的影視資料，你需要禁止熊孩子使用多餘的IO操作，只保留必要的IO操作，也就是列表裡的前三項。於是你定義了如下類型和相應的執行程序：

data QuizCmd : Type -> Type where GenRandom : QuizCmd Integer GetLine : QuizCmd String Display : String -> QuizCmd () (>>=) : QuizCmd a -> (a -> QuizCmd b) -> QuizCmd b runQuizCmd : QuizCmd a -> IO a -- 具體的執行程序懶得寫了=_=

並威脅熊孩子只能用QuizCmd來完成相關的IO操作否則就把隔壁李小花給他寫的情書交給他爹媽。迫於威脅的熊孩子A就只能老老實實的在訂好的框架內做事，而無法通過額外的IO操作搞事。

我們在寫程序的時候，雖然多數情況下在主觀上並不想成為刻意搞事的熊孩子，但總會在無意之中因為疏忽而做出很熊的事情。此時就需要更精細的類型來描述問題並幫助我們避免犯二。我們用越精細的類型來描述問題，類型系統就可以越多地幫我們預防問題。

Type, Define, Refine循環

非常精確的定義出想要的類型並不是一件容易的事情，因此TDD with Idris這本書中提出了"Type, Define, Refine"的循環來幫助我們實現這一目標。這個循環其實很簡單，首先寫出需要的類型(如例子中的QuizCmd)和相關函數的類型(如例子中的runQuizCmd)，然後根據類型信息補全上一步中沒寫的具體操作，最後再審視已經寫好的東西，並思考需要改進的方面。

回到上一個例子里。假如你突然希望，熊孩子只能以如下順序進行IO操作：

GenRandom GenRandom GetLine Display

那此時就需要改進我們的類型來表達這種更具體的約束。這時你就會想到用狀態機來描述這種狀態的變化：

Ready —GenRandom—> GotRandom1

GotRandom1 —GenRandom—> GotRandom2

GotRandom2 —GetLine—> GotInput

GotInput —Display—> Ready

這樣我們就可以改進QuizCmd的定義：

data QuizState = Ready | GotRandom1 | GotRandom2 | GotInput data QuizCmd : Type -> (beforeState : QuizState) -> (afterState : QuizState) -> Type where GenRandom1 : QuizCmd Integer Ready GotRandom1 GenRandom2 : QuizCmd Integer GotRandom1 GotRandom2 GetLine : QuizCmd String GotRandom2 GotInput Display : String -> QuizCmd () GotInput Ready (>>=) : QuizCmd a state1 state2 -> (a -> QuizCmd b state2 state3) -> QuizCmd b state1 state3 runQuizCmd : QuizCmd a Ready Ready -> IO a

如此一來，就只有按指定順序執行指定操作的程序才可以通過編譯了。

就我個人的體會來說，refine這一步是非常重要的。首先，由於TDD會在類型中加入很多信息，經常會出現寫著寫著就被海一樣的編譯錯誤所淹沒的情況。在一步步調整程序使其能通過編譯的過程中，我們很可能就會被海量編譯錯誤搞得頭腦發懵，然後忘記了這段代碼的初衷是什麼。因此在編譯通過以後，從頭審視一下這段代碼就會變得非常重要，這很可能會幫你發現跑偏的代碼片段，或者不小心寫錯的恰好還能通過編譯的不正確的類型。其次就如前文所說，寫出非常精確的類型是一件很難的事情。在沒有豐富的TDD經驗支撐的情況下，使用type define refine循環一步步向精確前進是非常有效的做法。

TDD with Other Languages

誠然，TDD在越強的類型系統中可以發揮的功效就越強，但這並不代表它在稍弱的類型系統中就無法使用。這個話題說實話我也只是有一些模糊的構思，之後有了更清晰的想法以後應該是會單獨再寫一篇的，咕咕咕。

總結

這篇文章其實只是粗略的總結了一下TDD with Idris這本書看下來的一些想法。如果對這本書有興趣的同志們不妨去買來看一看，個人覺得還是物有所值的。

<del>對了，Edwin老哥，廣告費記得轉我支付寶里(逃</del>


推薦閱讀：

※在 Haskell 等語言中是否無法表示 Functor 等的公理？

TAG:Idris | 函數式編程 | dependenttype |