L'approche qualité avec OCaml

Implémenter un ordre total sur un type revient à implémenter une fonction similaire à la fonction Pervasives.compare.
Parfois on a une implémentation d'un ordre total sur un type et on veut l'étendre à une structure de donnée.
Par exemple on peut vouloir étendre cet ordre vers un ordre sur les listes ou sur les n-uplets.
Il existe une façon générale de réaliser cette extension, cette façon se nomme ordre lexicographique et fonctionne de façon similaire à l'ordre alphabétique.

Prenons exemple sur les caractères.
On peut bien sûr comparer deux caractères de type char :

# 'a' < 'o';;
- : bool = true

Et on peut aussi comparer deux chaînes de caractères de type string :

# "baba" < "bobo";;
- : bool = true

Cette façon d'étendre la comparaison du type char vers le type string c'est l'ordre alphabétique. On compare d'abord le 1er caractère, en cas d'égalité on compare le 2d, puis éventuellement le 3e, et ainsi de suite jusqu'à éventuellement atteindre la fin de la chaîne. C'est justement cette méthode qu'utilise la fonction Pervasives.compare. Illustration avec les listes :

# ['b';'a';'b';'a'] < ['b';'o';'b';'o'];;
- : bool = true

Puis avec les n-uplets :

# ('b','a','b','a') < ('b','o','b','o');;
- : bool = true

Remarque : dans le cas où l'on implémente une fonction compare spécifique (nous l'avons déjà fait par exemple pour les inventaires) la fonction qui suit nous renvoie l'extension lexicographique de cet ordre sur les listes.

# let lexicographical (cmp:'a -> 'a -> int) =
  let rec loop l1 l2 =
    match l1,l2 with
    | [],[] -> 0
    | [],_ -> -1
    | _,[] ->  1
    | h1::t1,h2::t2 ->
        let c = cmp h1 h2 in
        if c = 0 then loop t1 t2
        else c
  in loop;;
val lexicographical : ('a -> 'a -> int) -> 'a list -> 'a list -> int = <fun>

On appelle type produit un type qui réalise le produit cartésien de deux ou plusieurs types.

En OCaml il s'agit essentiellement :

• des n-uplets dont on a parlé dans le chapitre 18. Les couples, le constructeur pour ces types est le caractère étoile, le constructeur pour ces valeurs est le caractère virgule ;
• des enregistrements dont on a parlé dans le chapitre 23. Les enregistrements, les constructeurs pour ces types sont les noms d'un type enregistrement, le constructeur pour ces valeurs est la paire d'accolades.

On appelle type somme un type qui réalise l'union disjointe de plusieurs types.
Il s'agit des types énumérés dont on a parlé au chapitre 13. Les types énumérés, le constructeur pour ces types est le caractère barre verticale, le constructeur pour ces valeurs est un variant.

À voix haute la barre verticale se lit "ou bien".

Les variants ne sont pas limités aux types énumérés et nous allons progressivement exposer toute leur généralité.
Nous allons commencer par un simple problème de jeu de cartes qui suffira amplement à se convaincre de leur étonnante expressivité. Le problème que nous avons choisi est celui de la main gagnante au poker, après l'abattage (showdown) : laquelle parmi deux mains l'emporte sur l'autre ?

Le néophyte pourra rapidement s'initier au poker, il retiendra en particulier qu'une main au poker est constituée de cinq cartes et que le jeu consiste à produire la meilleure combinaison possible :

• avoir en main une carte haute (HighCard) c'est passable ;
• avoir en main une paire (OnePair) c'est un peu mieux ;
• avoir en main deux paires (TwoPair) c'est déjà pas mal ;
• avoir en main un brelan (ThreeOfAKind) c'est meilleur ;
• avoir en main une quinte (Straight) c'est déjà confortable ;
• avoir en main une couleur (Flush) c'est encore plus confortable ;
• avoir en main une main pleine (FullHouse) c'est bien plus avantageux ;
• avoir en main un carré (FourOfAKind) c'est encore plus avantageux ;
• avoir en main une quinte-flush (StraightFlush) c'est l'idéal.

On résume ainsi la relation d'ordre total pour une combinaison :

