Canonical の最低限の例を作ってみた。
適当にレコードを定義して、そのメンバのひとつ (RecT) は型であり、 :> とすることで型の文脈で使われたらそのメンバが自動的に使われるよう coercion も定義する。 RecT 以外になにもないと寂しいので、特に意味は無いが、nat 型の RecN メンバも加える。
Record rec := Rec { RecT :> Type; RecN : nat }.
rec 型の値を適当に定義する。
Definition bool_Rec := Rec bool 0.
rec 型の値と、その値を型とする値を受け取る関数を定義する。
Definition f (T : rec) (x : T) := 0.
coersion を表示するように設定すると、以下の RecT T というように、T の中から取り出した RecT メンバを型として扱って、 それが引数の型となっていることがわかる。
Check f. (* f : forall T : rec, RecT T -> nat *)
ここで、f _ true として、f の適用で、第1引数 T を省略してみると、T がなにかわからないので失敗する。
Fail Check f _ true. (* The term "true" has type "bool" while it is expected to have type "RecT ?T". *)
Canonical で bool_Rec を登録する。
Canonical bool_Rec.
再度 f _ true として、T を省略してみると、今度は T に bool_Rec が埋められて成功する。
Check f _ true. (* f bool_Rec true *)
もちろん、T を bool_Rec で埋めていいのは f の第2引数 x が bool のときだけである。 なので、f _ 0 は依然として失敗する。
Fail Check f _ 0. (* The term "0" has type "nat" while it is expected to have type "RecT ?T". *)
SSReflect の eqType もこの機構を使っている。 eqType の場合は、(上記の RecN のかわりに) 同値性を判定する関数と、その関数が本当に同値性である (反射律、対称律、推移律を満たす) という証明が入っている。 x == y は @eq_op eqtype x y のことで、eq_op は eqtype から同値性を判定する関数を取り出して x と y に適用するというしかけになっている。 x == y という記法では eqtype を記述しないのだが、Canonical により x と y の型から Canonical で指定されたもの (bool_eqType とか nat_eqType) が埋められる。 あと、eqtype に入っている証明は (x == y) = (y == x) などといった定理の証明に使われる。
[latest]