Agda

Question

以下定义编译并运行良好：

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

我不明白为什么它们不等价。有什么区别，为什么第二个变体不正确？

Answer 1

冒号左边的参数称为参数；右边的那些称为索引。两者之间的区别在于：在 return 类型的数据类型构造函数中，参数必须始终是类型声明中的变量。另一方面，索引可以是任意项（正确类型）。

在你的第二个例子中，refl 的 return 类型是 Eq x x。但是，y 是一个参数，因此 return 类型必须是 Eq x y。在您的第一个示例中， refl 的类型是合法的，因为 y 是索引， x 是 A.

类型的术语

'return type' 是指构造函数类型中最后一个箭头右侧的表达式。为了说明这一点，这里是长度索引列表又名向量的定义：

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

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

_∷_ 的 return 类型是 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再次证明。更正式地说，当我们在 refl.

上匹配时，x 是 unified 和 y

您可能想知道是否应该简单地将数据类型的所有参数声明为索引。我相信在 Agda 中，这样做没有任何缺点，但如果可能的话，将参数声明为参数是一种很好的风格（因为这些更简单）。

相关：section of the Agda manual； SO question with more examples.

Agda – 冒号左右两侧类型参数的区别