Quelle est la différence entre les ADT, les GADT et les types inductifs?

Quelqu'un pourrait-il expliquer la différence entre:

• Types de données algébriques (que je connais assez bien)
• Types de données algébriques généralisés (qu'est-ce qui les rend généralisés?)
• Types inductifs (par exemple Coq)

(Types particulièrement inductifs.) Merci.

Les types de données algébriques vous permettent de définir des types de manière récursive. Concrètement, supposons que nous ayons le type de données

Cela signifie que est le plus petit ensemble généré par les opérateurs N i l et C o n s . On peut formaliser cela en définissant l'opérateur F ( X $\mathsf{list}$$\mathsf{Nil}$$\mathsf{Cons}$$F(X)$

puis définir comme$\mathsf{list}$

Un ADT généralisé est ce que nous obtenons lorsque nous définissons un opérateur de type de manière récursive. Par exemple, nous pouvons définir le constructeur de type suivant:

Ce type signifie qu'un élément de est un tuple de a s de longueur 2 n pour certains n , puisque chaque fois que nous entrons dans le constructeur N e s t l'argument type est apparié avec lui-même. Nous pouvons donc définir l'opérateur que nous voulons prendre un point fixe comme:$\mathsf{bush\;}a$$a$$2^n$$n$$\mathsf{Nest}$

Un type inductif dans Coq est essentiellement un GADT, où les index de l'opérateur de type ne sont pas limités à d'autres types (comme dans, par exemple, Haskell), mais peuvent également être indexés par des valeurs de la théorie des types. Cela vous permet de donner des types pour les listes indexées en longueur, etc.

Considérez les types de données algébriques tels que:

data List a = Nil | Cons a (List a)

Les types de retour de chaque constructeur dans un type de données sont tous les mêmes: Nilet les Consdeux retournent List a. Si nous permettons aux constructeurs de renvoyer différents types, nous avons un GADT :

data Empty -- this is an empty data declaration; Empty has no constructors
data NonEmpty

data NullableList a t where
    Vacant :: NullableList a Empty
    Occupied :: a -> NullableList a b -> NullableList a NonEmpty

Occupieda le type a -> NullableList a b -> NullableList a NonEmpty, tout en Consa le type a -> List a -> List a. Il est important de noter qu'il NonEmptys'agit d'un type et non d'un terme. Un autre exemple:

data Zero
data Succ n

data SizedList a t where
    Alone :: SizedList a Zero
    WithFriends :: a -> SizedList a n -> SizedList a (Succ n)

Les types inductifs dans les langages de programmation qui ont des types dépendants permettent aux types de retour des constructeurs de dépendre des valeurs (et pas seulement des types) des arguments.

Inductive Parity := Even | Odd.

Definition flipParity (x:Parity) : Parity :=
  match x with
    | Even => Odd
    | Odd => Even
  end.

Fixpoint getParity (x:nat) : Parity :=
  match x with
    | 0 => Even
    | S n => flipParity (getParity n)
  end.

(*
A ParityNatList (Some P) is a list in which each member
is a natural number with parity P.
*)

Inductive ParityNatList : option Parity -> Type :=
  Nil : forall P, ParityNatList P
| Cons : forall (x:nat) (P:option Parity), 
  ParityNatList P -> ParityNatList 
  (match P, getParity x with
     | Some Even, Even => Some Even
     | Some Odd, Odd => Some Odd
     | _, _ => None
   end).

Remarque: GHC dispose d'un mécanisme pour traiter les constructeurs de valeur comme des constructeurs de type . Ce n'est pas la même chose que les types inductifs dépendants de Coq, mais cela diminue quelque peu la charge syntaxique des GADT et cela peut conduire à de meilleurs messages d'erreur.