Agda 类型错误

Posted 2023-02-25

【中文标题】Agda 类型错误

【英文标题】：Agda type error

【发布时间】：2014-03-26 13:15:44

【问题描述】：

我是 Agda 的新手，我正在尝试定义一个常量 prod 类型： Z → (Z → ((Z → Set) → Set))

现在，我编写了以下 Agda 代码：

data Prod (X : Set) : ℕ → X where 
prod : ℕ → (ℕ → ((ℕ → X) → X))

当我对它进行类型检查时，agda 会产生以下错误消息：

X != Set (_33 X_) of type Set 
when checking the definition of Prod 

非常感谢任何帮助

【参考方案1】：

您的数据类型定义有两个问题。首先，所有数据类型都在Set（某种级别）中，您不能到处将数据类型声明为其他类型的元素。

data T : ℕ where

这个定义试图假设还有另一个自然数元素，即T。这没有多大意义。您可以添加更多元素的唯一可能的“类型”是Set - 所有（小）类型的类型。 （我在掩饰Sets 存在无限层级这一事实，您现在不需要处理它）。

所以没关系：

data T : Set where

---

您定义的第二个问题是prod 构造函数的类型并不能反映它确实构造了Prod 类型的东西。构造函数的意义在于它们可以是您定义的类型的元素。

我们来看看自然数的定义：

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

当我们写zero : ℕ 时，我们说zero 是一个自然数。如果我们有这个怎么办：

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

我们正在定义自然数，我们定义 zero 是 String?所以，既然我们定义了构造函数，我们给它的类型必须提到我们在最后一个位置定义的类型。 （这种提及也可以是间接的）。

Op₂ : Set → Set
Op₂ A = A → A → A

data Tree (A : Set) : Set where
  nil  :          Tree A
  node : A → Op₂ (Tree A)

---

您可以在冒号左侧添加参数，您不能在构造函数中更改这些参数。例如，这是无效的：

data T (A : Set) : Set where
  t : T ℕ

请注意，仅T 是不够的——它不是类型，而是从类型到类型的函数（即Set → Set）。这个没问题：

data T (A : Set) : Set where
  t : T A

冒号右侧是索引。这些类似于参数，只是您可以在构造函数中选择值。例如，如果我们有一个按自然数索引的数据类型，例如：

data T : ℕ → Set where

你可以有这样的构造函数：

data T : ℕ → Set where
  t₀ : T zero
  t₁ : T (suc zero)

就像上面一样，T 本身不是一个类型。在这种情况下，它是一个函数ℕ → Set。

---

无论如何，回到您的代码。如果您的意思是 Prod 包含一个 ℕ → (ℕ → ((ℕ → X) → X)) 类型的函数，那么它应该是：

data Prod (X : Set) : ℕ → Set where
  prod : (ℕ → (ℕ → ((ℕ → X) → X))) → Prod X zero

但是，我不知道您对索引的意图是什么。

【讨论】：

回到我的问题，我想定义某种缩写或引用这种类型的常量。现在我已经阅读了您的答案，我意识到新的数据类型将无法完成这项工作.. 所以，我想到了函数，我编写了以下内容并且它有效：prod = X : Set → ℕ → (ℕ → ((ℕ → X) → X)) 但如果我想用它来定义引理，我不知道如何使用它

@ymmagdi：嗯，因为类型是 Agda 中的第一类，你可以有函数接受和返回类型，所以这确实是可能的。例如，看看上面的Op₂ 函数。至于如何使用它——嗯，不知道你想做什么就很难说；如果您遇到困难，请考虑再问一个问题（这比在 cmets 中处理要好），我会看看是否可以提供帮助。