Résumé
En programmation informatique et théorie des types, un type récursif est un type de données dont la définition fait appel au type lui‐même, de façon récursive. Cela permet entre autres des structures de données qui contiennent des sous‐structures du même type. Cette notion s'applique naturellement dans l'étude des listes et des arbres. Type algébrique de données Les types algébriques sont de loin la forme la plus courante de types récursifs. Un exemple classique est le type liste. En syntaxe Haskell (avec une variable de type a qui rend cette définition polymorphe) : data List a = Nil | Cons a (List a) Autrement dit, une liste d’éléments de type a est soit une liste vide, soit une cellule contenant une donnée de type a (la « tête » de liste) et une autre liste (la « queue » de liste). Autre exemple, le type des entiers naturels (voir l’arithmétique de Péano) peut être défini par : data Nat = Zero | Succ Nat c’est‐à‐dire qu’un entier naturel est soit zéro, soit le successeur d’un entier naturel. On peut avoir besoin d’une fonction qui se prend elle‐même en argument. Par exemple, si l’on souhaite écrire le combinateur de point fixe Y, qui permet de définir des fonctions récursives : ne compile pas ! fix :: ((a -> b) -> a -> b) -> a -> b fix f = let g x a = f (x x) a in g g alors, bien que fix n’ait pas lui‐même un type récursif, sa définition en fait intervenir un. En effet, la variable x est appliquée à elle‐même donc, si l’on note son type, alors x est aussi une fonction prenant un argument de type . On obtient alors un type récursif défini par l’équation pour un certain type . De façon symétrique, il est parfois utile d’écrire une fonction qui se renvoie elle‐même, ou une autre fonction du même type (par exemple pour coder un automate ou un gestionnaire d’événements). Un exemple simplifié en langage C : /* syntaxe C pour l’équation de types « function_t = (int → function_t) » ; ne compile pas ! */ typedef function_t (function_t) (int) ; function_t f (int n) { printf("%i", n) ; return f ; } int main (void) { f(1)(2)(3) ; / devrait écrire « 123 » */ return 0 ; } Si l’on note le type de la fonction f, alors f est une fonction qui prend un entier (type ) et se renvoie elle‐même (type ) ; son type est donc aussi , d’où l’équation .
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.
Publications associées (2)