Quels schémas inductifs peuvent coder la définition Agda suivante ?

Question

Quels programmes d'intégration (par ex.induction-récursion par Dybjer et Setzer, induction-récursion "irlandaise" par McBride ou induction-induction par Forsberg et Setzer ou peut-être quelques plus simples) permettent de coder la définition Agda suivante

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

Je peux penser à quelques astuces pour reformuler List dans cette définition afin que la récursion par induction devienne applicable, mais existe-t-il des schémas qui me permettraient d'abord de dire ce qu'est une liste, puis de me référer à ces informations pour dire ce qu'est une liste ? A c'est comme ça que ça se passe à Agda ?

Modifier:Comme il ressort de la réponse d'András Kovács, ceci particulier la définition peut être reformulée comme une famille inductive.Voici comment faire:

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

Aucun schéma à ma connaissance ne code directement ce type.Parfois, on parle de définition inductive « imbriquée ».La complication ici est que Maybe et List sont des constructeurs de types externes à la signature, et nous devons formaliser une stricte positivité pour les opérateurs de types externes en général, si nous voulons autoriser de telles définitions.

Autrement dit, la cohérence de A dépend de la définition de Maybe et List.Certains opérateurs de type externe ne sont pas positifs, comme dans :

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

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

Agda examine toutes les définitions externes et essaie de déterminer la variance des paramètres de type.Bien que je ne connaisse pas de référence pour une spécification formelle directe de cela, un moyen simple de reformuler les définitions imbriquées comme non imbriquées consiste à inclure les opérateurs de type externes dans une signature inductive mutuelle.Par exemple:

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

Il s'agit d'un type inductif mutuel ordinaire, qui est couvert (détails cosmétiques modulo) par les familles inductives de Dybjer.