Quais esquemas indutivos podem codificar a seguinte definição de Agda?

Question

Quais esquemas de indução (por ex.indução-recursão de Dybjer e Setzer, indução-recursão "irlandesa" de McBride ou indução-indução de Forsberg e Setzer ou talvez alguns mais simples) permitem codificar a seguinte definição de Agda

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

Posso pensar em alguns truques para reformular List nesta definição para que a indução-recursão se torne aplicável, mas há algum esquema que me permita primeiro dizer o que é uma lista e depois referir-me a esta informação para dizer o que é? A é assim que é feito em Agda?

Editar:Como decorre da resposta de András Kovács, este especial a definição pode ser reformulada como uma família indutiva.Aqui está como fazer isso:

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

Nenhum esquema que eu conheça codifica diretamente esse tipo.Às vezes é chamada de definição indutiva "aninhada".A complicação aqui é que Maybe e List são construtores de tipos externos à assinatura, e temos que formalizar a positividade estrita para operadores de tipos externos em geral, se quisermos permitir tais definições.

Em outras palavras, a consistência A depende da definição Maybe e List.Alguns operadores de tipo externo não são positivos, como em:

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

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

Agda analisa todas as definições externas e tenta determinar a variação dos parâmetros de tipo.Embora eu não conheça uma referência para uma especificação formal direta disso, uma maneira fácil de reformular definições aninhadas como não aninhadas é incluir os operadores de tipo externo em uma assinatura indutiva mútua.Por exemplo:

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

Este é um tipo indutivo mútuo comum, que é coberto (detalhes cosméticos do módulo) pelas famílias indutivas de Dybjer.