Агда - разница между типом арг на левой и правой стороне толстой кишки - PullRequest
Новая
       94

Агда - разница между типом арг на левой и правой стороне толстой кишки

1 голос
/ 28 сентября 2019

Следующее определение компилируется и ведет себя хорошо: 

data Eq {lvl} {A : Set lvl} (x : A) : A → Set where
  refl : Eq x x

Однако это определение не компилируется: 

data Eq {lvl} {A : Set lvl} (x : A) (y : A) : Set where
  refl : Eq x x

, потому что 

x != y of type A
when checking the constructor refl in the declaration of Eq

Я не понимаюпочему они не эквивалентныВ чем разница и почему второй вариант не верен?

1 Ответ

1 голос
/ 29 сентября 2019

Аргументы слева от двоеточия называются параметрами;те, что справа, называются индексами.Разница между ними заключается в следующем: в типе возвращаемого значения конструкторов типа данных параметры всегда должны быть точно переменными из объявления типа.Индексы, с другой стороны, могут быть произвольными терминами (правильного типа).

Во втором примере тип возвращаемого значения refl равен Eq x x.Однако y является параметром, поэтому тип возвращаемого значения должен быть Eq x y.В первом примере тип refl является допустимым, поскольку y является индексом, а x является термином типа A.

Под «типом возврата» я подразумеваю выражение длясправа от последней стрелки в типе конструктора.Чтобы проиллюстрировать это, вот определение списков с индексацией длины, известных как векторы: 

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

data Vec (A : Set) : ℕ → Set where
  [] : Vec A zero
  _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)

Тип возврата _∷_ равен Vec A (suc n).Опять же, suc n является произвольным выражением типа ℕ.Если тип данных встречается в типе аргумента конструктора, как в случае с аргументом Vec A n для _∷_, и параметры, и индексы могут быть произвольными терминами (хотя здесь используется один и тот же параметр).

Когда вы сопоставляете шаблон с индексированным типом данных, индекс конструктора может дать вам дополнительную информацию.Рассмотрим head для векторов: 

head : ∀ {A n} → Vec A (suc n) → A
head (x ∷ xs) = x

Нам не нужно писать уравнение для конструктора [], потому что его тип Vec A zero, тогда как тип шаблона Vec A (suc n) и этитипы не могут быть равными.Аналогично, рассмотрим следующее доказательство того, что ваше равенство симметрично: 

data Eq {l} {A : Set l} (x : A) : A → Set where
  refl : Eq x x

sym : {A : Set} (x y : A) → Eq x y → Eq y x
sym x .x refl = refl

Путем сопоставления с шаблоном на refl мы узнаем, что y на самом деле x.Это обозначено точечным узором .x.Таким образом, наша цель становится x ≡ x, что можно снова подтвердить с помощью refl.Более формально, x является унифицированным с y, когда мы сопоставляем refl.

Вы можете задаться вопросом, следует ли просто объявлять все аргументы типа данных в качестве индексов.Я считаю, что в Agda нет недостатка в этом, но это хороший способ объявить аргументы как параметры, если это возможно (так как они проще).

Связанный: раздел руководства Agda ; ТАК вопрос с большим количеством примеров .

...