types - 如何在 Agda 中比较 Nats 的向量

Question

我正在尝试使用 Decidable Equality 来比较 Agda 中的两个 Nats 向量。我尝试打开 Vector Equality 模块，将 Nat DecSetoid 作为参数传递，如下所示:

open import Data.Nat
open import Data.Vec

open import Relation.Binary.PropositionalEquality
import Data.Vec.Equality

myFunction : {n : ℕ} -> Vec ℕ n -> Vec ℕ n -> ℕ 
myFunction v1 v2 
  with v1 Data.Vec.Equality.DecidableEquality.≟ v2
... | _  =  {!!}
  where 
    open Data.Vec.Equality.DecidableEquality  (Relation.Binary.PropositionalEquality.decSetoid Data.Nat._≟_) 

但是，我收到以下错误:

Vec ℕ .n !=< .Relation.Binary.DecSetoid (_d₁_6 v1 v2) (_d₂_7 v1 v2)
of type Set
when checking that the expression v1 has type
.Relation.Binary.DecSetoid (_d₁_6 v1 v2) (_d₂_7 v1 v2)

我不确定我做错了什么。我使用的模块系统是错误的，还是我需要以不同的方式使用 ≟？

Answer 1

这里的问题是 where 子句没有为 with 中的表达式带来标识符。因此，当您使用 Data.Vec.Equality.DecidableEquality.≟ 时，您指的不是专门用于自然数向量的向量，而是指 Data.Vec.Equality 中定义的一般向量。这就是为什么 Agda 期望 DecSetoid 作为第一个参数并提示。

一个可能的解决方法是先命名您感兴趣的模块，然后使用限定名称来引用它的 _≟_。我通过 as 定义别名来冒昧地使用较短的名称:

open import Relation.Binary.PropositionalEquality as PropEq
import Data.Vec.Equality as VecEq

module VecNatEq = VecEq.DecidableEquality (PropEq.decSetoid Data.Nat._≟_)

myFunction : {n : ℕ} -> Vec ℕ n -> Vec ℕ n -> ℕ 
myFunction v1 v2 
  with v1 VecNatEq.≟ v2
... | _  =  {!!}