juin
2010
Un article de SpiceGuid
Un exercice simple pour débutant en ocaml c’est d’écrire un interpréteur pour un petit langage simple comme par exemple une calculatrice :
type arithmetic = | Cst of int | Neg of arithmetic | Add of binary | Sub of binary | Mul of binary | Div of binary and binary = arithmetic * arithmetic
Mais cet exercice anodin change complètement de nature quand on passe à un langage fortement normalisant, dans ce cas vous devez aussi prouver que le programme se termine toujours et sans accident, quelles que soient les circonstances.
Cette preuve ce fait en deux étapes :
- d’abord il changer d’algèbre initiale
- ensuite il faut établir une égalité entre les deux types algébriques
Le changement d’algèbre initiale se fait en paraphrasant la déclaration du type, en remplaçant chaque occurrence de arithmetic par une occurrence de fold f :
let rec fold f = function | Cst n -> f#cst n | Neg a -> f#neg (fold f a) | Add (a,b) -> f#add (fold f a) (fold f b) | Sub (a,b) -> f#sub (fold f a) (fold f b) | Mul (a,b) -> f#mul (fold f a) (fold f b) | Div (a,b) -> f#div (fold f a) (fold f b)
Le paramètre f est une égalité entre les deux types algébriques :
let id x = x
let eval =
fold (
object
method cst = id
method neg = (~-)
method add = ( + )
method sub = ( - )
method mul = ( * )
method div = ( / )
end )
À cette étape on est à l’abri des boucles infinies.
Mais on n’est pas à l’abri des interruptions intempestives, par exemple lors d’une division par zéro.
# eval (Div(Cst 1,Cst 0));; Exception: Division_by_zero.
Dans les langages fortements normalisants les exceptions n’existent pas.
Pour simuler les exceptions on utilise la monade result pour propager le diagnostic d’erreur.
type ('a,'b) result =
| Ok of 'a
| Error of 'b
let ok1 f v =
match v with
| Ok x -> Ok (f x)
| Error _ -> v
let ok2 f v1 v2 =
match v1,v2 with
| Ok x1,Ok x2 -> Ok (f x1 x2)
| Error _, _ -> v1
| _, Error _ -> v2
let result2 f v1 v2 =
match v1,v2 with
| Ok x1,Ok x2 -> f x1 x2
| Error _, _ -> v1
| _, Error _ -> v2
let safe_division a b =
if b=0 then Error "Division_by_zero"
else Ok (a/b)
À l’aide de cette monade result on peut définir une nouvelle égalité qui prend en compte les possibilités d’erreur :
let ok n = Ok n
let eval =
fold (
object
method cst = ok
method neg = ok1 (~-)
method add = ok2 ( + )
method sub = ok2 ( - )
method mul = ok2 ( * )
method div = result2 safe_division
end )
Cette fois le programme suit son cours jusqu’au bout, sans interruption :
# eval (Div(Cst 1,Cst 0));; - : (int, string) result = Error "Division_by_zero"
Bien sûr un tel raffinement de style n’est pas forcément utile ou même désirable dans chaque code ocaml. Le langage étant multi-paradigmes par nature il vous invite à trouver le style qui vous convient le mieux.
Cependant, avec cette introduction courte et informelle sur les récurseurs et les monades, j’espère avoir donné quelques encouragements à ceux qui voudraient faire le grand saut vers un assistant de preuve.
– damien