agda - 在 Agda 中用证明无关的等价关系重写？

Question

我对类型理论和依赖类型编程还很陌生，最近正在试验 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₂ 应该通过在前面添加一个 . 来声明无关(或者，在最新的开发版本 2.6.0 中，替换为 Prop 类型的等价关系，例如

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

)，这样两个具有相同组件的C实例可以通过refl直接统一，而不管不同的证明eq。但是，无论哪种方式，程序都会停止编译，因为我无法对不相关的值/Prop 进行模式匹配。

我想知道是否有可能以任何方式在 Agda 中实现相同的功能，或者一般来说为什么不可能在 Agda 中用证明无关的等价关系重写(技术支持困难，或者这个打破了 Agda 类型理论的某些部分，等等)？

Answer 1

由于技术限制，目前在 Agda 中这还不可能:'rewrite' 只是 refl 上模式匹配的语法糖，目前不允许在不相关参数上进行模式匹配。在我们的 paper at POPL '19我们描述了一个标准，Prop 中的数据类型是“自然的”，因此可以进行模式匹配。我希望在 2.6.1 发布之前将这个标准添加到 Agda 中，但我不能做出任何 promise (欢迎帮助 Agda 的开发)。