haskell-ja > Archives > 2013/05/17

2013/05/17 00:03:10 UTCcutsea110
#
あ、「全体が○○となって…」と言いましたがそうなるようなものが構成できる可能性があるということです。もちろん。
2013/05/17 11:22:20 UTCLost_dog
#
CPDTだと、ここの最初の2節に書いてありました > Library Universes http://adam.chlipala.net/cpdt/html/Universes.html
2013/05/17 11:26:23 UTCLost_dog
#
でもあんま詳しくは書いてないですね…
#
インデックスはPredicativity制約があって、自身より真に小さいレベルの型しか持てないが、パラメーターはインデックスほど柔軟でないので、自身と同じか小さいレベルの型が持てるんだよ、的な説明が
2013/05/17 14:39:31 UTCcutsea110
#
それが答なんですね.
#
Predicativity制約ってのは?
2013/05/17 14:54:05 UTCcutsea110
#
述語制約って見つかるのがそうかな.意味的にはまさにパラドックスがでてくる可能性があるから階層を分けないとダメってやつのことかな.
2013/05/17 16:52:45 UTCLost_dog
#
僕もCPDTのその部分を読んだだけなので、詳しく知るにはCICまわりを追ってみる必要がありそうですね。。その辺の歴史がまとまってる読み物があると嬉しい…