Agda 中的参数化归纳类型

Question

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

data List (A : Set) : Set where
  []   : List A
  _::_ : A → List A → List 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 之间的实际区别是什么？

感谢您的宝贵时间！

Answer 1

我冒昧地重命名数据类型。第一个，也就是 在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，这是一个归纳家庭：它“取决于” 指标，虽然在这个例子中是微不足道的。

参数化数据类型在the wiki上定义， 和 here 是一个小小的介绍。

归纳族并未真正定义，但在the wiki 中进行了详细说明 用一些似乎需要归纳的典型例子 家庭：

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

不考虑类型索引，这不可能是简化版本 由于lam 构造函数，使用Dummy-module 方式编写。

另一个很好的参考是Inductive Families Peter Dybjer 从 1997 年开始。

祝 Agda 编码愉快！