在看 OTT 的時候發現只有 bottom, unit, bool 這三種基本的 type 跟 , 前面五種都好理解, 然而最後一個 W-types 就夠了嗎? 結果回頭看了 Martin-Lof 的 ITT, 以及 Peter Dybjer, Anton Setzer 寫的東西以及 McBride 做的 Ornament 三個 constructor 之一的 arg 就是 W-types …
類別： 閒聊 Tagged: type theory