• HighCard < OnePair < TwoPair < ThreeOfAKind < Straight < Flush < FullHouse < FourOfAKind < StraightFlush

Ainsi bien sûr que la relation d'ordre total pour une carte seule :

• 2 < 3 < 4 < 5 < 6 < 7 < 8 < 9 < 10 < jack < queen < king < ace.

Pour implémenter l'ordre total sur une seule carte, il suffit de désigner les cartes numériques par leur valeur entière et les figures par cette définition multiple (à l'aide de l'appariement de motif sur un quadruplet) :

# let ace,king,queen,jack = 50,40,30,20;;
val ace : int = 50
val king : int = 40
val queen : int = 30
val jack : int = 20

La tentation est grande d'appliquer la même technique (appariement de motif sur un n-uplet) pour implémenter l'ordre total sur une combinaison :

let
  highcard,onepair,twopair,threeofakind,straight,
  flush,fullhouse,fourofakind,straightflush
  =
  1,2,3,4,5,6,7,8,9
  ;;

Et cela nous permet bien la comparaison de deux combinaisons. Cependant l'exemple des jours de la semaine dans le déjà lointain chapitre 14. Le filtrage et la discussion qui en découlait nous incitent à penser qu'un type énuméré ferait mieux l'affaire. Nous préfèrerons donc déclarer le type poker_hand :

type poker_hand =
  | HighCard
  | OnePair
  | TwoPair
  | ThreeOfAKind
  | Straight
  | Flush
  | FullHouse
  | FourOfAKind
  | StraightFlush
  ;;

D'un côté, en éliminant les valeurs numériques arbitraires, nous gagnons en clarté, de plus le type poker_hand est désormais candidat au filtrage, une facilité si essentielle que l'habitude et le confort nous l'ont déjà rendue indispensable. De l'autre côté, nous ne perdons absolument rien, car, les fonctions standards de comparaisons étant polymorphes, les types énumérés sont aussi bien ordonnés que les int. Pour l'exemple :

# ThreeOfAKind < FullHouse;;
- : bool = true
# compare Straight StraightFlush;;
- : int = -1

Toutefois il subsiste encore deux questions sans réponse :

• que décider en cas de combinaisons de force égale, par exemple comment comparer un brelan de dames avec un brelan de rois ? ;
• comment comparer deux mains opposant la même combinaison, par exemple une paire de dames contre une paire de dames ?

À ces deux problèmes OCaml apporte une seule et même solution :

• ou bien un variant n'attend aucun paramètre ;
• ou bien un variant attend exactement un paramètre.

Le paramètre d'un variant peut être de n'importe quel type et en particulier un type produit.
Un type énuméré est un type somme dégénéré, aucun de ses variants n'admet un paramètre.

Pour spécifier le paramètre d'un variant on utilise le mot-clé of suivi du type du paramètre.
Par exemple il est tout à fait judicieux de déclarer notre type poker_hand comme ceci :

type poker_hand =
  | HighCard of int * int * int * int * int
  | OnePair of int * int * int * int
  | TwoPair of int * int * int
  | ThreeOfAKind of int
  | Straight of int
  | Flush of int * int * int * int * int
  | FullHouse of int * int
  | FourOfAKind of int
  | StraightFlush of int
  ;;

Le type poker_hand réalise l'union disjointe de n-uplets, c'est donc un type somme de produits ou type algébrique (non récursif).

À variant égal la comparaison de deux valeurs de type poker_hand se fait selon l'ordre lexicographique sur les n-uplets.
Par exemple cet extrait de session compare dans l'ordre, deux cartes hautes, deux paires de dames, deux mains pleines, et pour fournir une quinte-flush au 8 face à une quinte-flush au 6 :

HighCard(king,queen,jack,10,7) > HighCard(king,queen,jack,10,5);;
- : bool = true
OnePair(queen,king,jack,10) > OnePair(queen,king,jack,7);;
- : bool = true
FullHouse(queen,jack) > FullHouse(queen,10);;
- : bool = true
StraightFlush(8) > StraightFlush(6);; 
- : bool = true

On appelle type inductif un type algébrique récursif.

