Это действительно запутанный аспект определений типов данных. Проблема в том, что list1
не эквивалентен list0
из-за того, как индексы и параметры обрабатываются в этих определениях. В жаргоне Coq «индекс» означает аргумент, объявленный справа от двоеточия, как в list1
. «Параметр», напротив, является аргументом, объявленным слева от двоеточия, как A
в list0
.
Когда вы используете индекс, возвращаемый тип выражений match
должен быть универсальным по отношению к индексу. Это можно увидеть в виде list1_rec
, комбинатора для записи рекурсивных определений в списках:
Check list1_rec.
list1_rec
: forall P : forall T : Type, list1 T -> Set,
(forall A : Type, P A (nil1 A)) ->
(forall (A : Type) (a : A) (l : list1 A), P A l -> P A (cons1 A a l)) ->
forall (T : Type) (l : list1 T), P T l
Этот тип говорит, что, учитывая универсальный тип P
, проиндексированный списками и элементом l : list1 A
, вы можете получить результат типа P A l
, сообщив Coq, что возвращать на nil1
и cons1
. Однако тип ветви cons1
(третий аргумент list1
) говорит о том, что ветка должна работать не только для A
, который появляется в типе l
, но и для всех других типов A'
. Сравните это с типом list0_rec
:
Check list0_rec.
list0_rec
: forall (A : Type) (P : list0 A -> Set),
P (nil0 A) ->
(forall (a : A) (l : list0 A), P l -> P (cons0 A a l)) ->
forall l : list0 A, P l
Ветвь cons0
не имеет бита forall A
, что означает, что ветвь должна работать только для типа A
в l : list0 A
.
Это имеет значение при написании такой функции, как map
. В map0
нам разрешено применять f : A -> B
, потому что мы знаем, что аргумент cons0
имеет тип A
. В map1
аргумент cons1
имеет другой универсальный тип A'
, что приводит к этому сообщению об ошибке:
Fail Fixpoint map1 {A : Type} {B : Type} (f : A -> B) (xs : list1 A) :=
match xs with
nil1 A' => nil1 B
| cons1 A' v ys => cons1 B (f v) (map1 f ys)
end.
(* The term "v" has type "A'" while it is expected to have type "A". *)