Agda型误差

Question

我是Agda的新手，我试图定义一个类型为prod的常量Z → (Z → ((Z → Set) → Set))：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 --所有(小)类型的类型。(我想说明的是，Set的层次结构是无限的，您现在不需要处理这个问题)。

所以这没问题：

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

然而，我不知道你对指数的意图是什么。