La récursivité permet la création de types composites, avec un type inductif on peut créer des composants, c'est-à-dire des valeur-objets enfichables qui sont toujours du même type et qui sont traités de façon uniforme quelle que soit leur complexité.

Premier exemple :

Une liste de type 'a list est :

• ou bien la liste vide Nil ;
• ou bien une paire Cons formée d'une tête de type 'a et d'une queue de type 'a list.

Le type 'a list est donc un type inductif que l'on pourrait déclarer ainsi :

# type 'a list =
  | Nil
  | Cons of 'a * ('a list)
  ;;
type 'a list = Nil | Cons of 'a * 'a list

La liste 1::2::3::[] s'écrirait alors Cons(1,Cons(2,Cons(3,Nil))) et l'opérateur de concaténation s'implémenterait ainsi :

# let rec append l1 l2 =
  match l1 with
  | Nil -> l2
  | Cons(h,t) -> Cons(h,append t l2) 
  ;;
val append : 'a list -> 'a list -> 'a list = <fun>

Même si le type 'a list n'était pas prédéfini en OCaml nous pourrions encore l'implémenter simplement grâce à un type inductif.

Remarque : la définition du type list ci-dessus a écrasé la définition du type list prédéfini, celui-ci n'est plus disponible pour l'utilisateur, il vous faut redémarrer l'interpréteur pour avoir à nouveau accès au type list prédéfini que bien sûr nous allons continuer d'utiliser dans la suite de ce cours.

Autre exemple :

Au chapitre 33 nous n'avons pas réussi à implémenter les arbres n-aires à l'aide d'un couple (c'est-à-dire à l'aide d'un simple type produit), nous allons voir que ce qui faisait obstacle c'étaient la notion de type inductif qui nous manquait encore à ce moment.

Un arbre n-aire est :

• un nœud (node) contenant un élément et une liste de sous-arbres n-aires (récursivement).

La déclaration de ce type suit immédiatement :

# type 'a tree =
    Node of 'a * ('a tree list);;
type 'a tree = Node of 'a * 'a tree list

Pas de surprise, nos fonctions sur ces arbres n-aires sont tout à fait analogues à leurs cousines du chapitre 33 qui utilisaient un type enregistrement :

let rec rev_tree (Node(a,l)) =
  Node(a,List.rev_map rev_tree l);;

let rec map_tree f (Node(a,l)) =
  Node(f a,List.map (map_tree f) l);;

let rec exists_tree p (Node(a,l)) =
  p a or List.exists (exists_tree p) l;;

Une dernière utilisation des types inductifs est d'une importance particulière, ce sont les arbres de syntaxe abstraite qui modélisent les expressions, par exemple les expressions arithmétiques, ici avec les quatre opérateurs :

type arithmetic =
  | Int of int
  | Neg of arithmetic
  | Add of arithmetic * arithmetic
  | Sub of arithmetic * arithmetic
  | Mul of arithmetic * arithmetic
  | Div of arithmetic * arithmetic
  ;;

Ces types inductifs sont généralement accompagnés d'une fonction d'évaluation, soit eval pour notre exemple :

# let rec eval expr =
  match expr with
  | Int n -> n
  | Neg a -> - eval a
  | Add(a,b) -> eval a + eval b
  | Sub(a,b) -> eval a - eval b
  | Mul(a,b) -> eval a * eval b
  | Div(a,b) -> eval a / eval b
  ;;
val eval : arithmetic -> int = <fun>

On appelle fonction partielle une fonction dont le domaine de définition est strictement inclus dans son type.

Jusqu'ici nous avons contourné cette question du domaine de définition à l'aide :

• soit d'une assertion ;
• soit d'une exception.

Typiquement nous avions ce genre de comportement :

# eval (Div(Int 1, Int 0));;
Exception: Division_by_zero.

Non seulement l'interpréteur ne nous affiche pas de valeur, mais en plus il n'est même pas capable de nous afficher un type.
Une exception, au même titre qu'une assertion, est toujours un recours dynamique face à un constat d'échec du typage statique.
Ne peut-on pas typer eval statiquement, de manière totale, sûre et définitive ?

C'est possible, et la solution vient des types sommes.
Ce qu'il nous faut c'est transcrire le fait que le résultat de eval est :

