gadt - 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 ，这是一个归纳族:它“取决于”
指数，虽然在这个例子中是微不足道的。

参数化数据类型在 thewiki 上定义,
和
here
是一个小介绍。

归纳族并未真正定义，但在 thewiki 中有详细说明
用一些似乎需要归纳的典型例子
家庭:

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

无视类型索引，这不可能是简化版本
写在 Dummy -模块方式因为 lam构造函数。

另一个很好的引用是 InductiveFamilies
1997 年由彼得·戴比耶 (Peter Dybjer) 撰写。

快乐的 Agda 编码!