哪些归纳方案可以编码以下Agda定义？

Question

哪些诱导方案（例如dybjer和Setzer的归纳-递归，McBride的"爱尔兰"归纳-递归或Forsberg和Setzer的归纳-归纳，或者可能是一些更简单的）允许人们对以下Agda定义进行编码

  data A : Set where
    a : Maybe (List A) → A

我能想到一些技巧来重新制定 List 在这个定义中，以便归纳递归变得适用，但是是否有任何方案可以让我首先说列表是什么，然后参考这些信息来说什么 A 在阿格达是这样做的吗？

编辑:从András Kovács的回答如下，这 特别是 定义可以重新定义为归纳家庭。以下是如何做到这一点:

data Three : Set where one two three : Three

data AG : Three → Set where
  a'       : AG three → AG one
  nil'     : AG two
  cons'    : AG one → AG two → AG two
  nothing' : AG three
  just'    : AG two → AG three

A = AG one
ListA = AG two
MaybeListA = AG three

a : MaybeListA → A
a = a'

nil : ListA
nil = nil'

cons : A → ListA → ListA
cons = cons'

nothing : MaybeListA
nothing = nothing'

just : ListA → MaybeListA
just = just'

Answer 1

我所知道的任何方案都没有直接编码该类型。有时它被称为"嵌套"归纳定义。这里的复杂之处在于 Maybe 和 List 是签名外部的类型构造函数，如果我们想允许这样的定义，我们必须为外部类型运算符形式化严格的积极性。

换句话说， A 取决于定义 Maybe 和 List.一些外部类型运算符不是正的，如:

data Neg (A : Set) : Set where
  neg : (A -> Bool) -> Neg A

data B : Set where
  b : Neg B -> B

Agda确实会查看所有外部定义，并尝试确定类型参数的方差。虽然我不知道对此的直接正式规范的引用，但将嵌套定义重新定义为非嵌套的简单方法是将外部类型运算符包含到相互归纳的签名中。例如:

data A : Set 
data ListA : Set
data MaybeListA : Set

data A where
  a : MaybeListA -> A

data ListA where
  nil : ListA
  cons : A -> ListA -> ListA

data MaybeListA where
  nothing : MaybeListA
  just : ListA -> MaybeListA

这是一个普通的互感类型，由Dybjer的归纳家族复盖（modulo化妆品细节）。