Coq型推論
型推論は、型を推論するものである。
多相的な型の型パラメータの値は、推論される型じゃないので省略出来ない。
Inductive list (X:Type) : Type := | nil : list X | cons : X -> list X -> list X.
の Xみたいなやつね。
型パラメータを持つ多相的な型のコンスラクタを使うときには、
型パラメータを渡す。
definition mynil := nil nat.
cons nat 1 (nil nat).
*
型推論によって型は省略出来る。
Fixpoint app (X : Type) (l1 l2 : list X) : (list X) := match l1 with | nil => l2 | cons h t => cons X h (app X t l2) end.
は、
Fixpoint app' X l1 l2 : list X := match l1 with | nil => l2 | cons h t => cons X h (app' X t l2) end.
と書ける。
単に引数の型を省略する代わりに
app' (X : _) (l1 l2 : _) : list X :=...
と書ける。
Definition list123' := cons _ 1 (cons _ 2 (cons _ 3 (nil _))).
このように、推論可能な型は[_]で書くことができる。
これを引数同化と言う。そうな