Агда: переписать вместо явного принуждения в определении типа? - PullRequest
Новая
       46

Агда: переписать вместо явного принуждения в определении типа?

0 голосов
/ 08 февраля 2019

Когда речь идет о равенстве типов в Агде, часто необходимо принуждать жителей к типам, используя ручное принуждение, подобное 

coerce : ∀ {ℓ} {A B : Set ℓ} → A ≡ B → A → B
coerce refl x = x

. Обсуждали здесь , что явноиногда можно было избежать применения терминов, используя переписывание.Мне было интересно, если этот метод работал так же хорошо при определении типов.Итак, я написал небольшой пример, где f,g : A → Set - это два (в равной степени) равных зависимых типа и свойство p : A → Set, где p x утверждает, что каждый элемент y : f x равен каждому элементу z : g x, то есть y ≡ z.Последнее равенство не типизировано, как можно ожидать, поскольку y : f x и z : g x не разделяют один и тот же тип априори, однако я надеялся, что переписывание может позволить это.Что-то вроде: 

open import Relation.Binary.PropositionalEquality

postulate A : Set
postulate B : Set
postulate f : A → Set
postulate g : A → Set
postulate f≡g : ∀ {x} → (f x) ≡ (g x)

p : {x : A} → Set
p {x} rewrite f≡g {x} = (y : f x ) (z : g x) → y ≡ z

Но ошибка все еще существует, хотя совет по переписыванию принят.Итак, есть ли способ заставить Агду принять это определение без использования явного принуждения, например 

p {x} = (y : f x ) (z : g x) → (coerce f≡g y) ≡ z

?

Спасибо

1 Ответ

0 голосов
/ 08 февраля 2019

Вот вариант вашего кода, который делает то, что вы хотите: 

open import Relation.Binary.PropositionalEquality

postulate
  A : Set
  f : A → Set
  g : A → Set
  f≡g : ∀ x → f x ≡ g x

p : (x : A) → Set
p x = ∀ y z → R y z
  where
    R : f x → g x → Set
    R fx gx rewrite f≡g x = fx ≡ gx

Почему это работает, если ваша версия не работает?rewrite влияет на две вещи: (а) типы переменных, введенные в шаблоны слева от rewrite;(б) тип цели.Если вы посмотрите на ваш rewrite, когда он вступит в силу, f x не будет найдено, поэтому он ничего не делает.Мой rewrite, с другой стороны, меняет тип fx : f x на g x, потому что fx вводится до rewrite.

Однако я был бы удивлен, если бы этоочень помог тебеПо моему опыту, гетерогенное равенство (то есть равенство между вещами разных типов) остается раздражающим, независимо от того, какие уловки вы бросаете на него.Например, рассмотрим этот вариант вашей идеи, где мы определяем тип R, переписав: 

R : ∀ {x} → f x → g x → Set
R {x} fx gx rewrite f≡g x = fx ≡ gx

R - это гетерогенное отношение, которое «выглядит» рефлексивно.Однако, самое близкое, что мы можем прийти к утверждению, что рефлексивность это 

coerce : {A B : Set} → A ≡ B → A → B
coerce refl x = x

R-refl : ∀ {x} {fx : f x} → R fx (coerce (f≡g x) fx)
R-refl {x} rewrite f≡g x = refl

Без coerce, fx будет иметь неправильный тип, и поэтому мы возвращаемся к проблеме того, что эти принуждения загрязняютнаши типы.Это не обязательно нарушает условия сделки, но усложняет ситуацию.Поэтому я советую избегать разнородных отношений, если это возможно.

...