- 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. Cette notion s'applique naturellement dans l'étude des listes et des arbres.
Sommaire
Exemple
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 :aest 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)
Théorie
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
ZeroetSuccavecZerone prenant pas d'arguments (donc représenté par le type unité) etSuccprenant un autreSucc(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](d/1fd62d81f21fd44a7f85856b9f98cd30.png)
et ![unroll : \mu\alpha.T \to T[\mu\alpha.T/\alpha]](a/71a0676467e0b676787d24776ed2d24d.png)
, 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.
Voir aussi
Cet article est fondé sur une traduction de la Free On-line Dictionary of Computing et est utilisé avec permission selon la GFDL.
Wikimedia Foundation. 2010.
