Agda – 冒号左侧和右侧类型 args 的区别

Posted 2023-05-08

【中文标题】Agda – 冒号左侧和右侧类型 args 的区别

【英文标题】：Agda – difference between type args on the left and right side of the colon

【发布时间】：2020-01-28 13:20:32

【问题描述】：

以下定义编译并表现良好：

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

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

【问题讨论】：

我很惊讶地发现这个相当基本的问题显然还没有被问到（尽管请参阅我的答案中链接的相关问题）。所以，谢谢你的提问！

【参考方案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 中这样做没有缺点，但如果可能的话，将参数声明为参数是一种很好的风格（因为这些更简单）。

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

【讨论】：

这个答案就它而言很好，但它反映了最近和常见的，但在我看来无益的，从 Dybjer 的归纳家庭中的“参数”和“索引”之间的区别转移。 true 参数不仅在构造函数返回类型中统一使用，而且在数据类型的所有递归使用中都统一使用，因此它可以被抽象为模块参数。有 两种 种索引：遗憾的是，没有公认的术语来区分它们，所以就这样吧。冒号右侧是“特定于返回”的索引。在冒号的左边，我们可以有“return-generic”索引，这些索引在递归使用中会有所不同。

@pigworker，“这样它就可以被抽象为一个模块参数”——如果我们有办法引用当前模块，我们可以抽象一个“可变”参数。喜欢module M n where data Term where Lam : M.Term (suc n) -> Term。最好以这种方式定义像 map : forall B -> (A -> B) -> List -> M.List B 这样的函数（对于在由 A 参数化的模块 M 中定义的 List）。可能是功能请求...

如果发生这种情况，它们将不再是模块“参数”。