Agda中的参数化归纳类型

Question

我只是在阅读工作中的依赖类型.在参数化类型的介绍中,作者在本声明中提到了这一点

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

Listis 的类型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一个归纳族更简单:它"取决于"指标,尽管在这个例子中是一个微不足道的方式.

参数化数据类型在wiki上定义, 这 是一个小介绍.

归纳家族并没有真正定义,但在wiki中详细阐述 了似乎需要归纳家庭的典型例子:

data Term (? : Ctx) : Type ? Set where
  var : Var ? ? ? Term ? ?
  app : Term ? (? ? ?) ? Term ? ? ? Term ? ?
  lam : Term (? , ?) ? ? Term ? (? ? ?)

忽略Type索引,Dummy由于lam构造函数,无法以-module方式编写此类型的简化版本.

另一个很好的参考是 Peter Dybjer从1997年开始的归纳家族.

快乐的阿格达编码!