Type récursif

En théorie des types, un type récursif a la forme ${\displaystyle \mu \alpha .T}$. Intuitivement, cette notation désigne le type ${\displaystyle U}$ représenté par l’expression ${\displaystyle T}$, dans lequel la variable de type ${\displaystyle \alpha }$ peut apparaître et désigne le type ${\displaystyle U}$ lui‐même[note 2].

Par exemple, si ${\displaystyle T=\mathrm {Int} \to \alpha }$, alors ${\displaystyle U=\mu \alpha .\mathrm {Int} \to \alpha }$ est le type d’une fonction qui prend un entier et renvoie une fonction de même type qu’elle‐même. On peut dérouler cette expression de type, en remplaçant dans ${\displaystyle T}$ la variable ${\displaystyle \alpha }$ par le type ${\displaystyle U}$ (ce qu’on note ${\displaystyle T[U/\alpha ]}$), ce qui donne ${\displaystyle \mathrm {Int} \to U}$. On peut itérer cette opération autant de fois que souhaité :

${\displaystyle U}$

${\displaystyle \mathrm {Int} \to U}$

${\displaystyle \mathrm {Int} \to (\mathrm {Int} \to U)}$

${\displaystyle \mathrm {Int} \to (\mathrm {Int} \to (\mathrm {Int} \to U))}$

${\displaystyle \vdots }$

L’exemple ci‐dessus des entiers naturels s’écrit ${\displaystyle \mathrm {Nat} =\mu \alpha .\mathbf {1} +\alpha }$, où les deux bras du type somme représentent les constructeurs Zero et Succ, avec Zero ne prenant pas d'argument (représenté par le type unité) et Succ prenant un élément du type Nat lui‐même (représenté par la variable de type ${\displaystyle \alpha }$).

L’exemple des listes d’éléments de type ${\displaystyle A}$, quant à lui, s’écrit ${\displaystyle \mathrm {List} A=\mu \alpha .\mathbf {1} +A\times \alpha }$. Le type unité représente le constructeur Nil sans argument, le type produit ${\displaystyle A\times \alpha }$ représente le constructeur Cons ayant pour arguments une valeur de type ${\displaystyle A}$ et une autre valeur de type ${\displaystyle \mathrm {List} A}$. En déroulant :

${\displaystyle \mathrm {List} A}$

${\displaystyle \mathbf {1} +A\times \mathrm {List} A}$

${\displaystyle \mathbf {1} +A\times (\mathbf {1} +A\times \mathrm {List} A)}$, soit ${\displaystyle \mathbf {1} +A+A^{2}\times \mathrm {List} A}$

${\displaystyle \mathbf {1} +A\times (\mathbf {1} +A+A^{2}\times \mathrm {List} A)}$, soit ${\displaystyle \mathbf {1} +A+A^{2}+A^{3}\times \mathrm {List} A}$

${\displaystyle \mathbf {1} +A\times (\mathbf {1} +A+A^{2}+A^{3}\times \mathrm {List} A)}$, soit ${\displaystyle \mathbf {1} +A+A^{2}+A^{3}+A^{4}\times \mathrm {List} A}$

${\displaystyle \vdots }$

On obtient successivement le type des listes de longueur zéro (${\displaystyle 1}$), un (${\displaystyle A}$), deux (${\displaystyle A^{2}}$), trois (${\displaystyle A^{3}}$), et ainsi de suite.

L’idée est que le type récursif ${\displaystyle U}$ vérifie l’équation informelle suivante :

${\displaystyle U=T[U/\alpha ]}$

Dans les exemples précédents, elle s’écrit respectivement :

• ${\displaystyle U=\mathrm {Int} \to U}$
• ${\displaystyle \mathrm {Nat} =\mathbf {1} +\mathrm {Nat} }$
• ${\displaystyle \mathrm {List} A=\mathbf {1} +A\times \mathrm {List} A}$

Si l’on s’autorisait les expressions de type infinies, on pourrait dérouler à l’infini et écrire, respectivement :

• ${\displaystyle U=\mathrm {Int} \to \mathrm {Int} \to \mathrm {Int} \to \ldots }$ (une fonction curryfiée acceptant autant d’arguments de type ${\displaystyle \mathrm {Int} }$ que souhaité)
• ${\displaystyle \mathrm {Nat} =\mathbf {1} +\mathbf {1} +\mathbf {1} +\ldots =\{0\,;1\,;2\,;\ldots \}}$ (c’est en effet une union disjointe de singletons que l’on peut nommer ${\displaystyle \{0\}}$, ${\displaystyle \{1\}}$, ${\displaystyle \{2\}}$, etc.)
• ${\displaystyle \mathrm {List} A=\mathbf {1} +A+A^{2}+A^{3}+\ldots =A^{*}}$ (l’étoile de Kleene)

Ces expressions infinies sont cependant mal définies, car elles ne reflètent qu’un seul type solution alors que l’équation de types peut en admettre plusieurs. On résout l’ambigüité en choisissant le plus petit ou le plus grand point fixe du déroulement, comme expliqué dans la section « Données & co‐données ».

Pour donner un sens à cette égalité de types, on distingue deux formes de récursivité qui diffèrent dans la manière d’introduire et d’éliminer les types récursifs : l’équirécursivité et l’isorécursivité.

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

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

roll :: (Bool->Fine) -> Fine
roll x = Fun x
unroll :: Fine -> (Bool->Fine)
unroll (Fun x) = x

data FunctionTakingItself b = R (FunctionTakingItself b -> b)
fix :: ((a -> b) -> a -> b) -> a -> b
fix f = let g y@(R x) a = f (x y) a in g (R g)

