Agda中的参数化归纳类型

Question

Agda中的参数化归纳类型

15

我正在阅读Dependent Types at Work。在参数化类型的介绍中，作者提到在这个声明中：

data List (A : Set) : Set where
  []   : List A
  _::_ : A → List A → List A

List 的类型是 Set → Set，而 A 成为这两个构造函数的隐式参数，即：

List 的类型是 Set → Set，并且 A 成为这两个构造函数的默认参数。

[]   : {A : Set} → List A
_::_ : {A : Set} → A → List A → List A

好的，我试着以稍微不同的方式重写它。

data List : Set → Set where
  []   : {A : Set} → List A
  _::_ : {A : Set} → A → List A → List A

很遗憾，这并不起作用(我尝试学习Agda已经两天左右了，但根据我所了解的，这是因为构造函数参数化在Set₀上，因此List A必须在Set₁中)。

事实上，以下内容被接受：

data List : Set₀ → Set₁ where
  []   : {A : Set₀} → List A
  _::_ : {A : Set₀} → A → List A → List A

然而，我不再能使用{A : Set} → ... → List (List A)（这是完全可以理解的）。

所以我的问题是：List (A : Set) : Set和List : Set → Set之间的实际区别是什么？

感谢您的时间！

- Vitus

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- danr · Accepted Answer

我在这里自作主张地更改了数据类型的名称。第一个数据类型，也就是以 Set 作为索引的将被称为 ListI，第二个数据类型 ListP 则带有一个 Set 参数：

data ListI : Set → Set₁ where
  []  : {A : Set} → ListI A
  _∷_ : {A : Set} → A → ListI A → ListI A

data ListP (A : Set) : Set where
  []  : ListP A
  _∷_ : A → ListP A → ListP A

在数据类型中，参数出现在冒号前面，而冒号后面的参数称为索引。构造函数可以以同样的方式使用，您可以应用隐式集合：

nilI : {A : Set} → ListI A
nilI {A} = [] {A}

nilP : {A : Set} → ListP A
nilP {A} = [] {A}

当进行模式匹配时，它们之间的区别就出现了。对于索引版本：

null : {A : Set} → ListI A → Bool
null ([]  {A})     = true
null (_∷_ {A} _ _) = false

对于 ListP，这是不可能的：

-- does not work
null′ : {A : Set} → ListP A → Bool
null′ ([]  {A})     = true
null′ (_∷_ {A} _ _) = false

错误信息为：

The constructor [] expects 0 arguments, but has been given 1
when checking that the pattern [] {A} has type ListP A

ListP也可以使用一个虚拟模块定义，如ListD:

module Dummy (A : Set) where
  data ListD : Set where
    []  : ListD
    _∷_ : A → ListD → ListD

open Dummy public

可能有些令人惊讶的是，ListD 等于 ListP。我们无法对传递给 Dummy 的参数进行模式匹配：

-- does not work
null″ : {A : Set} → ListD A → Bool
null″ ([]  {A})     = true
null″ (_∷_ {A} _ _) = false

这会产生与ListP相同的错误消息。 ListP是参数化数据类型的一个示例，比ListI更简单，后者是归纳族：它“依赖”于索引，尽管在这个示例中以一种微不足道的方式。

参数化数据类型在维基百科上有定义，而这里有一个简短的介绍。

归纳族没有真正被定义，但在维基百科上详细论述了它，并给出了似乎需要归纳族的规范示例。

data Term (Γ : Ctx) : Type → Set where
  var : Var Γ τ → Term Γ τ
  app : Term Γ (σ → τ) → Term Γ σ → Term Γ τ
  lam : Term (Γ , σ) τ → Term Γ (σ → τ)

忽略类型索引，如果使用Dummy模块的方式来简化这个问题，由于lam构造器的原因，无法实现。

另一个很好的参考资料是Peter Dybjer于1997年发表的归纳族。

愉快的Agda编码！