什麼是 Type Driven Development ？

解決了軟體開發中遇到的什麼問題 ？

---

EB 那本書里的吧，一言以概，Test-driven development 用測試約束程序行為，Type-driven 用（複雜的）類型系統約束程序行為，讓編譯器強迫你按照某種「正確」方式實現出來。

為什麼其他語言不這麼干呢？因為它們的類型機制沒有強到可以描述邏輯。

Type-driven development is a style of programming in which we write types first and use those types to guide the definition of functions. The overall process is to write the necessary data types, and then, for each function, do the following:

- Write the input and output types.

- Define the function, using the structure of the input types to guide the implementation.

- Refine and edit the type and function definition as necessary.

---

就是防止bug出現的一種手段，通過構造一些命題的證明來實現避免bug出現。

比如，我要取一個數組的第n項，我就要調用一個函數，傳入兩個參數，數組本身和下標，這是常規做法。如果你需要安全性，你就先檢查一下下標是否越界，這個檢查是可選的，不寫就可能出錯。但是在TDD中，你需要再傳一個參數，就是關於這個下標小於長度的證明。這個證明是作為一個GADT呈現的，在運行時可以取掉。

解決了Test-Driven Development中要想達到（保質保量的，對結果有驗證的，不是那種調用一遍就了事的）100% coverage 很困難的問題，但忽視了現在廣大程序員的智商連coinductive data type和inductive data type的區別都搞不懂的問題。

最後那句只是個玩笑，我現在決定改成『但忽視了現在廣大程序員的智商連完整的dependently typed programming和template metaprogramming的區別都搞不懂的問題』（逃

---

我有時候要寫一個 feature，就先讀 code。讀過之後就想：「我就把這個這個變數的類型這麼一改，然後就去 fix compile errors，就行了。」

然後就 fix errors 昏天黑地。腦子裡邏輯都沒了，就是為了 fix errors。

然後突然就成了！

---

你可以想像成用量綱解物理題。

---

這東西和函數式沒必然關係吧？說個C++裡面的玩法：

std::string GetFormData();
std::string SanitizeFormData(const std::string);
void ExecuteQuery(const std::string);


上面的代碼有可能出現隱晦的bug——ExecuteQuery的參數沒有Sanitized。

可以藉助模板避免這個問題：

template &
struct FormData {
explicit FormData(const string input) : m_input(input) {}
std::string m_input;
};
struct sanitized {};
struct unsanitized {};


有人把這個T叫做 "Phantom Type"

現在ExecuteQuery的型參可以帶著冗餘信息，這樣就不會出現之前的bug：

FormData& GetFormData();
std::optional&&>
SanitizeFormData(const FormData&);
void ExecuteQuery(const FormData&);


這就算一個Type Driven Development的實際應用。

以上例子取材自

https://youtu.be/ojZbFIQSdl8?

youtu.be

---

Type-Driven Development with Idris

---

你知道Score Oriented Programming么？學生做project的時候，submitter提交出來能跑滿分就是好程序。沒有滿分我就改個參數再交一遍看看，直到submitter給出滿分為止。Type Driven Development感覺和Score Oriented Program差不多（大霧

---

俺覺得可以簡單粗暴地理解為面向防呆編程（逃

---

未來程序語言的方向之一，就像現在的資料庫，約束外鍵用上，數據就沒那麼容易出錯，就算程序有漏洞都不行

---

推薦閱讀：