Pour les types sommes comme pour les types produits, nous avons dit que les informations associés aux champs ou aux constructeurs peuvent être de n'importe quel type. Il est même possible d'utiliser le type en train d'être défini, afin de définir un type inductif. Ce n'est pas spécialement original, par exemple pour faire une liste simplement chainée en Java, on écrirait :
La classe LinkedList contient donc une référence à elle-même.
La même construction est possible en OCaml avec un type somme et un type produit mutuellement récursifs :
Contrairement à Java, la liste vide est explicitement définie comme étant une valeur propre au type des listes, plutôt que de réutiliser le pointeur nul. L'avantage est qu'OCaml nous force ensuite à prendre en considération le cas où une liste est Nil
La véritable définition des listes est cependant un peu plus simple : on utilise une paire plutôt qu'un type produit, ce qui réduit la verbosité :
Les arbres binaires sont un autre exemple classique :
Un arbre binaire est soit une feuille, soit un nœud avec deux sous-arbres.
Les constructions inductives sont une technique formelle pour construire des ensembles infinis de valeurs. On définit une ou plusieurs valeurs élémentaires, et une ou plusieurs opérations de construction par combinaison de valeurs de l'ensemble, et on définit alors l'ensemble des valeurs qui peuvent être ainsi construite.
On peut construire beaucoup de choses ainsi. Par exemple, les entiers naturels :
L'ensemble des entiers naturels est alors le plus petit ensemble qui vérifie ces deux propriétés. Nous avons que $0 :=$ Zero est un entier par la première règle, $1 :=$ Succ Zero est un entier par la deuxième règle, $2 :=$ Succ (Succ Zero) est un entier par la deuxième règle aussi en prenant $n = 1$, etc. Donc tout ensemble vérifiant ses deux règles contient les entiers naturels (ou en tout cas une représentation des entiers naturels).
Mais il y a d'autres ensembles vérifiant ces deux règles, par exemple les nombres relatifs, et même des ensembles très exotiques. Mais une définition inductive définit le plus petit ensemble, autrement dit seulement les valeurs que les règles nous obligent de créer. Il se trouve qu'il existe un seul ensemble minimal de valeurs vérifiant ces deux règles, et c'est cet ensemble que la définition inductive définit.
La définition des listes est presque identique (ce n'est pas une coïncidence) :
et pour les arbres :
La définition de ces types en OCaml est une réécriture dans la syntaxe du langage de ces définitions inductives. Les définitions inductives permettent de définir quasiment toutes les données que nous pourrions souhaiter manipuler. En informatique les définitions inductives sont fréquentes, par exemple, les grammaires hors-contextes (telles que les grammaires en Backus-Naur Form BNF qui permettent de décrire la syntaxe d'un langage de programmation) sont des définitions inductives d'ensembles de termes, et c'est l'une des applications des types inductifs.
Les types inductifs ont en OCaml deux principales applications.
Leur premier usage est pour la définition de structures de données. Nous avons par exemple déjà vu les listes et les arbres binaires, et nous savons depuis les cours d'algorithmique que les listes et les arbres sont les deux principales composantes de la plupart des structures de données. Nous pouvons facilement définir plusieurs types d'arbres :
Il est donc assez facile d'adapter la définition générique d'arbre pour obtenir diverses variantes selon les besoins. On peut aussi facilement ajouter des informations dans les nœuds, éventuellement en utilisant un type produit adapté, pour éviter de manipuler des tuples trop longs.
Le deuxième usage des types inductifs est de représenter des arbres syntaxiques. Nous avons mentionné que les grammaires hors-contextes sont des définitions inductives de l'ensemble des termes d'un langage. Il n'est donc pas étonnant que les arbres syntaxiques, qui représentent des dérivations de la grammaire, se représentent naturellement par des types inductifs. Considérons l'exemple des expressions arithmétiques, avec l'addition et la multiplication sur les entiers :
Une expression arithmétique est soit un entier, soit une somme de deux termes, soit un produit de deux facteurs. Le type arithpermet de représenter toutes les expressions arithmétiques pouvant être construite par sommes et produits de littéraux.
Un exemple plus complexe est l'arbre syntaxique des programmes OCaml. La librairie standard contient un module ParseTreequi expose la représentation qu'utilise le compilateur pour les programmes, et qui utilise des types sommes et produits mutuellement récursifs. Ce n'est qu'une version extrêmement développée de l'exemple des expression arithmétiques.
D'autres applications des types inductifs sont à mi-chemin entre structure de données et arbres syntaxiques. La librairie yojson utilise un type inductifs pour représenter des données au format json.
Si on ignore les crochets et les accents graves bizarres, que nous expliquerons bientôt, il s'agit d'un type inductif. De même on peut décrire les données au format XML par un type inductif. On peut aussi représenter des calculs à effectuer, par leur arbre syntaxique, qui pourront être évalués ultérieurement, ce qui permet de retarder le calcul. Beaucoup de librairies utilisent cette technique pour exposer une interface fonctionnelle et efficace. Par exemple Vg, la librairie de dessin vectoriel, ne dessine rien pendant la construction du dessin, mais enregistre en quelque sorte les opérations de construction à l'aide de types algébriques. C'est seulement lors du rendu, en svg ou en pdf, que la construction est interprétée et le dessin réalisé.
