Переписать с доказательством не относящихся к делу отношений эквивалентности в Agda? - PullRequest
Новая
       16

Переписать с доказательством не относящихся к делу отношений эквивалентности в Agda?

2 голосов
/ 12 апреля 2019

Я довольно новичок в теориях типов и зависимо-типизированном программировании, и недавно я экспериментировал с различными функциями Agda. Ниже приведен очень упрощенный пример, который я написал для типа записи C, который содержит несколько записей компонентов и некоторые ограничения, с которыми мы можем доказать вещи. 

open import Relation.Binary.PropositionalEquality 

module Sample (α : Set) where
  record A (type : α) : Set where

  record B : Set where
    field
      type : α

  record C : Set where
    field
      b₁ : B
      b₂ : B
      eq : B.type b₁ ≡ B.type b₂

    conv : A (B.type b₁) → A (B.type b₂)
    conv a rewrite eq = a

Мне кажется привлекательным, что ограничение eq : B.type b₁ ≡ B.type b₂ должно быть объявлено неактуальным путем добавления . в начале (или, в последней версии dev 2.6.0, для замены отношением эквивалентности вида Prop например, 

data _≡_ {ℓ} {α : Set ℓ} (x : α) : α → Prop ℓ where
  refl : x ≡ x

), так что два экземпляра типа C с одинаковыми компонентами могут быть напрямую объединены через refl независимо от различных доказательств eq. Тем не менее, в любом случае, программа прекращает компиляцию, потому что я не могу сопоставить шаблон с не относящимся к делу значением / Prop.

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

1 Ответ

1 голос
/ 21 апреля 2019

В настоящее время это невозможно в Agda из-за технических ограничений: «перезапись» является просто синтаксическим сахаром для сопоставления с образцом на refl, и в настоящее время сопоставление с образцом для нерелевантных аргументов не допускается. В нашей статье на POPL '19 мы описываем критерий, для которого типы данных в Prop являются «естественными» и, таким образом, могут соответствовать шаблону. Я надеюсь добавить этот критерий в Agda до выпуска 2.6.1, но не могу дать никаких обещаний (помощь в разработке Agda всегда приветствуется).

...