Search code examples
polymorphismcoqdependent-typeparametric-polymorphism

types as parameters in coq


I found this code on this stackexchange post and I'm confused about why it works. In particular,

Inductive Vector {A : Type} : nat -> Type :=
| nil : Vector 0
  | cons : forall n, A -> Vector n -> Vector (S n).

(* This works. *)
Check (let n := 0 in cons n 42 nil).

In the check, is 42 being bound to A? Doesn't A have to be a type? I tried replacing 42 with things that obviously are types, like 'bool' or 'Type', and those worked too. That makes sense to me. But how does 42 typecheck there?


Solution

  • A is an implicit argument for Vector, which (by default) is inherited by the constructor cons. This is indicated by the curly brackets around A : Type in Inductive Vector {A : Type} : nat -> Type.

    Thus, in cons n 42 nil, cons is applied to some implicit type ?A, the natural number n, the element of type ?A 42 and the Vector 0 nil. Since 42 has type nat, ?A can be inferred to be nat.