日々の流転

λ. 「型の型」問題

LL Future のスタッフ&発表者の打ち上げ*1で「型の型」についての話が出たらしい。 あろはさんのTwitterの<URL:http://twitter.com/alohakun/statuses/904102768>や、東京行ってきた - 黎明日記とそのコメント欄で、その辺りの話が出ていたので、ちょっと簡単な説明を書いてみる。

HaskellとかCCの場合

まず、Haskellの場合。 Haskellでは型の型は「種(kind)」と呼ばれていて普通の型とはレベルの異なるものになっている。つまり、型の型は普通の型ではない。

種について簡単に説明する。 例えば、Bool や Maybe Bool などの型は * という種に属する。 また、Maybeという型構築子は * に属する型を受け取って * に属する型を返す関数なので、*→* という種に属する。また、一般化薔薇木のデータ型 data GRose f a = GBranch (f (GRose f a)) で定義される型構築子 GRose は (*→*)→*→* という種に属する。 種の存在意義は型をパラメータとして受け取るような何かを型付けすることだ。 Haskellの場合にはその「何か」には、Maybe :: *→* や GRose :: (*→*)→*→* のような型構築子と、[] :: ∀a::*. [a] や map :: ∀a::*. [a]→[a] のような多相的な式との二つがある。

このようなHaskellの型システムの背景にはFωやλωと呼ばれる型理論が存在していて、Fωにさらに依存型を追加するとCC(Calculus of Construction)やλCと呼ばれる型理論になる。

ところで、型の型が種なら、種の型はなんだということになるが、CCではそれは考えないし、λCでは便宜的に定数記号 □ に属するということにしている。 何故かというと、これらの型理論では種を受け取る「何か」を扱わないから、種の型を考える意味があまりないため。

AgdaとかCoqの場合

CCのような型理論とは毛色の違う型理論もある。

例えば、Agdaの型理論では通常の型はSetに属するがSet自身はSetには属さない。その代わりSet1という型があり、これがSet1を要素かつ部分として含む。さらに、Set2はSet1を要素かつ部分として含み、Set∈Set1∈Set2∈… という風に型の宇宙が累積的階層をなしている。 ある階層に属する型を集めた全体(型の型)は、その階層自身には属さずに一つ上の階層に属するものになる。 つまり、「型の型」は同じレベルの型ではない。

一方、Coqの型理論では通常の型はSetに属してSetはTypeに属している。そして、Typeは構文的にはType自身に属する、すなわち Type∈Type なのだけど、これは文字通りの「Typeの型はType」という意味ではない。 CoqのTypeは実のところ単一の型ではなく、Type と書いたものは実際には適当な自然数αをおいて(Agdaでいうところの) Setα として解釈されている。そして、Type∈Type は実際には Setα∈Setβ と α<β という制約とを表しているのである*2。 なので、意味的にはAgdaの場合と同じで、「型の型」は同じレベルの型でない。

何故「型の型」を型にしないのか?

CCの場合にしても、AgdaやCoqの場合にしても、なんでこんなにややこしい仕組みにしているかというと、素朴に型全体の型SetもSet自身に属すると考えると、ジラールのパラドックス(Girard's paradox)*3が成り立ってしまうため。 ジラールのパラドックスが成り立ってしまうと、論理体系としては矛盾してしまうし、計算的にも強正規化性が成り立たなくなってしまって、まああんまりよろしくない。

2008-09-10追記

ytbさんが Martin-Lofの V∈V 理論とそのパラドックス - あいまいな本日の私 というエントリでジラールのパラドックスについて面白そうなことを書いているのを発見。

λ. 飲み会

• AdS/CFT対応
  • Anti de Sitter space
    • Black hole
    • 5次元の超重力理論
  • Conformed Field Theory
    • 四次元の場の理論 guage theory
  • Juan Maldacena
• 量子色力学 (Quantum Chromodynamics, QCD)
• 大栗博司 (Hirosi Ooguri)
• Atiyah-Singer の K-theory
• Mr. guage 理論 Gerard t'Hooft

ホログラフィー原理の話を知っていたら、ちょっと感動されてしまった。もっとも、私は エレガントな宇宙 や Decoding Universe でちょっと読んだくらいの知識しか知らないのだけど。