• ou bien un entier ;
• ou bien l'échec d'une opération de division.

Une fois cette alternative intégrée dans le type de eval la fonction redeviendra forcément totale.

Le type result nous permet de généraliser cette alternative, un résultat result sera ou bien Ok ou bien une Error :

type ('a,'b) result =
  | Ok of 'a
  | Error of 'b
  ;;

Nous pouvons à présent écrire une version exception-less de notre évaluateur arithmétique :

# let rec eval expr =
  match expr with
  | Int n ->
     Ok n
  | Neg a ->
     ( match eval a with
     | Ok a -> Ok (-a)
     | _ -> Error "Division by 0")
  | Add(a,b) ->
     ( match eval a,eval b with
     | Ok a,Ok b -> Ok (a+b)
     | _,_ -> Error "Division by 0")
  | Sub(a,b) ->
     ( match eval a,eval b with
     | Ok a,Ok b -> Ok (a-b)
     | _,_ -> Error "Division by 0")
  | Mul(a,b) ->
     ( match eval a,eval b with
     | Ok a,Ok b -> Ok (a*b)
     | _,_ -> Error "Division by 0")
  | Div(a,b) ->
     ( match eval a,eval b with
     | Ok a,Ok b when b<>0 -> Ok (a/b)
     | _,_ -> Error "Division by 0")
  ;;
val eval : arithmetic -> (int, string) result = <fun>

Ce code contient trop de redites, certes nous n'avons plus d'exception, mais le calcul du résultat est comme obscurci par la gestion de la propagation de l'erreur. Nous allons remédier à cela.

À l'aide de ces trois petites fonctions utilitaires :

let ok1 v f =
  match v with
  | Ok x -> Ok (f x)
  | Error _ -> v
  ;;

let ok2 v1 v2 f =
  match v1,v2 with
  | Ok x1,Ok x2 -> Ok (f x1 x2) 
  | Error _, _ -> v1
  | _, Error _ -> v2
  ;;

let result2 v1 v2 f =
  match v1,v2 with
  | Ok x1,Ok x2 -> f x1 x2 
  | Error _, _ -> v1
  | _, Error _ -> v2
  ;;

Nous pouvons refactoriser la fonction eval comme ceci :

# let rec eval expr =
  match expr with
  | Int n ->
     Ok n
  | Neg a ->
     ok1 (eval a) (~-)
  | Add(a,b) ->
     ok2 (eval a) (eval b) (+)
  | Sub(a,b) ->
     ok2 (eval a) (eval b) (-)
  | Mul(a,b) ->
     ok2 (eval a) (eval b) ( * )
  | Div(a,b) ->
     result2
     (eval a) (eval b)
     (fun a b -> if b=0 then Error "Division by 0" else Ok (a/b))
  ;;
val eval : arithmetic -> (int, string) result = <fun>

C'est nettement plus clair !

Le bon point ici est que nos fonctions utilitaires sont universelles au sens où nous n'aurons pas à les réécrire, elles constituent une solution réutilisable au problème des fonctions partielles sur les types inductifs.

Nous allons l'illustrer sur un second exemple.
Il s'agit cette fois de dimensionner correctement une expression matricielle.
Le type grid nous servira de dimension matricielle :

type grid =
  {rows: int; columns: int};;

Tandis que le type mat_expr représentera une expression matricielle :

type mat_expr =
  | Mat of grid
  | MatNeg of mat_expr
  | MatTrans of mat_expr
  | MatPower of mat_expr * int
  | MatSum of mat_expr * mat_expr
  | MatProduct of mat_expr * mat_expr
  ;;

Avec pour opérations :

• la négation ;
• la transposée ;
• la puissance par un entier ;
• la somme ;
• le produit matriciel.

Le code de la fonction mat_size, qui dimensionne une expression matricielle, montre comment une solution exception-less passe à nouveau par les fonctions utilitaires ok1, ok2 et result2.

