Comprendre les catamorphismes
Bananes, lentilles, enveloppes et barbelés
Functional Programming with bananas, lenses, envelopes and barbed wires est un article célèbre qui explore différentes formes (ou patterns) de récursion. C’est à dire que l’on cherche à exprimer la récursion non pas comme une caractéristique du langage mais comme une fonction d’ordre supérieur, ou un combinateur comme un autre, comme tel donc susceptible d’être généralisé, réutilisé, composé. Depuis ma découverte de cet article j’ai été fasciné par ses possibilités sans avoir jamais pris le temps de les comprendre vraiment. Cet article est une tentative d’explication de ce qu’est un catamorphisme, l’une des formes de récursions classifiées dans l’article sus-cité.
Types de données récursifs
Quand on définit une structure (un type de données), il est fréquent de définir des types qui soient récursifs, c’est à dire qui utilisent des données de leur propre type. L’exemple le plus typique en est l’ensemble des entiers naturels, définissable en Java comme suit:
public class Natural {
public static final Natural Zero = new Natural();
public static final Natural succ(Natural natural) {
return new Natural(natural);
}
private Natural() {}
private Natural(Natural pred) {
this.pred = pred;
}
}
Un entier est ici construit à l’aide de la méthode succ
et de la constante Zero
:
- soit 0 ;
- soit le successeur d’un autre entier.
La question que l’on peut se poser, si l’on s’intéresse à ce genre de choses, c’est : comment peut-on caractériser algébriquement l’ensemble des entiers ainsi défini, si ce n’est de manière tautologique ? Il peut nous apparaître très naturel d’utiliser un type dans sa propre définition mais c’est parce que nous sommes habitués à raisonner récursivement.
Point Fixe
Pour répondre à la question posée, on peut reformuler de manière “compacte” le problème en cherchant à définir le type Natural
comme la solution d’une équation algébrique (+ joue ici le rôle de OU
):
Natural = Zero + Succ (Natural),
équation dont la solution est problématique puisque la variable apparaît des deux côtés de l’équation !
Si l’on substitue naïvement la définition de Natural
en partie droite, alors on obtient quelque chose comme
Natural = Zero + Succ (Zero + Succ ( Zero + Succ (Zero +...
ce qui peut se réécrire en
Natural = Zero + Succ (Zero) + Succ (Succ (Zero)) +...
Natural
apparait bien comme un ensemble infini d’éléments qui sont soit Zero
soit de la forme \(Succ^n Zero\) pour tout \(n\)
entier.
Du point de vue mathématique, la solution d’une équtation de la forme \(x = f(x)\) est appelée un point fixe, ce qui est bien la
forme de l’équation de Natural. On peut donc dire que Natural
est le point fixe de l’équation \(X = Zero + Succ (X)\). Nous disons
le point fixe, mais ce n’est pas tout à fait exact : comme on ne considére que des nombres finis (même si l’ensemble lui-même
est de taille infinie), il s’agit là du plus petit point fixe. Il existe en effet des ensembles qui sont des points fixes de
cette équation mais dont la cardinalité est plus grande que N car ils contiennent des nombres infinis (en quantité infinie…).
Ce type de définition étant très courant, il a paru utile de généraliser cette notion de plus petit point fixe, d’où l’introduction l’opérateur μ. Pour toute fonction f, μf est le plus petit point fixe de f, plus formellement: \[ μf = x \in dom(f), x = f(x) \] et \[ \forall x' \in dom(f), x'= f(x') \Rightarrow x' \geq x \]
Or ici la définition de Natural ne semble pas être une fonction. En fait, pour qu’une définition de type soit une fonction, il
faut qu’elle soit une fonction sur des types, prenant en argument des types et retournant des types, en d’autres termes un
foncteur. Mais c’est exactement ce que dit la forme \(Zero + Succ (X)\) où X désigne un type quelconque, et donc on peut
légitimement définir Natural = μ(Zero + Succ(x))
comme un ensemble d’éléments point fixe d’un foncteur.
Définition explicite
Toute cette mécanique est rendu implicite dans tous les langages, même les plus sophistiqués comme Haskell, Scala ou Caml. Pour définir un type de données récursif, nul besoin d’utiliser l’opérateur μ, on se contente d’utiliser les possibilités syntaxiques du langage qui autorise l’usage du nom d’un type dans sa définition. Mais pour pouvoir généraliser les mécanismes de récursions sous forme de FOS, il est nécessaire de déconstruire cette vision et d’introduire explicitement la récursion.
C’est ce que l’on va faire, en Haskell tout d’abord.
On introduit d’abord l’opérateur Mu
comme un nouveau type de données prenant en paramètre un foncteur f
. Mu
a un seul
constructeur, In
qui empaquette le foncteur f
dans une boucle récursive, ce qui nous donne 2 fonctions permettant de naviguer dans la “pile” de récursion:
In : f (Mu f) -> Mu f
(le constructeur, vu comme une fonction),out : Mu f -> f (Mu f)
(l’accesseur de l’unique champ de la structure encapsulée par In).
-- newtypes in Haskell are cheaps, they do not add any runtime overhead and serve
-- only for the compiler to distinguish types
newtype Mu f = In { out :: (f (Mu f)) }
Essayons maintenant de définir les entiers comme ci-dessus au moyen de Mu
en évitant la récursion explicite et en définissant Natural
comme un foncteur:
-- le foncteur engendrant les entiers naturels
data Natf x = Zero | Succ x
-- le type (un simple alias) Natural comme point fixe d'un foncteur
type Natural = Mu Natf
Voici quelques objets de type Natural
que l’on peut construire en utilisant directement les constructeurs de Natf
sans se préoccuper de Mu
pour l’instant:
*Main> let zero = Zero
*Main> let un = Succ Zero
*Main> :t un
un :: Natf (Natf x)
*Main> let deux = Succ un
*Main> :t deux
deux :: Natf (Natf (Natf x))
On peut constater que chaque “nombre” a un type différent, ce qui n’est pas très pratique. En utilisan Mu
, on uniformise le type d’où nait Natural
, un ensemble contenant des objets de type homogène:
*Main> let zero = In Zero
*Main> :t zero
zero :: Mu Natf
*Main> let un = In (Succ zero)
*Main> :t un
un :: Mu Natf
*Main> let deux = In (Succ un)
*Main> :t deux
deux :: Mu Natf
Tous les nombres ont bien ici le type Mu Natf
et l’on peut sans problème les combiner, par exemple pour définir l’addition:
add :: Natural -> Natural -> Natural
In Zero) x = x
add (In Zero) = x
add x (In (Succ x)) (In (Succ x')) = In (Succ (In (Succ (add x x')))) add (
Foncteur et F-Algèbre
Evidemment, c’est théoriquement très intéressant mais ce qu’on veut c’est manipuler des “vrais” nombres, pas de longues chaînes de constructeurs, sauf dans les cas où l’on s’intéresse à la récursion explicite, évidemment. On voudrait donc pouvoir transformer des objets de notre type Natural
en un type plus commun, par exemple Int
. Pour ce faire, notre type de base Natf
manque d’un ingrédient: la fonctorialité (ou propriété d’être un foncteur). On a vu que ce qui définissait un foncteur, c’était le fait de posséder une fonction fmap
possédant quelques bonnes propriétés de compositionnalité. Dans le cas de Natf
, cette définition est simple:
instance Functor Natf where
fmap f (Zero) = Zero
fmap f (Succ x) = Succ (f x)
Dès que l’on a un foncteur f
, alors pour tout type a
on peut définir (entre autres myriades de choses) des fonctions de types h :: f a -> a
qui “déconstruisent” des éléments de a
“transformés” par f
en éléments de a
: c’est comme si on enlevait une couche d’une pelure d’oignon. Ce type de fonction est suffisamment courant pour avoir été nommé, on les appelle des f-algèbres. Par exemple, on peut écrire une f-algèbre qui permet de transformer des objets de type Natf Int
en objets de type Int
(nos gentils entiers habituels):
intalgebra :: Natf Int -> Int
Zero = 0
intalgebra Succ x) = 1 + x intalgebra (
Cette fonction est très simple et non récursive, elle décrit simplement une correspondance univoque entre des opérations du type de départ (les constructeurs de Natf
) et des opérations du type d’arrivée (les fonctions plus
et la constante 0
). Ce serait encore plus explicite si l’on pouvait écrire ceci:
-- does not compile
intalgebra :: Natf Int -> Int
Zero = 0
intalgebra Succ = (1+) intalgebra
Mais une fois que l’on a cette fonction, on n’est guère avancé car de toute évidence, elle ne peut s’appliquer aux nombres de type Natural
. C’est ici qu’entre un jeu notre premier “récurseur” d’ordre supérieur: le catamorphisme (roulement de tambour) !
Catamorphismes
Un catamorphisme est donc une fonction d’ordre supérieure permettant de produire une valeur d’un type arbitraire en “repliant” une structure, un type algébrique, récursivement, par application d’un opérateur quelconque sur une valeur initiale.
Le catamorphisme “canonique” est l’opérateur foldr
sur les listes:
foldr :: (a -> b -> b) -> b -> [a] -> b
foldr op x [] = x
foldr op x (y:ys) = y `op` (foldr op x ys)
Pour tout opérateur binaire ⊙ et toute valeur x, \(h = \textrm{foldr} ⊙ x\), est un catamorphisme pour les listes de type [a] -> b
. Le parcours de la liste est imbriqué avec l’application de l’opérateur dans l’appel récursif à foldr
. Par ailleurs, on a vu ci-dessus que la récursion pouvait être rendue explicite au travers de la structure du type de données, par l’opérateur Mu
, qui produit un point fixe d’un foncteur quelconque. On aimerait donc pouvoir distinguer, séparer, dans foldr et d’autres opérations du même type qui transforment un type de données récursif en une valeur quleconque, deux entités distinctes:
- le traitement de chaque instance possible d’un foncteur, autrement dit une f-algèbre quelconque ;
- et la récursion.
Ces deux contraintes peuvent s’exprimer dans le système de type, ce qui nous donne la signature suivante pour cata
:
cata :: Functor f => (f a -> a) -> (Mu f -> a)
cata
est donc une fonction qui, à partir d’une f-algèbre, produit une fonction transformation un point fixe du foncteur f
ene une valeur. Sa définition est la suivante et l’on voit bien que la récursion y est explicite:
= h . fmap (cata h) . out cata h
On est désormais équipé pour appliquer notre fonction intalgebra
définie ci-dessus pour transformer les nombres algébriques en entiers “sympathiques”:
toInt :: Natural -> Int
toInt = cata intalgebra
et l’on peut utiliser toint
pour obtenir de “vrais” entiers:
*Main> toint (In Zero)
0
*Main> toint (In (Succ (In (Succ (In Zero)))))
2
*Main>