Probleme – Un module OCaml compilé : ce que la signature refuse

1. Le module.

(* ensemble.mli -- l'INTERFACE. Le type n'a pas de definition ici. *)
type t
val vide : t
val ajouter : int -> t -> t
val appartient : int -> t -> bool
val cardinal : t -> int

(* ensemble.ml -- la REALISATION.
   INVARIANT : la liste est triee par ordre strictement croissant. *)
type t = int list
let vide = []
let rec ajouter x = function
  | [] -> [x]
  | y :: r when x < y -> x :: y :: r
  | y :: r when x = y -> y :: r          (* deja present : rien a faire *)
  | y :: r -> y :: ajouter x r
let rec appartient x = function
  | [] -> false
  | y :: _ when x = y -> true
  | y :: _ when x < y -> false           (* triee : on peut s'arreter *)
  | _ :: r -> appartient x r
let cardinal = List.length

2. La compilation et l'usage.

ocamlc ensemble.mli ensemble.ml usage.ml -o usage

(* usage.ml *)
let e = Ensemble.ajouter 3 (Ensemble.ajouter 1 (Ensemble.ajouter 3 Ensemble.vide))
let () = Printf.printf "cardinal = %d, 1 present : %b, 2 present : %b\n"
           (Ensemble.cardinal e) (Ensemble.appartient 1 e) (Ensemble.appartient 2 e)

Mesuré : cardinal = 2, 1 present : true, 2 present : false. L'ajout répété de $3$ n'a produit qu'un élément : l'invariant « sans doublon » est tenu par ajouter, et lui seul en est responsable.

3. Ce que la signature refuse. On tente de fabriquer un ensemble à la main, ni trié ni sans doublon :

let e : Ensemble.t = [2; 1; 1]

Error: This constructor has type 'a list
       but an expression was expected of type Ensemble.t

Le compilateur ne sait plus que Ensemble.t est une liste — la signature le lui a caché. Toute valeur du type est donc sortie de vide ou de ajouter, et l'invariant tient par récurrence sur la construction : c'est une preuve, pas une convention.

4. Sans le .mli. On compile les deux mêmes fichiers, sans l'interface :

ocamlc -c ensemble.ml && ocamlc -c fraude.ml     -->  les deux compilent

La ligne let e : Ensemble.t = [2; 1; 1] passe. En l'absence de .mli, OCaml expose la signature complète, définition du type comprise : Ensemble.t est int list, et l'invariant n'est plus protégé par rien. appartient 1 rendrait alors false sur [2;1;1], puisqu'elle s'arrête au premier élément supérieur.

Le fichier .mli n'est donc pas de la documentation, et c'est l'enseignement du problème : c'est lui qui transforme un commentaire d'invariant en une propriété vérifiée par le compilateur. Le typedef struct pile_s pile; de C joue exactement le même rôle, avec la même conséquence — et c'est en cela que les deux langages, si différents par ailleurs, réalisent la même idée de structure abstraite.