Pour accéder à la documentation officielle du langage
Objective-Caml cliquez sur le chameau ci-dessus.
Pour toute interrogation suscitée par
L'approche qualité avec Objective-Caml veuillez exposer ce qui vous fait obstacle dans
le fil de discussion réservé à cet effet.
Partie VIII. Les types algébriques
On appelle
type algébrique un type qui réalise la
somme de produits de types.
Ce vocabulaire sera défini en deux chapitres :
- le chapitre 54 a pour objet de définir la nature d'un type produit
- le chapitre 55 a pour objet de définir la nature d'un type somme
La connaissance des
types somme et des
types produit entraîne la connaissance des
types algébriques.
Les
types inductifs sont des
types algébriques récursifs et feront l'objet du
chapitre 56.
Enfin, les
schémas de récursion les plus courants seront présentés dans les
chapitres 58 et 59.
- Ordre lexicographique
- Les types produit
- Les types somme
- Les types inductifs
- Le typage des fonctions partielles
- Les catamorphismes
- Les paramorphismes
53. Ordre lexicographique
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 1
ier caractère, en cas d'égalité on compare le 2
nd, puis éventuellement le 3
ième, 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>
|
|
54. Les types produit
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
55. Les types somme
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 5 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 1 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
|
|
56. Les types inductifs
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 noeud (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 4 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>
|
|
57. Le typage des fonctions partielles
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 obscurcit 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 répré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>
|
|
58. Les catamorphismes
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 :
- 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 reprise 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'appèlerons
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
|
|
59. Les paramorphismes
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 noeud 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ésumer nous voulons à la fois :
- manger un noeud
- 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 appelerons
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 bagette 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.
Copyright © 2007 Damien Guichard.
Permission is granted to copy and distribute under the terms of the Creative Commons licence, Version 3.0 or any later version published by the Creative Commons Corporation; with Attribution, No Commercial Use and No Derivs. Read the full license here : http://creativecommons.org/licenses/by-nc-nd/3.0/legalcode