id

id関数

任意の型 A の引数をとり、それ自身を返す関数

Coqは、

変数名 : 型 

の順序でいろいろ宣言する。変数も、関数の引数も。
一番最初のもの。http://www.iij-ii.co.jp/lab/techdoc/coqt/coqt1.html

Definition id (A : Type) (x : A) : A := x.

型引数A (A:Type) と型Aの変数x(x:A)を引数に取る関数でA型を返却する。(: A)その本体は、:=で定義され、本体は、x

実行

Eval compute in id nat 10. (* => 10. *)

Coqは型推論があり、(x : A)で宣言されたxからなる本体があるので、戻りの型は自明。ゆえに以下のようにも書ける。

Definition id2 (A : Type) (x : A) := x.

無名関数バージョン

Definition id3 := fun (A : Type) (x : A) => x.

しかしこれは、変数id3の型を(型推論を頼って)省略した書き方。
型つきバージョンは以下のもの。

Definition id4 : forall (A : Type), A -> A := fun (A : Type) (x : A) => x.

id4は forall (A : Type) において、A型の変数を取ってA型を返す(A -> A)関数。
その本体は、:= 以降に定義されてる。

基本的な考えはCやjavaの

型 変数名 = 値

int n = 10;

などと書き方は違うけれども、本質？は変わらない。関数がその場で定義して変数に放りこめるのが、java7までのjavaとか、Cとかと違うけれど、考えかたは同じだと思う。変数には、型があり、変数といっしょに宣言する。と。

型推論に頼って型を省略したものが次

Definition id5 : forall (A : Type), A -> A := fun (A : Type) x => x.
Definition id6 : forall (A : Type), A -> A := fun A (x : A) => x.

そして、

Definition id' : forall (A : Type) , A -> A := fun A x => x.

と、http://www.iij-ii.co.jp/lab/techdoc/coqt/coqt1.htmlの記述につながる。
昔見たとき、
fun A x => x
という書き方がすげい謎だったけど、今なら少しだけ分かる。よかったよかった。

しかし、HaskellやOCamlで、
id :: a -> a
id x = x
のように書けるって書いてあるのに、Coqにおいては、型変数を明示的に渡さなければならないのは微妙に納得いかないけど、この文法なら仕方なしか。