タグ

集合論と型理論に関するkgbuのブックマーク (1)

  • ヒビルテ(2008-09-05)

    日々の流転 最近、携帯を変えました。MNPを使わなかったので番号が変わります。新しい番号は前の番号(090〜)から、電卓で1003227378をマイナスしたものです。また、メールアドレスはgmailのものを使っています。 λ. 「型の型」問題 LL Future のスタッフ&発表者の打ち上げ*1で「型の型」についての話が出たらしい。 あろはさんのTwitterの<URL:http://twitter.com/alohakun/statuses/904102768>や、東京行ってきた - 黎明日記とそのコメント欄で、その辺りの話が出ていたので、ちょっと簡単な説明を書いてみる。 HaskellとかCCの場合 まず、Haskellの場合。 Haskellでは型の型は「種(kind)」と呼ばれていて普通の型とはレベルの異なるものになっている。つまり、型の型は普通の型ではない。 種について簡単に説明

    kgbu
    kgbu 2008/09/09
    型の型を型にすると、パラドックスを逃れられないから、だそうで。
  • 1