Agda 类型错误

Question

我是 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 

非常感谢任何帮助

Answer 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

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