типы как параметры в coq

Question

Я нашел этот код в этом стековом сообщении , и я не понимаю, почему он работает. В частности,

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).

При проверке 42 связан с A? А не должен быть типом? Я попытался заменить 42 вещами, которые, очевидно, являются типами, такими как «bool» или «Type», и они тоже работали. Это имеет смысл для меня. Но как там 42 проверки типов?

Answer 1

A - это неявный аргумент для Vector, который (по умолчанию) наследуется конструктором cons. На это указывают фигурные скобки вокруг A : Type в Inductive Vector {A : Type} : nat -> Type.

Таким образом, в cons n 42 nil, cons применяется к некоторому неявному типу ?A, натуральному числу n, элемент типа ?A 42 и Vector 0 nil. Поскольку 42 имеет тип nat, ?A можно сделать выводом nat.