Coq では型も値なので、型にも型がある。 ソートとも呼ばれるが、 あまり気にせずに型と呼ぶことにすると、nat の型は Set である。
Coq < Check nat.
nat
: Set
では、Set の型は何かというと、Type である。
Coq < Check Set.
Set
: Type
さらに、Type の型は何かというと、Type である。
Coq < Check Type.
Type
: Type
しかし、実はここにはごまかしがあって、 見かけどおりに、Type にその Type そのものが属しているというわけではない。
デフォルトでは表示されないが、Type には universe という情報がついていて、 以下のようにすると表示できる。 (CoqIDE なら View -> Display universe levels)
Coq < Set Printing Universes.
Coq < Check Type.
Type@{Top.1}
: Type@{Top.1+1}
(* Top.1 |= *)
universe というのは自然数で、型の型の型の型の... という階層のどのレベルかを示しているのだが、 Type とだけ書いた段階では具体的なレベルは不明なので、不明な値 Top.1 ということになっており、 Type@{Top.1} の型は 1階層上のレベル (Top.1 + 1) の Type@{Top.1+1} となっている。
以下のように T1 と T2 に Type を束縛すると、 universe level は Type の出現ごとに生成される (と思う) ので、 T1 と T2 には別の universe level が割り当てられる。
Definition T1 := Type. Definition T2 := Type.
以下のように、Check で見てみると、T1 の型は Type@{Top.2+1} なので、 T1 そのものの universe level は Top.2 なのだろう。 同様に、T2 そのものの universe level は Top.3 だろう。
Coq < Check T1.
T1
: Type@{Top.2+1}
Coq < Check T2.
T2
: Type@{Top.3+1}
ここで、T1 : T2 という式を Check してみる。
Coq < Check T1 : T2.
T1 : T2
: T2
(* |= Top.2 < Top.3
*)
T1 : T2 というのは T1 の型を T2 に cast するという式である。 この式が成立するには、T1 よりも T2 の universe level が上でなければならない。 この制約が Top.2 < Top.3 として表示されている。 (Coq では、ある universe level の Type は、直上の Type だけではなく、もっと上の Type にも属していると定義されている)
Check で発生した制約は、後には残らない。 残らないので、T1 : T2 という式を Check した後に T2 : T1 という式を Check できる。
Coq < Check T2 : T1.
T2 : T1
: T1
(* |= Top.3 < Top.2
*)
ここではさきほどとは逆に Top.3 < Top.2 という制約が表示されているが、 これはさきほどの Top.2 < Top.3 という制約とは両立しない。
T1 : T2 という式をなんらかの形で環境に登録すると、こうはいかず、 制約は後に残る。 以下のように T1T2 という名前で定義してみる。
Coq < Definition T1T2 := T1 : T2.
そうすると、Check T2 : T1 はエラーとなる。
Coq < Check T2 : T1.
Toplevel input, characters 6-8:
> Check T2 : T1.
> ^^
Error:
The term "T2" has type "Type@{Top.3+1}" while it is expected to have type
"T1" (universe inconsistency: Cannot enforce Top.3 < Top.2 because Top.2
< Top.3).
エラーメッセージにも、Top.3 < Top.2 というのは Top.2 < Top.3 のせいで満たせないと書いてある。
[latest]