/* définition récursive du type encapsulée dans une structure */
struct function_t {
	struct function_t (*fun) (int) ;
};
typedef struct function_t function_t ;
/* définition mutuellement récursive de la fonction f et de son encapsulation g */
static function_t g ;
function_t f (int n)
{
	printf("%i", n) ;
	return g ;
}
static function_t g = { .fun = f } ;
int main (void)
{
	g.fun(1).fun(2).fun(3) ; /* écrit « 123 » */
	return 0 ;
}

Algébriquement, on peut définir le type ${\displaystyle \mu \alpha .T}$ comme un point fixe de la fonction ${\displaystyle \alpha \mapsto T}$ (qui à un type associe un type). La question est de choisir ce point fixe. On peut prendre soit le plus petit point fixe, soit le plus grand. On parle parfois de données dans le premier cas et de co‐données dans le second cas. Cette distinction est particulièrement importante en programmation totale (en), où l’on veut garantir la terminaison de tous les calculs[2]. En effet, dans le cas des types algébriques :

• les données sont bien fondées et présentent donc un principe de récurrence, qui permet de les détruire (définir des fonctions sur ces données) récursivement de façon terminante ;
• les co‐données présentent un principe de co-récurrence, qui permet de les construire (définir de telles valeurs) récursivement de façon productive.

Ces deux notions sont duales.

Dans un langage total, ce sont les deux seules formes autorisées de récursivité. Ces deux restrictions visent à garantir un bon comportement des programmes.

• Que les données soient nécessairement finies assure la terminaison des fonctions qui les traitent, grâce au principe de récurrence.
• L’introduction des co‐données potentiellement infinies permet de retrouver une forme de non‐terminaison nécessaire pour réaliser des programmes à boucle d’ïnteraction, tels qu’un système d’exploitation, qui réagissent à un flux d’événements extérieurs. Ici, le bon comportement est garanti par la productivité des définitions co‐récursives : chaque étape de calcul produit une portion (un co‐constructeur) de co‐donnée, qui est donc exploitable par la suite.

Afin de ne pas risquer qu’une fonction définie par récurrence sur une donnée soit appelée sur une co‐donnée infinie, on considérera distincts les types de données et les types de co‐données, avec deux mots‐clés différents pour les définir.

Dans l’exemple précédent des listes, la fonction de types était ${\displaystyle \alpha \mapsto \mathbf {1} +A\times \alpha }$.

• Son plus petit point fixe est ${\displaystyle A^{*}=\mathbf {1} +A+A^{2}+A^{3}+\ldots }$, c’est‐à‐dire le type des listes finies.
• Son plus grand point fixe est ${\displaystyle A^{*}+A^{\infty }}$, c’est‐à‐dire l’ensemble des listes potentiellement infinies.

Si l’on n’avait pas le constructeur Nil (permettant de fonder une liste), alors la fonction serait ${\displaystyle \alpha \mapsto A\times \alpha }$ et alors :

• le plus petit point fixe est le type vide ${\displaystyle \emptyset }$, ne contenant aucune valeur (sans Nil, il est impossible de construire une liste finie) ;
• le plus grand point fixe est ${\displaystyle A^{\infty }}$, le type des listes infinies.

De même, dans l’exemple des entiers naturels, on considère ${\displaystyle \alpha \mapsto \mathbf {1} +\alpha }$ :

• le plus petit point fixe est ${\displaystyle \mathbf {N} =\{0\}\cup \{1\}\cup \{2\}\cup \ldots =\mathbf {1} +\mathbf {1} +\mathbf {1} +\ldots }$, le type des entiers naturels ;
• le plus grand point fixe est ${\displaystyle \mathbf {N} \cup \{\infty \}}$.

Et une remarque analogue s’applique pour le constructeur Zero.

Les langages Turing‐complets usuels ignorent cette nuance et permettent une récursivité non contrôlée. Il n’y a donc qu’un seul mot‐clé pour définir un type récursif, qui est implicitement le plus grand point fixe. Ainsi en Haskell :

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

on peut utiliser ces listes comme des données, avec une fonction définie par récurrence (cette définition est bien fondée : chaque appel récursif se fait sur des données structurellement plus petites) :

length :: List a -> Int
length Nil           = 0
length (Cons _ tail) = 1 + length tail

ou comme des co‐données, avec une définition par co‐récurrence (cette définition est productive : chaque itération produit un constructeur) :

infinite_list :: List Int
infinite_list = Cons 1 infinite_list -- la liste [ 1, 1, 1, … ]

naturals :: List Int
naturals = naturals_from 0 where -- la liste [ 0, 1, 2, … ]
  naturals_from n = Cons n (naturals_from (n+1))

L’évaluation paresseuse permet d’écrire cette définition sans entrer dans une boucle infinie d’évaluation. On voit ainsi que la paresse est essentielle pour construire des co‐données dans un langage total.

Mais on peut également écrire des définitions récursives qui ne sont ni récurrentes ni co‐récurrentes, qu’elles soient pertinentes ou pas. Ainsi l’exemple précédent peut se réécrire de façon parfaitement valide suivant un idiome courant en Haskell (cette définition n’est pas co‐récurrente au sens le plus courant, à cause de l’appel à map) :

naturals :: List Int
naturals = Cons 0 (map succ naturals) -- la liste [ 0, 1, 2, … ]

Mais rien ne nous empêche d’écrire des programmes bogués :

stupid list = stupid (Cons 1 list)
idiot = length naturals

• Induction structurelle
• Récursivité
• type algébrique de données

(en) Cet article contient des extraits de la Free On-line Dictionary of Computing qui autorise l'utilisation de son contenu sous licence GFDL.