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 _))).
このように、推論可能な型は[_]で書くことができる。
これを引数同化と言う。そうな

*

さらに
Arguments nil {X}.
Arguments cons {X} _ _.
Arguments length {X} l.

のように、あらかじめ暗黙の引数を宣言しておくことで、
_ も省略して書くことが出来るようになる。

Definition list123'' := cons 1 (cons 2 (cons 3 nil)).

コンストラクタの場合は引数名はどこにも指定されてないので、暗黙の引数宣言では、
_ を使用する。

引数名が指定されてる普通の関数は、変数名を書く。
ようだ。