2008/04/25

Predicativity

超討厭 = =。看來真的沒辦法把 sets 的層級壓下來。那…全部提上去如何?Coq 裡面好像已經有 universe polymorphism,那乾脆把 AoPA 移植到 Coq 算了 XD。

--
顯然我的潛意識認為寧可把 AoPA 整個翻修一遍也不要再造那麼多版本的 arrows XD。


看來目前還是 scm 老師說的 "specialised versions" 比較可行一點點。不如就寫得很醜很醜,然後當作支持 universe polymorphism 的好理由 XD。

--
前途一片黯淡啊 XD。

Labels:

Blogger yen34/25/2008 1:02 pm 說:

聽起來又是一個很耗工程的事

 

<< 回到主頁