Type recursif

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)

Sommaire 1 Théorie 1.1 Types isorécursifs 1.2 Types équirécursifs 2 Voir aussi

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 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 : et , 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

• Récursion
• type algébrique de données

Cet article est basé sur une traduction de la Free On-line Dictionary of Computing et est utilisé avec permission selon la GFDL.

Éléments de programmation informatique
Bibliothèque logicielle	Bibliothèque standard • Espace de nom • Framework • Gabarit (template) • Interface • Interface de programmation (API)
Vocabulaire	Algorithme • Expression • Indentation • Ligne de code • Opérateur • Pseudo-code • Surcharge des opérateurs Autour des fonctions Convention de nommage • Factorisation • Fonction imbriquée • Fonction de rappel • Fonction récursive • Généricité • Opérande • Paramètre • Polymorphisme • Procédure • Signature de type Autour de l'objet Classe • Constructeur • Destructeur • Encapsulation • Héritage • Héritage multiple • Instance • Méthode • Ramasse-miettes (garbage collector) • Référence
Dans le code source	Structures de données Arbre • Attribut • Caractère • Enregistrement • File • First in, first out (fifo) • Last in, first out (lifo) • Liste • Liste chaînée • Pile • Table de symboles • Tableau • Tas • Type abstrait • Sémaphore Déclarations : types et variables Affectation • Pointeur • Portée • Tableau associatif • Type énuméré • Type récursif • Typage statique • Variable • Variable globale • Variable locale Structures de contrôle case • do • else • eval • if • for • goto • loop • switch • while Fonctions usuelles Concaténation • Incrémentation • malloc • printf
Outil de développement logiciel	Environnement de développement • Environnement de développement intégré (IDE) • Générateur de documentation • Gestion de versions • Modèle • Patch • Spécification
Folklore	Hello world • Keep it Simple, Stupid • Langage de programmation exotique
Catégorie:Développement logiciel • Catégorie:Programmation informatique

• Portail de la programmation informatique