Почему средство проверки типов coq отклоняет мое определение карты? - PullRequest
Новая
       39

Почему средство проверки типов coq отклоняет мое определение карты?

1 голос
/ 03 мая 2019

Я пытаюсь поэкспериментировать с определением списка.Например, давайте посмотрим на это определение: 

Inductive list1 : Type -> Type := nil1 : forall (A : Type), list1 A
                               | cons1 : forall (A : Type), A -> list1 A -> list1 A.

Вы можете подумать, что приведенное выше определение эквивалентно этому: 

Inductive list0 (A : Type) : Type := nil0 : list0 A
                                   | cons0 : A -> list0 A -> list0 A.

Почему эта карта: 

Fixpoint map0 {A : Type} {B : Type} (f : A -> B) (xs : list0 A) : list0 B :=
  match xs with
    nil0 _ => nil0 B
  | cons0 _ v ys => cons0 B (f v) (map0 f ys)
  end.

принято, но это не так: 

Fail Fixpoint map1 {A : Type} {B : Type} (f : A -> B) (xs : list1 A) :=
  match xs with
    nil1 _ => nil1 B
  | cons1 _ v ys => cons1 B (f v) (map1 f ys)
  end.

?

Ответы [ 2 ]

1 голос
/ 03 мая 2019

Это действительно запутанный аспект определений типов данных. Проблема в том, что 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". *)
0 голосов
/ 06 мая 2019

Чтобы завершить, вы можете определить функцию map over list1: 

Fixpoint map1 {A : Type} {B : Type} (f : A -> B) (xs : list1 A) :=
  match xs with
  | nil1 A' => fun _ => nil1 B
  | cons1 A' v ys => fun f => cons1 B (f v) (map1 f ys)
  end f.

Это пример так называемого шаблона конвоя .Обычно нужно добавить предложение return к конструкции match, чтобы она проверяла типы, но здесь Coq достаточно умен, чтобы вывести его.

Однако я, конечно, не рекомендую использовать это определение списков, так как онобудет громоздким для использования в подобных случаях.

...