Lire un type sans l'écrire

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)

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 -> 'b

D'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 <- 0 force le type des éléments à int ; l'indice d'un tableau est un int ; et une affectation ne rend rien, d'où unit.
• h : le + 1 force int des 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 de g doit être l'entrée de f, d'où la même variable 'a aux 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 $n$ cases. Si t.(0) est lui-même un objet mutable, les $n$ cases le partagent. C'est le neuvième exercice de cette série.