Coq 8.15.2 の manual の Template polymorphism のところを 読んでいて疑問に思ったのだが、なんか Ind-Family の規則が、partial application に対応しているようなのだが、 実装はそうなっていない気がする
Coq 8.15.2, Template polymorphism
ふと思いついて、古い manual を見てみると、 Template polymorphism が入った当初の 8.1 でだけ、(fun A:Set => prod A) という例の結果が異なるようだ
Coq 8.1pl4 の manual:
Coq < Check (fun A:Set => prod A).
fun A : Set => prod A
: Set -> Type -> Set
Coq 8.2pl2 の manual:
Coq < Check (fun A:Set => prod A).
fun A : Set => prod A
: Set -> Type -> Type
prod は 2引数で、引数を 1つしか与えていない prod A は partial application なのだが、 これの型が Type -> Set になるか Type -> Type になるかが異なる
なんとなく、prod A B で、A が Set であっても B が Type だったら prod A B を Set にするのはまずいような気がするので、 実装が正しい、のかなぁ。 実装を直したけれど manual が直っていないという感じか?
さらに manual を読み直した
そーか、具体的に与えた ql から Pl' が決まり、Ci : sqi を成立できるように si が選ばれる、 という仕掛けか
そこで ΓP' は、partial application で ql が与えられなかった部分はそのまま残るから別にいいのか
ということは manual も実装も問題ない、のかな
いや、以下の例では変?
Inductive I (A B : Type) : Type :=
| C1 : A -> B -> I A B
| C2 : I A (B * B) -> I A B.
Check (fun (A : Set) (B : Set) => I A B).
(*
fun A B : Set => I A B
: Set -> Set -> Set
*)
B は recursively non-uniform parameters なので、 Ind-Family の中で B は扱われず、 ΓP' の中で B は Type として扱われ、 C1 : A -> B -> I A B で B が Type なので A -> B -> I A B は Type となる、 はずなのに、Set になっている、と思う
manual に対して実装が拡張されている?
[latest]