トップ «前の日記(2008-08-31) 最新 次の日記(2008-09-06)» 月表示 編集

日々の流転


2008-09-05 [長年日記]

λ. 「型の型」問題

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 理論とそのパラドックス - あいまいな本日の私 というエントリでジラールのパラドックスについて面白そうなことを書いているのを発見。

*1 私は参加してないけど

*2 制約に違反するようなものを書こうとすると、「Error: Universe inconsistency.」とか怒られる。例えば「Definition T : Type := forall X : Type, X->X. Check fun (x : T) => x T.」とか試してみよう。

*3 ジラールのパラドックスについてはここでは説明しないけど、知らない人はラッセルのパラドックスみたいなものと思うと良いと思う。

λ. 飲み会

  • 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 でちょっと読んだくらいの知識しか知らないのだけど。

Tags: quantum
本日のツッコミ(全2件) [ツッコミを入れる]
ψ タナカコウイチロウ (2008-09-09 20:38)

>飲み会<br><br>内容が凄すぎ。人名Atiyah、ですね。Atiyah-Singer といえば、index theory 。hiroki_fさんが、8・27に参考図書のカテゴリーで「指数定理」をあげているので、何か聞けるかもしれない。オジャマしました。

ψ さかい (2008-09-09 22:38)

まあ、「……というのがあって凄く面白い」というのを聞いただけで、私自身はほとんど理解出来てないですけどね (^^;<br><br>> 人名Atiyah、ですね。<br>ありがとうございます。修正しておきました。<br><br>> hiroki_fさんが、8・27に参考図書のカテゴリーで「指数定理」をあげているので<br>そうですね。今度の圏論勉強会のときにでも聞いてみようと思います。