Type récursif

Dans un langage de programmation, un type récursif ou type inductif est un type de données pour des valeurs qui contiennent d'autres valeurs du même type.

Un exemple est le type liste en Haskell :

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

Cela spécifie que la liste de a est soit une liste vide ou un cellule cons contenant un a (la "tête" de liste) et une autre liste (la "queue" de liste). Note : a est une variable de type, ce qui fait cette expression utilise du polymorphisme paramétrique.

La récursion n'est pas permise en Miranda ou les types synonymes en Haskell, donc les types Haskell suivants sont illégaux :

type Bad = (Int, Bad) type Evil = Bool -> Evil

Mais, les types de données algébriques apparemment équivalent sont pourtant acceptables :

data Good = Pair Int Good data Fine = Fun (Bool->Fine)

En théorie des types, un type récursif a la forme μα.T où la variable de type peut apparaître dans le type T et représente le type entier lui-même.

Par exemple, un nombre naturel (voir arithmétique de Péano) peut être défini par le type de donnée Haskell :

data Nat = Zero | Succ Nat

Et en théorie des types, nous dirions nat = μα.1 + α. Où les deux bras du type somme représentent les constructeurs Zero et Succ avec Zero ne prenant pas d'arguments (donc représenté par le type unité) et Succ prenant un autre Succ (donc un autre élément de μα.1 + α).

Il y a deux formes de types récursifs, les types isorécursifs et les types équirécursifs. Les deux formes diffèrent dans la manière avec laquelle les types récursifs sont introduits et éliminés.

Types isorécursifs

Avec des types isorécursifs μα.T et son expansion T[μα.T / α] sont des types distincts et disjoints avec des constructions spéciales de termes géméralement appelés roll et unroll, avec un isomorphisme entre elles. Pour être précis : $roll:T[\mu \alpha .T/\alpha ]\to \mu \alpha .T$ et $unroll:\mu \alpha .T\to T[\mu \alpha .T/\alpha ]$, et ce sont des fonctions inverses.

Types équirécursifs

Avec la règle de types équirécursifs, un type récursif μα.T et son déroulement T[μα.T / α] sont égaux -- c'est-à-dire que ces deux expressions de type dénotent le même type.

En fait, la plupart des théories de types équirécursifs va plus loin et stipule que deux expressions avec la même "expansion indéfinie" sont équivalentes. La conséquence de ces règles est que les types équirécursifs ajoutent beaucoup plus de complexité au système de type que les types isorécursifs. Les problèmes algorithmiques tels que la vérification des types ou l'inférence de types sont aussi plus difficiles avec les types équirécursifs.

Les types équirécursifs capturent la forme d'auto-référentialité (ou de référentialités mutuelles) de définitions de types dans les langages procéduraux et orientés objet. Ils surviennent aussi dans la sémantique "type-theoritic" des objets et des classes.

Dans les langages de programmation, les types isorécursifs (sous la forme de types de données) sont beaucoup plus courants.