#Agdaだと--type-in-typeオプションでPredicativityを外すことができ，その状態ではFooの例などがwell-typedになりますが，普通やりません．
#Girardのパラドックスが出てきてAgda的にはΩのような"empty以外のbottom"が書けてしまうので論理的にも計算的にも都合が悪いようです．
#そういや対話セッションで:typeInってコマンドあるけどありゃなんだ？って状態です。なんでしょ？:typeOfはまぁ使うので分かりますが。
#:typeInは特定のholeを指定して，その位置でのスコープ内における:typeOfです．
haskell-ja > Archives > 2013/05/18