# let rec mat_size mat_expr = 
  match mat_expr with
  | Mat g ->
      Ok g
  | MatNeg m ->
      mat_size m
  | MatPower(m,n) ->
      mat_size m
  | MatTrans m ->
      ok1
      (mat_size m)
      (fun g -> {rows=g.columns;columns=g.rows})
  | MatSum(m1,m2) ->
      result2
      (mat_size m1)
      (mat_size m2)
      (fun g1 g2 ->
         if g1 = g2 then Ok g1
         else Error "Addition of different sized matrices")
  | MatProduct(m1,m2) ->
      ok2
      (mat_size m1) 
      (mat_size m2)
      (fun g1 g2 -> {rows=g1.rows;columns=g2.columns})
  ;;
val mat_size : mat_expr -> (grid, string) result = <fun>

On appelle catamorphisme une fonction qui réalise un parcours canonique sur un type inductif.

Le type inductif le plus élémentaire est le type list, le module List fournit deux sortes de parcours sur les listes :

• la fonction fold_right effectue un parcours récursif, on pourrait l'implémenter comme ceci :

let rec fold_right f l init =
  match l with
  | [] -> init
  | h::t -> f h (fold_right f t init)
  ;;

• la fonction fold_left effectue un parcours récursif terminal, on pourrait l'implémenter comme ceci :

let rec fold_left f init l =
  match l with
  | [] -> init
  | h::t -> fold_left f (f init h) t
  ;;

Plutôt que ces implémentations un peu ardues, essayons de donner une définition d'un catamorphisme de liste :

• l'image de [] par un catamorphisme est la valeur initiale init ;
• la fonction f attend deux arguments ;
• soit $$ un opérateur infixe égal à la fonction f et que l'on pourrait déclarer ainsi :

let ($$) = f;;

• alors l'image d'une liste a0::a1:: ... ::an::[] par un catamorphisme est la valeur a0$$a1$$ ... $$an$$init.

En résumé :

• le constructeur inital [] est remplacé par la valeur initiale init ;
• chaque constructeur :: est remplacé par l'opérateur $$.

Le module Seq qui suit illustre la généralité des catamorphismes fold_left et fold_right, cette implémentation d'une partie de la signature du module List est surprenante de concision :

module Seq = struct
  let rec fold_left f init l =
    match l with
    | [] -> init
    | h::t -> fold_left f (f init h) t
  let rec fold_right f l init =
    match l with
    | [] -> init
    | h::t -> f h (fold_right f t init)
  let length l = fold_left (fun a b -> a+1) 0 l
  let rev l = fold_left (fun a b -> b::a) [] l
  let append l1 l2 = fold_right (fun a b -> a::b) l1 l2
  let rev_append l1 l2 = fold_left (fun a b -> b::a) l2 l1
  let iter f l = fold_left (fun a b -> f b) () l
  let map f l = fold_right (fun a b -> f a::b) l []
  let rev_map f l = fold_left (fun a b -> f b::a) [] l
  let flatten l = fold_right append l []
  let for_all f l = fold_left (fun a b -> f b && a) true l
  let exists f l = fold_left (fun a b -> f b or a) false l
  let mem x l = fold_left (fun a b -> x=b or a) false l
  let filter f l = fold_right (fun a b -> if f a then a::b else b) l []
  let partition f l = fold_right (fun a (p,q) -> if f a then (a::p,q) else (p,a::q)) l ([],[])
  let split l = fold_right (fun (a,b) (p,q) -> (a::p,b::q)) l ([],[])
end;;

Le cas des arbres binaires est également intéressant.

Un arbre binaire est :

• ou bien une feuille (leaf) sans élément ;
• ou bien un noeud (node) contenant un élément et deux sous-arbres binaires (récursivement).

Le module BinaryTree qui suit introduit un type tree et son catamorphisme fold, ensuite il utilise fold pour implémenter la taille (size), la profondeur (depth), le nombre de Strahler (strahler), puis d'autres fonctions de parcours de même sémantique que leurs homonymes sur les listes :

