Well-founded type

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

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s