informatique (MP2I/MPI) · Chapitre 6 · Application directe du cours
Lire un type sans l'écrire
Types et structures de données abstraites · niveau 2
Énoncé
Donner le type inféré par OCaml pour chacune de ces définitions, et dire d'où vient chaque contrainte.
let f x y = x :: y
let g t i = t.(i) <- 0
let h l = List.map (fun x -> x + 1) l
let m t = Array.make (Array.length t) t.(0)
let compose f g x = f (g x)Corrigé
Vérifié avec ocamlc -i, qui affiche la signature inférée sans produire d'exécutable :
val f : 'a -> 'a list -> 'a list
val g : int array -> int -> unit
val h : int list -> int list
val m : 'a array -> 'a array
val compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'bD'où viennent les contraintes.
f:::exige que sa gauche ait le type des éléments de sa droite. Rien d'autre n'est imposé, d'où la variable'a: la fonction est polymorphe.g: l'affectation<- 0force le type des éléments àint; l'indice d'un tableau est unint; et une affectation ne rend rien, d'oùunit.h: le+ 1forceintdes deux côtés. Une seule opération arithmétique suffit à fermer tout le type.m: rien n'est fait des valeurs, seulement de leur nombre ; le type reste donc paramétré.compose: la sortie degdoit être l'entrée def, d'où la même variable'aaux deux endroits. Trois variables, trois libertés indépendantes.
Ce que l'exercice éprouve, et c'est tout ce que le programme demande — « un étudiant est capable d'inférer un type à la lecture d'un fragment de code, cependant toute théorie du typage est hors programme » : on lit les contraintes que les opérations imposent, on n'applique aucun algorithme d'unification.
Un piège dans m. Le type est correct, la fonction ne l'est pas toujours : Array.make n v met la même valeur v dans les cases. Si t.(0) est lui-même un objet mutable, les cases le partagent. C'est le neuvième exercice de cette série.
