Agda –结肠左侧和右侧的args类型之间的差异

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

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

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

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

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

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

_∷_的返回类型为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证明。更正式地说，当我们在x上进行匹配时，unified是y与refl。

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