討論 "Universe Polymorphism discussion"

Agda

今後のAgdaの方針を決める討議、本日はUniverse Polymorphismに関して。
Agdaはご存知の通り、非常に厳格なpredicativityに基づいていますが、しかし厳格な可述性は、しばしばデータ型を定義する際の面倒の元になります。例えば

record Cat: Set1 where
Obj: Set
Morphism: Obj -> Obj -> Obj


data M (A: Set):Set1 where
return A -> MA

  • ><- {B: Set} -> M B -> (B -> M A) -> MA

などの圏論をデータ型として表現する場合、上のオペレーター M のソートはSet1 になります。そして、そのソートを持つ圏に対して同じMを定義する場合は新たにM': Set2を定義する必要があり・・・と面倒この上ない。同じようなことは、Power Setを表すオペレーター

P A = A-> Set
P: Set -> Set1

とかでも事情は同じです。もちろん、Agdaでも record構文を使って抜け道的にimpredicativeなデータ型を定義するのは可能ですが、しかしその場合型検査をしてくれないので、あまりよろしくない。抜け道ではなく、正式な対応をするべきではないのか。
という訳で、対策として以下が提案されました：

  1. Set: Set ：これは、もちろんMartin-Lofの1971年論文に基づいており、その体系は実質的には依存型理論+ Type:Type （Martin-Lofの用語では V\in V）ですが、しかしご存知のようにGirardのパラドックスによって矛盾を導きます。その意味で、決して真剣な考慮の対象ではないのですが、まあ、一応候補として。
  2. Impredicativity：タイトなMartin-Lofの直観主義型理論ではなく、もう少しimpredicativityを認める立場を導入したらどうだ、という考え方。Agdaでは (x: Set)-> A : Set1 ですが、Coq. では (x: Set)-> A : Set とできます。この辺でCoqやLegoを見習おう、という主張です。
    1. CC (Calculus of Construction)では (x:Set_{i})\to Set_j: \, Set_{\mbox{max(i,j)+1}} (*) が可能です。これは、j
    2. Coq.やLegoは、実質的にはCCに基づいています。そのため、Coqの方が可述性に関して自由度が高いと言えます。
    3. ちなみに論文は "The calculus of constructions"(Thierry Coquand, Gerard Huet)Information and Computation, Vol.76, (1988) pp.95-120.
  3. スキーム i:level \to Set_i: Sortを導入する、という方法。現在は i はメタレベルの添字として扱われていますが、それを体系内でやってしまおう、と言う話です。これが一番穏健と言えます。
  4. 最後に、厳格性の擁護者からは「現状に何の問題もない」という声が出ました。

という訳で、非常に興味深い議論が戦わされたのですが、結論が出る訳もなく、結局は「各自がそれぞれの解決法を追求しよう」という所に落ち着きました。

（追加）午後は、この話で知らなかった点をN先生とD先生とNに聞いてまわり、情報を集める。Nがこの話を提起したのは、Typesメーリングリストのこのスレッドに触発されたからだそうで。非常に参考になる。