Aller au contenu

Principe

En OCaml, chaque valeur a un unique type. On note x : t pour dire que x est du type t.

Quand on évalue une expression, OCaml répond ainsi avec son type :

# 2+3;;
- : int = 5

Le - signifie qu'on n'a pas nommé l'expression, si on écrit un let, on aura le nom associé (précédé de val) :

# let x = 2+3;;
val x : int = 5

OCaml déduit tout seul le type d'une expression par un algorithme appelé l'inférence de types.

Si on écrit x+y, comme l'opération plus ne peut se faire qu'avec des valeurs du type int, OCaml sait que x et y doivent être du type int.

Pour des fonctions, OCaml procède de même : il déduit le type des arguments et celui du résultat de la manière dont ils sont utilisés dans le corps de la fonction.

Ainsi let f x y = x + y va avoir le type int -> int -> int : x et y sont des int car ils sont arguments de +, et le résultat est un int car c'est le résultat d'une addition.

Types génériques

Quand on écrit let f x = x, OCaml n'a aucune contrainte sur le type de x. Dans ce cas, il utilise une variable de type 'a signifiant n'importe quel type :

# let f x = x;;
val f : 'a -> 'a = <fun>

Quand 'a apparait dans un type, on peut le remplacer par n'importe quel type du moment qu'on remplace de même toutes ses occurrences. On parle de spécialisation d'un type. Ainsi int -> int spécialise 'a -> 'a.

Principe de l'inférence

On présente ici, de manière informelle, la méthode suivie par OCaml pour trouver le type d'une expression. Elle est due à Hindley et Milner et se décompose en trois temps :

  1. on attribue une variable de type inconnue à chaque sous-expression dont on ne connait pas encore le type ;
  2. on parcourt l'expression et chaque construction impose des contraintes, c'est-à-dire des équations entre types ;
  3. on résout ces équations : c'est l'unification.

Variables de type et contraintes

Dans la suite, on note \(\alpha, \beta, \gamma, \dots\) les inconnues qui représentent des types non encore déterminés. Les contraintes proviennent des règles suivantes :

  • une constante a un type connu : 1 : int, true : bool, (+) : int -> int -> int, ... ;
  • si e1 e2 est une application avec e1 : t1 et e2 : t2, on introduit une nouvelle inconnue \(\alpha\) pour le type du résultat et on pose la contrainte \(t_1 = t_2 \to \alpha\) ;
  • pour fun x -> e, on donne une nouvelle inconnue \(\alpha\) à x et, si e : t, l'expression a le type \(\alpha \to t\) ;
  • pour if c then e1 else e2, on pose c : bool et on impose que e1 et e2 aient le même type, qui est celui de l'expression.

Exemple

Considérons let f g x = g (x + 1), c'est-à-dire let f = fun g -> fun x -> g (x + 1).

  • On pose g \(: \alpha\) et x \(: \beta\).
  • Dans x + 1, l'opérateur + est de type int -> int -> int : on obtient les contraintes \(\beta = \texttt{int}\) et x + 1 : int.
  • Dans g (x + 1), on applique g à une valeur de type int, on introduit donc une inconnue \(\gamma\) pour le résultat et la contrainte \(\alpha = \texttt{int} \to \gamma\).

Le type de f est \(\alpha \to \beta \to \gamma\), qui devient, en remplaçant les inconnues déterminées, \((\texttt{int} \to \gamma) \to \texttt{int} \to \gamma\). L'inconnue \(\gamma\) n'est soumise à aucune contrainte, elle devient une variable de type générique 'a :

