Type recursif

Type recursif

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)

Sommaire

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 : 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.

Voir aussi

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

  • Portail de la programmation informatique Portail de la programmation informatique
Ce document provient de « Type r%C3%A9cursif ».

Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Type recursif de Wikipédia en français (auteurs)

Игры ⚽ Поможем сделать НИР

Regardez d'autres dictionnaires:

  • 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 1… …   Wikipédia en Français

  • Type algebrique de donnees — Type algébrique de données Un type algébrique de données est un type de données dont chacune des valeurs est une donnée d un autre type enveloppée dans un des constructeurs du type. Toutes les données enveloppées sont des arguments du… …   Wikipédia en Français

  • Type algébrique — de données Un type algébrique de données est un type de données dont chacune des valeurs est une donnée d un autre type enveloppée dans un des constructeurs du type. Toutes les données enveloppées sont des arguments du constructeur. Par contraste …   Wikipédia en Français

  • Type statique — Typage statique Sommaire 1 Définition 2 Langages à objets et typage statique 3 Problèmes 4 Résolution, autres difficultés …   Wikipédia en Français

  • Type abstrait — En génie logiciel, un type abstrait est une spécification mathématique d un ensemble de données et de l ensemble des opérations qu elles peuvent effectuer. On qualifie d abstrait ce type de données car il correspond à un cahier des charges qu une …   Wikipédia en Français

  • Type algébrique de données — Un type algébrique de données est un type de données dont chacune des valeurs est une donnée d un autre type enveloppée dans un des constructeurs du type. Toutes les données enveloppées sont des arguments du constructeur. Par contraste aux autres …   Wikipédia en Français

  • Type énuméré — Pour les articles homonymes, voir Enum. En programmation informatique, un type énuméré est un type de données qui consiste en un ensemble de constantes appelées énumerateurs. Lorsque l on crée un type énuméré on définit ainsi une énumeration.… …   Wikipédia en Français

  • Signature de type — Pour les articles homonymes, voir Signature (homonymie). En programmation informatique, la signature de type définit les types de données acceptables pour une fonction ou une méthode. Une signature inclut au moins le nom de la fonction et le… …   Wikipédia en Français

  • Algorithme Récursif — Les algorithmes récursifs et les fonctions récursives sont fondamentaux en informatique. Un algorithme est dit récursif s il s appelle lui même. Les premiers langages de programmation qui ont introduit la récursivité sont LISP et Algol 60 et… …   Wikipédia en Français

  • Algorithme recursif — Algorithme récursif Les algorithmes récursifs et les fonctions récursives sont fondamentaux en informatique. Un algorithme est dit récursif s il s appelle lui même. Les premiers langages de programmation qui ont introduit la récursivité sont LISP …   Wikipédia en Français

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”