L'invariant que seule l'abstraction protège

type frac = { num : int; den : int }
let cree n d = let g = pgcd (abs n) (abs d) in { num = n/g; den = d/g }
let egales f1 f2 = f1.num = f2.num && f1.den = f2.den

Mesuré :

cree 2 4 = 1/2, cree 1 2 = 1/2 : egales dit true
{ num = 2; den = 4 } contre cree 1 2 : egales dit false

Le défaut. cree maintient l'invariant « la fraction est réduite », et tant qu'on passe par elle, egales est correcte. Mais rien n'oblige à passer par elle : la notation d'enregistrement

let brute = { num = 2; den = 4 }        (* ni reduite, ni passee par cree *)

construit directement une valeur du type, hors de tout contrôle, et egales brute (cree 1 2) rend false alors que les deux fractions valent un demi. L'invariant n'est pas garanti par le type, il est seulement garanti par la politesse de l'utilisateur — et une politesse n'est pas une preuve.

La correction consiste à rendre le type abstrait, en le déclarant dans une signature sans sa définition :

(* frac.mli *)
type t                              (* la definition n'apparait PAS *)
val cree : int -> int -> t          (* la seule entree dans le type *)
val egales : t -> t -> bool
val num : t -> int
val den : t -> int

Dès lors, tout habitant du type Frac.t est sorti de cree, donc est réduit, et egales devient correcte par construction. Vérifié : la tentative de fabriquer une valeur du type à la main est rejetée à la compilation,

let f : Frac.t = { Frac.num = 2; den = 4 }
Error: Unbound record field Frac.num

et le message dit exactement ce qui se passe — les champs ne sont pas seulement interdits, ils sont invisibles : la signature ne les mentionne pas, donc ils n'existent pas hors du module.

La formulation générale, et c'est la vraie raison d'abstraire : une structure de données abstraite est un type dont toutes les valeurs satisfont un invariant, parce que toutes les portes d'entrée sont dans le module. Le programme le dit en termes de modularité ; c'est la même chose vue de l'autre côté. Retenir le critère de la fin du chapitre : on abstrait ce dont l'invariant est fragile — et un invariant qu'un utilisateur peut casser en une ligne est exactement cela.