Predicativity
超討厭 = =。看來真的沒辦法把 sets 的層級壓下來。那…全部提上去如何?Coq 裡面好像已經有 universe polymorphism,那乾脆把 AoPA 移植到 Coq 算了 XD。
--
顯然我的潛意識認為寧可把 AoPA 整個翻修一遍也不要再造那麼多版本的 arrows XD。
看來目前還是 scm 老師說的 "specialised versions" 比較可行一點點。不如就寫得很醜很醜,然後當作支持 universe polymorphism 的好理由 XD。
--
前途一片黯淡啊 XD。
Labels: 雜記
聽起來又是一個很耗工程的事
<< 回到主頁