# let f g x = g (x + 1);;
val f : (int -> 'a) -> int -> 'a = <fun>

Unification

Résoudre les contraintes consiste à trouver une substitution, c'est-à-dire un remplacement de certaines inconnues par des types, qui rend chaque équation vraie. On traite les équations une par une :

  • \(t = t\) : rien à faire, on la supprime ;
  • \(\alpha = t\) (ou \(t = \alpha\)) où \(\alpha\) n'apparait pas dans \(t\) : on remplace \(\alpha\) par \(t\) dans toutes les autres équations et on retient \(\alpha := t\) ;
  • \(t_1 \to t_2 = t_1' \to t_2'\) : on remplace cette équation par les deux équations \(t_1 = t_1'\) et \(t_2 = t_2'\) (de même pour les couples, les listes, ...) ;
  • deux types de formes différentes, comme \(\texttt{int} = \texttt{bool}\) ou \(\texttt{int} = t_1 \to t_2\) : il n'y a pas de solution, c'est une erreur de typage ;
  • \(\alpha = t\) où \(\alpha\) apparait dans \(t\) sans être égal à \(t\) : pas de solution non plus, car un type est une expression finie.

Exemple

Déroulons l'inférence sur let compose f g x = f (g x).

  • On pose f \(: \alpha\), g \(: \beta\), x \(: \gamma\).
  • Pour g x, on introduit \(\delta\) et la contrainte \(\beta = \gamma \to \delta\).
  • Pour f (g x), on introduit \(\varepsilon\) et la contrainte \(\alpha = \delta \to \varepsilon\).

Le type cherché est \(\alpha \to \beta \to \gamma \to \varepsilon\). Les deux équations sont de la forme « inconnue = type » sans occurrence de l'inconnue à droite, on obtient la substitution \(\beta := \gamma \to \delta\), \(\alpha := \delta \to \varepsilon\) et le type

\[ (\delta \to \varepsilon) \to (\gamma \to \delta) \to \gamma \to \varepsilon \]

Il reste trois inconnues libres que OCaml renomme dans l'ordre d'apparition : \(\delta\) devient 'a, \(\varepsilon\) devient 'b et \(\gamma\) devient 'c.

# let compose f g x = f (g x);;
val compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b = <fun>

Exemple

Pour let h x = if x then 1 else x, on pose x \(: \alpha\). La condition impose \(\alpha = \texttt{bool}\) et les deux branches imposent \(\texttt{int} = \alpha\). Après la substitution \(\alpha := \texttt{bool}\), la seconde équation devient \(\texttt{int} = \texttt{bool}\) : erreur.

# let h x = if x then 1 else x;;
Line 1, characters 27-28:
1 | let h x = if x then 1 else x;;
                               ^
Error: The value x has type bool but an expression was expected of type int

Le message d'erreur indique l'endroit où l'unification a échoué, qui n'est pas forcément l'endroit où se trouve l'erreur du programmeur : ici, le then 1 est peut-être le vrai coupable. C'est une source classique d'incompréhension, il faut alors relire tout le code qui a contribué au type.

Exemple

Pour let k f = f f, on pose f \(: \alpha\) et l'application impose \(\alpha = \alpha \to \beta\) : \(\alpha\) apparait à droite, il n'y a pas de solution.

# let k f = f f;;
Line 1, characters 12-13:
1 | let k f = f f;;
                ^
Error: The value f has type 'a -> 'b but an expression was expected of type
         'a
       The type variable 'a occurs inside 'a -> 'b

Remarque

On peut montrer que lorsque les contraintes admettent une solution, cette méthode trouve la plus générale : toute autre solution s'obtient en spécialisant celle-ci (admis). C'est ce qui permet à OCaml d'afficher le type d'une expression.

Polymorphisme du let

Une fois le type d'une définition let x = e obtenu, les inconnues qui y restent libres sont généralisées : elles deviennent des variables de type 'a, 'b, ... qu'on pourra spécialiser différemment à chaque utilisation de x.

# let id x = x in (id 1, id true);;
- : int * bool = (1, true)

Ici, id : 'a -> 'a est utilisée une fois avec 'a = int et une fois avec 'a = bool.

En revanche, un argument de fonction n'est pas généralisé : à l'intérieur du corps, son type est une unique inconnue, qui ne peut être unifiée qu'avec un seul type.

# (fun id -> (id 1, id true)) (fun x -> x);;
Line 1, characters 21-25:
1 | (fun id -> (id 1, id true)) (fun x -> x);;
                         ^^^^
Error: The constructor true has type bool
       but an expression was expected of type int

L'utilisation id 1 a imposé \(\alpha = \texttt{int} \to \beta\), et id true impose alors \(\texttt{int} = \texttt{bool}\). Pourtant, ce programme ne provoquerait aucune erreur à l'exécution : c'est une limite assumée de l'inférence, qui reste ainsi simple et efficace.

Restriction de valeur

La généralisation n'est pas toujours possible en présence de traits impératifs. Si on écrivait let r = ref [] avec r : 'a list ref, on pourrait faire r := [1] puis utiliser !r comme une bool list : le typage ne garantirait plus rien.

Pour l'éviter, OCaml ne généralise que les définitions dont la partie droite est une valeur (une constante, une fonction fun ..., un constructeur appliqué à des valeurs, ...) et pas un calcul comme une application. Les inconnues non généralisées sont affichées '_weak1, '_weak2, ... : elles représentent un type précis pas encore connu, qui sera fixé à la première utilisation.

# let r = ref [];;
val r : '_weak1 list ref = {contents = []}
# r := [1];;
- : unit = ()
# r;;
- : int list ref = {contents = [1]}

Cela touche aussi les applications partielles. Dans ce cas, il suffit de rajouter l'argument explicitement pour retrouver une fonction, donc une valeur :

# let l = List.map (fun x -> x);;
val l : '_weak2 list -> '_weak2 list = <fun>
# let l2 x = List.map (fun x -> x) x;;
val l2 : 'a list -> 'a list = <fun>