module BinaryTree = struct 
  type 'a tree =
    | Leaf
    | Node of ('a tree) * 'a * ('a tree)
  let fold f init t =
    let rec loop t = 
      match t with
      | Leaf -> init
      | Node(l,a,r) -> f (loop l) a (loop r)
    in loop t
  let size t  = fold (fun l a r -> l + r + 1) 0 t
  let depth t = fold (fun l a r -> max l r + 1) 0 t
  let strahler t = fold (fun l a r -> if l=r then l+1 else max l r) 1 t
  let rev t = fold (fun l a r -> Node(r,a,l)) Leaf t
  let iter f t = fold (fun l a r -> f a) () t
  let map  f t = fold (fun l a r -> Node(l,f a,r)) Leaf t
  let flatten t = fold (fun l a r -> l @ a::r) [] t
  let for_all f t = fold (fun l a r -> l && r && f a) true t
  let exists  f t = fold (fun l a r -> l or r or f a) false t
  let mem x t = fold (fun l a r -> l or r or x=a) false t
  let split t = fold (fun (m,q) (a,b) (p,r) -> Node(m,a,p),Node(q,b,r)) (Leaf,Leaf) t
end;;

Nous vous renvoyons à la thèse de Nicolas Janey pour une définition des nombres de Horton-Strahler (lire les paragraphes 3.2.1 à 3.2.3) et pour leur application en botanique, en hydrogéologie et en topologie.

Le module BinaryTree se prête volontiers à une généralisation aux arbres n-aires tels que nous les avons définis au chapitre 57.
Ce sera le module NaryTree qui, après la définition du type tree et l'introduction des ses deux catamorphismes fold_left et fold_right, implémente les opérations sur les arbres n-aires, toujours avec une extrême concision :

module NaryTree = struct 
  type 'a tree =
    Node of 'a * ('a tree list)
  let fold_left g f init t =
    let rec helper (Node(a,l)) =
      let loop = List.fold_left (fun a b -> f (helper b) a) init l
      in  g a loop
    in helper t
  let fold_right g f init t =
    let rec helper (Node(a,l)) =
      let loop = List.fold_right (fun a b -> f (helper a) b) l init 
      in  g a loop
    in helper t
  let cons a b = a::b
  let size t = fold_left (fun a l -> l + 1) (+)  t
  let depth t = fold_left (fun a l -> l + 1) max 1 t
  let rev t = fold_left (fun a l -> Node(a,l)) cons [] t
  let iter f t = fold_left (fun a l -> f a) (fun a b -> ()) () t
  let map f t = fold_right (fun a l -> Node(f a,l)) cons [] t
  let rev_map f t = fold_left (fun a l -> Node(f a,l)) cons [] t
  let flatten t = fold_left cons (@) [] t
  let for_all f t = fold_left (fun a l -> l && f a) (&&) true t
  let exists  f t = fold_left (fun a l -> l or f a) (||) false t
  let mem x t = fold_left (fun a l -> l or x=a) (||) false t
end;;

À ce stade on peut se demander à quoi servent les catamorphismes.
Après tout on a déjà le filtrage qui est une facilité très puissante.
Et les modules exportent d'autres facilitées plus immédiates comme rev, map ou filter.
Alors on peut penser que les catamorphismes c'est concis, le concept est élégant, mais en pratique ce qui compte c'est l'inferface d'un module et non la concision de son implémentation.

Sans vouloir minimiser le bien-fondé de ces deux remarques, il faut tout de même dire que le programmeur fonctionnel expérimenté ne peut pas complètement faire l'économie des catamorphismes.

Pour deux raisons principales :

• en tant qu'utilisateur d'un module le programmeur fonctionnel peut être confronté à une situation où son besoin n'est pas couvert par l'interface du module (les fonctions classiques rev, map ou filter...). Dans ce cas il ne peut pas non plus coder son propre parcours à l'aide du filtrage, car l'implémentation du type à parcourir est cachée par le module, on ne connaît pas son schéma, on ne peut pas filtrer ses valeurs. Il ne reste alors plus qu'une option disponible: paramétrer le fold dont le bon implémenteur de module aura eu soin d'équiper son interface ;
• en tant qu'implémenteur de composants certifés ou critiques, paramétrer un fold est une option plus sûre, car on ne peut pas faire une récursion mal fondée. Un catamorphisme est structurellement bien fondé, l'utiliser c'est déjà une preuve de terminaison, mais surtout c'est une base pour le raisonnement inductif et un premier pas important vers la preuve de programme.

Comme nous avons déjà vu beaucoup d'exemples de modules, jusqu'à la fin de ce chapitre nous allons nous placer dans le cadre plus confidentiel de la preuve de programme. Aussi, si vous n'êtes pas intéressé par la preuve de programme, vous pouvez sans conséquence aucune faire l'impasse sur cette fin de partie VIII.

Sinon vous allez voir comment remplacer la récursion par l'utilisation systématique de schémas de récursion afin de faciliter le raisonnement inductif.
Pour l'exemple nous allons nous concentrer sur les arbres binaires et le type :

  type 'a tree =
    | Leaf
    | Node of ('a tree) * 'a * ('a tree)

Avec l'intention de lui adjoindre des opérations classiques comme member, insert et remove, autant dire que ce que nous voulons spécifier ce n'est plus un simple arbre binaire, mais bien un arbre binaire de recherche (binary search tree).

Un arbre binaire de recherche est un arbre binaire qui vérifie les deux propriétés suivantes :

• l'élément porté par un fils gauche est toujours strictement plus petit que l'élément porté par son parent ;
• l'élément porté par un fils droit est toujours strictement plus grand que l'élément porté par son parent.

Comme nous l'avons déjà mentionné à maintes reprises, le système de types d'OCaml n'est que structurel, il n'est pas capable de distinguer un arbre binaire ordonné (par la propritété ci-dessus) d'un simple arbre binaire quelconque. Si bien que nous allons recourir au pis aller habituel : un prédicat ordered nous dit si un arbre binaire est ordonné et ce prédicat nous sert de précondition pour les fonctions member, insert et remove.

  let fold init f t =
    let rec loop t = 
      match t with
      | Leaf -> init
      | Node(l,a,r) -> f (loop l) a (loop r)
    in loop t

Ce fold devrait faire l'affaire, il devrait suffire de le paramétrer pour obtenir le prédicat ordered que nous voulons.
Malheureusement ce que l'on cherche c'est à encadrer chaque arbre par un minorant et un majorant, or Leaf ne porte aucune valeur, dans ces conditions il n'est pas facile de l'encadrer, et pas facile non plus d'encadrer son parent.

Le prédicat ordered serait plus évident à implémenter si nous avions toujours accès à au moins une valeur initiale, il serait plus confortable que chaque feuille contienne au moins un élément.
Après tout OCaml exige bien une valeur initiale pour créer une référence ou pour créer un tableau alors pourquoi pas pour quelque chose de plus compliqué comme un arbre binaire de recherche ?
Sans plus d'états d'âme, nous interdisons carrément qu'un arbre binaire soit vide :

type 'a tree =
  | One  of 'a
  | Pair of 'a * 'a
  | Node of ('a tree) * 'a * ('a tree)

Puis nous équipons cet arbre binaire de son catamorphisme canonique :

let cata_rec one pair node t =
  let rec loop t = 
    match t with
    | One a -> one a
    | Pair(a,b) -> pair a b
    | Node(l,a,r) -> node (loop l) a (loop r)
  in loop t

Est-ce qu'au moins cela nous facilite l'implémentation du prédicat ordered ? Oui, car il est désormais facile d'encadrer n'importe quel arbre par un intervalle (minorant, majorant) :

let ordered t =
  let a,b =
    cata_rec
    (fun a -> a,a)
    (fun a b -> a,b)
    (fun (l1,l2) a (r1,r2) ->
       if l1>l2 then l1,l2
       else if l2>a then l2,a
       else if a>r1 then a,r1
       else if r1>r2 then r1,r2
       else l1,r2
    )
    t
  in a<=b

Muni de ce prédicat et de notre catamorphisme canonique rien n'est plus simple que d'implémenter member c'est-à-dire une fonction de recherche d'un élément x dans t (un arbre binaire ordonné) :

let member x t =
  assert(ordered t);
  cata_rec
  (fun a -> x=a)
  (fun a b -> x=a or x=b)
  (fun l a r -> l or x=a or r)
  t

Mais attendez voir... c'est exactement la même fonction que mem, la recherche dans un arbre binaire quelconque! Où est l'intérêt d'un arbre binaire de recherche s'il n'accélère pas la recherche ?
Nous voudrions pouvoir rechercher un élément dans un temps proportionnel à la profondeur de l'arbre, et pas dans un temps proportionnel à sa taille.

Comment empêcher notre catamorphisme de parcourir l'arbre en totalité ?
Ce qu'il nous faudrait c'est un parcours moins avide, un parcours qui se laisse diriger. Ce parcours plus lazy nous l'appellerons caty_rec, il est le frère de cata_rec, le même en plus paresseux :

let caty_rec one pair node t =
  let rec loop t () =
    match t with
    | One a -> one a
    | Pair(a,b) -> pair a b
    | Node(l,a,r) -> node (loop l) a (loop r)
  in loop t ()

Et il nous permet d'effectuer notre recherche en temps logarithmique :

let member x t =
  assert(ordered t);
  caty_rec
  (fun a -> x=a)
  (fun a b -> x=a or x=b)
  (fun l a r ->
     if x < a then l()
     else if x > a then r()
     else true)
  t

Autant le dire tout de suite : le plus difficile est encore devant nous, car il reste les opérations d'insertion (insert) et de suppression (remove).

Comment aborder l'insertion ?
Avec les mêmes exigences que pour l'appartenance : nous ne voulons pas reconstruire tout l'arbre, mais seulement le chemin qui mène à la nouvelle feuille.
Or, pour ne reconstruire que ce chemin, nous avons besoin de ses effluents, c'est-à-dire des anciennes composantes de chaque nœud que nous voulons remplacer.
Comme diraient les anglophones nous voulons 'eat our cake and have it too', et cela un catamorphisme ne nous le permet pas.

En résumé nous voulons à la fois :

• manger un nœud ;
• l'avoir encore sous les yeux et dans la main ;
• rester paresseux (ne pas parcourir tout l'arbre).

C'est ce petit miracle (ou plutôt ce schéma de récursion) que nous appellerons paramorphisme.
Pour un arbre binaire il prendra cette forme :

let para_rec one pair node t =
  let rec loop t () = 
    match t with
    | One a -> one a
    | Pair(a,b) -> pair a b
    | Node(l,a,r) -> node (l,loop l) a (r,loop r)
  in loop t ()

Avec cette baguette magique, l'insertion d'un élément x ne pose plus vraiment problème :

let insert x t =
  assert(not(member x t));
  para_rec
  (fun a -> if x > a then Pair(a,x) else Pair(x,a))
  (fun a b ->
     if x > b then Node(One a,b,One x)
     else if x < a then Node(One x,a,One b)
     else Node(One a,x,One b)
  )
  (fun (l1,l2) a (r1,r2) ->
     if x < a then Node(l2(),a,r1)
     else Node(l1,a,r2())
  )
  t

D'ailleurs notre baguette est tellement magique, utilisons-la vite avant qu'on nous la confisque !
Vite, nous enlevons le minorant d'un arbre binaire de recherche :

let remove_min t =
  assert(ordered t);
  para_rec
  (fun a -> One a,a)
  (fun a b -> One b,a) 
  (fun (l1,l2) a (r1,r2) ->
     match l1 with
     | One b -> r1,b
     | _ -> let b,c = l2() in Node(b,a,r1),c
  ) 
  t

Grâce à quoi nous pouvons finalement retirer un élément x quelconque :

let remove x t =
  assert(member x t);
  para_rec
  (fun a -> One a)
  (fun a b -> if x > a then One a else One b)
  (fun (l1,l2) a (r1,r2) ->
     if x < a then Node(l2(),a,r1)
     else if x > a then Node(l1,a,r2())
     else
       match l1,r1 with 
       | One b,One c -> Pair(b,c)
       | One _,Node(_,_,_) -> r1
       | Node(_,_,_),One _ -> l1
       | Pair(b,c),One d | One b,Pair(c,d) ->
           Node(One b,c,One d)
       | _,_ ->
           let b,c = remove_min r1 in Node(l1,c,b)
  )
  t

Et voilà !
Nous avons implémenté un Type Abstrait de Données récursif sans utiliser directement aucune récursion.

Si vous souhaitez approfondir le sujet et faire connaissance avec de nouveaux schémas de récursion (anamorphismes, hylomorphismes, apomorphismes) je ne peux que vous recommander la lecture de Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire par Fokkinga.