Ocaml
Typage des programmes
Cours Exercices
Typage
  1. Erreurs d'évaluation
  2. Typage
  3. Polymorphisme
  1. Évaluation bloquée
  2. Indécidabilité
  3. Variables libres (1, 2, 3)
  4. Substitutions (1, 2)
  5. Composition de substitutions
  6. Inférence, primitives

Erreurs d'évaluation

L'exécution d'un programme peut ne pas produire le résultat attendu par le programmeur. Hormis une erreur d'implémentation, c'est dans tous les cas une erreur du programmeur. On peut classe les erreurs en différentes catégories.
  1. Une erreur bête, une typographie, une étourderie, etc.
  2. une erreur de raisonnement, d'algorithmique (le programmeur a fait une fautre dans la conception de son programme).
  3. une erreur sémantique: le programmeur peut avoir mal compris la sémantique d'une construction du langage.
Le classement ci-dessus est par fréquence (par exemple, le troisième type d'erreur est extrêmement rare, sauf chez les débutant...)

Indépendamment de l'origine de l'erreur, on peut observer la manisfestation de l'erreur.

En fait, on voudrait éliminer le premier cas, de telle façon que la sémantique soit bien définie pour tous les programmes.

Exercice 1   Donner deux exemples où l'évaluation est bloquée dans l'évaluation du noyau de ML.
Réponse

Pour cela il faut restreindre l'ensemble des programmes à un sous-ensemble des programmes qui s'évaluent correctement.

Cependant cet ensemble n'est pas décidable: on ne peut pas écrire un algorithme qui caractérise les programmes qui s'évaluent correctement.

Exercice 2   Montrer que si on pouvait décider des programmes qui s'exécutent correctement, on pourrait décider de l'arrêt des programmes.
Réponse



On cherche donc une approximation par défaut et décidable de l'ensemble des programmes corrects.

Évidemment il n'existe pas de meilleure approximation, i.e. de plus grand sous-ensemble décidable des programmes corrects. Sinon, cet ensemble ne contiendrait que les programmes corrects et les contiendrait rous. Cet ensemble serait donc décidable.

Une façon de définir un tel sous-ensemble est d'utiliser le typage.

Typage

Le typage est une appoximation statique (décidable) et modulaires des expressions. Il  permet de déduire la forme des valeurs (des programmes) qui peuvent être le résultat de leur évaluation.

Typiquement, on identifie toutes les valeurs de la même forme en leur donnant le même type. Par exemple,

Plus précisément, le type d'une fonction t ® t' décrit le type t de son argument et le type t' du résultat de l'application de la fonction à une valeur du type t.

La clé et la difficulté résident dans le types des fonctions et de l'application. En effet, c'est là que se passe le calcul, et c'est donc là qu'il faut ne pas perdre d'information dans l'approximation du calcul.

Un type peut aussi être une variable de type, ce qui signifie que le type est quelconque. Mais attention deux occurrences de la même variable représenteront nécessairement le même type.

Par exemple, l'identité fun  x ® x est une fonction qui retourne son argument. Elle prend une valeur de type t et retourne une valeur du même type t. Elle est donc de type t ® t pour tout type t et on peut donc dire qu'elle est de type a ® a.

Lorsqu'une fonction est d'un type polymorphe, par exemple a ® a, on peut en déduire immédiatement d'autres types, en remplaçant simultanément toutes les occurrences d'une variable par un même type t.

Aussi l'identité a les types int ® int, string ® string, (b ® b) ® (b ® b), mais elle n'a pas le type b ® g.

Les types de ML

  t ::=     Valeurs
    c   Constantes de type
    a   Variable de type
    t ® t   Type flèche
  c ::= int, string, ...
Les constantes de types sont int, string, ..., mais on se limitera pour simplifier au seul type int.

En OCaml, la solution la plus natuelle est:

type tvar = int
type texp =
Tint | Tvar of tvar
| Tarrow of texp * texp;;
(Voir pour une autre solution)

On définit l'ensemble vl (t) des variables de types de t de façon naturelle.

Exercice 3   Écrire une fonction libre_texpr : texpr -> tvar list qui une liste contenant les variables (de type) libres de son argument (éventuellement avec des doublons).
Réponse


Exercice 4   Écrire une fonction libre : tvar -> texp -> boollibre v t retourne true si la variable v apparaît dans le type t (i.e. si vÎ vl (t) et false sinon.
Réponse



Règles de typage

La relation de typage A |- a : t exprime que dans l'environnement de typage A le programme a a le type t.

Un environnement de typage est une fonction partielle des identificateurs de programmes vers les types. Concrètement,
  A ::=     Environnenent de typage
    Ø   Environnement vide
    x : t, A   Déclaration du type d'un identificateur
On étend la notion de variables (de type) libres aux contextes.

Exercice 5   Le type des environnements de typage est

type tenv = (ident * texp) list;;
Définir une fonction libre_tenv : tenv -> tvar list et qui retourne les variables libres d'un environnement de typage.
Réponse



La relation de typage est définie par des règles d'inférence.

Const
A |- n : int
      
Var
x Î dom (A)
A |- x : A(x)

Fun
A, x : t1 |- a : t2
A |- fun  x ® a : t1 ® t2
      
App
A |- a1 : t2 ® t1        A |- a2 : t2
A |- a1 a2 : t1

Let
A |- a1 : t1        A, x : t1 |- a2 : t2
A |- let  x = a1  in  a2 : t2


Preuve de typage

Les règles précédentes, permettent de prouver qu'un programme a un type dans un environnement donné. Pour cela, on présente un dérivation de typage. Par exemple,

Let
Fun
Var
y : int|-y : int
A|-fun  y ® y : int®int
  
App
Var
f : int®int|-f : int
  
Const
f : int®int|-1 : int
f : int®int|-f 1 : int
A|-let  f = fun  y ® y  in  f 1


Mais, il existe plusieurs typage possibles pour un même programme. Par exemple, on peut dériver


x : int |- x : int
Ø |- fun  x ® x : int ® int
      

x : a |- x : a
Ø |- fun  x ® x : a ® a


Substitution

Parmi les deux typages précédents, l'un peut se déduire de l'autre par remplacement de la variable a par le type int.

On appelle substitution d'un type a par un type t0 une fonction des type dans les types qui remplace dans un type t toutes les occurences de a dans t par t0.

On généralise à la substitution simultanée d'un ensemble de types.

Exercice 6   En ocaml, on peut représenter une substitution par une liste de paires:

type subst = (tvar * texp) list;;
Écrire une fonction subst_texp : subst -> texp -> texp qui prend une substitution s et un type t et retourne le résultat de l'application de la substitution s au type t.
Réponse


Exercice 7   Généraliser la substitution en une fonction sur les environnements de typage: subst_tenv : subst -> tenv -> tenv.
Réponse



Types principaux

Parmi tous les typages possibles d'un programme a, il en existe un dit principal A |- a : t. Cela signifie que tout autre typage A' |- a : t' du programme a peut se déduire du précédent par instantiation (substitution de ses variables de type par des types).

Inversement, si A |- a : t, alors q (A |- a : t) i.e. q (A) |- a : q(t)).

Cela permet de remplacer la relation de typage par une fonction qui étant donné un environement de typage A et un programme a retourne le type principal t et une substitution q tels que q(A) |- a : t soit un typage principal de a.

Ce calcul a besoin de deviner les contraintes minimales à imposer sur les variables pour rendre certains types égaux: il utilise un mécanisme d'unification.

Pour l'instant on suppose que l'on a à notre disposition une fonction

unif : texp -> texp -> subst

unify t1 t2 calcule la plus petite substitution s qui égalise t1 et t2.

Unification

On se donne une liste l de paires types et on cherche une substitution s qui rende tous les éléments de u égaux.

Par exemple, si est réduit à la paire (a ® int =? int ® a') alors la substitution (a |® int, a' |® int) est une solution.

S'il existe une solution à un problème d'unification, alors il existe une solution principale.

L'unification utilise la composition de substitutions: q2 ° q1 est la composition au sens mathématique, qui à x associe q2 (q1 (x)).

Elle est définie comme suit:
  1. si x Î dom (q1), alors (q2 ° q1) (x) = q2 (q1 (x))
  2. si x Î dom  (q2) \ dom  (q1), alors (q2 ° q1) (x) = q2(x)
  3. sinon, (q2 ° q1) (x) = x

Exercice 8   Écrire successivement, les fonctions:
    a) domain : subst -> tvar list qui retourne le domain d'une substitution.
    b) restrict_out : subst -> tvar list -> substrestrict_out s l retourne la restriction de s aux valeurs en dehors de l.
    c) compose : subst -> subst -> subst qui retourne la composition de deux substitutions.

On peut maintenant implémenter les fonctions

unify : texp -> texp -> subst
unify_list : (texp * texp) list -> subst.

récursivement.

exception Unify of texp * texp;;
let rec unify t1 t2 =
match t1, t2 with | Tvar x, Tvar y when x = y -> []
| Tvar x, t ->
if libre x t then raise (Unify (t1, t2)) else [ x, t ]
| t, Tvar x ->
if libre x t then raise (Unify (t1, t2)) else [ x, t ]
| Tint, Tint -> [ ]
| Tarrow (t11, t12), Tarrow (t21, t22) ->
unify_list [ t11, t21; t12, t22 ]
| t1, t2 -> raise (Unify (t1,t2))

and unify_list l =
match l with [] -> [] | (t1,t2)::l -> let s1 = unify_list l in
let s2 = unify (subst_texp s1 t1) (subst_texp s1 t2) in compose s2 s1 ;;

unify (Tarrow (Tint, Tvar 1)) (Tarrow (Tint, Tvar 2));;
# - : (tvar * texp) list = [1, Tvar 2]


Algorithme d'inférence

L'algorithme d'inférence de types s'implante en inférant toujours le type le plus général.

La fonction infer : tenv -> texp -> (texp * sustititution) retourne le type principal et la substition minimal à appliquer à l'environnement pour que le programme soit typable.

Il faut alors reporter cette substitution à toutes les autres prémisses de la dérivation.

infer-prim.ml
exception Libre of ident
let tvar = let last = ref 0 in fun () -> incr last; Tvar !last;;
let find_type_var x env =
try List.assoc x env with Not_found -> raise (Libre x)

let rec infer env a =
match a with
| Const n -> Tint, [ ]

| Ident x -> find_type_var x env, [ ]

| App (a1, a2) ->
let t1, s1 = infer env a1 in let t2, s2 = infer (subst_tenv s1 env) a2 in let t3 = tvar() in let s3 = unif (subst_texp s2 t1) (Tarrow (t2, t3)) in subst_texp s3 t3, compose s3 (compose s2 s1) | Fonction (x, a) ->
let t0 = tvar() in let t1, s1 = infer ((x, t0)::env) a in Tarrow (subst_texp s1 t0, t1), s1

| Liaison (x, a1, a2) ->
let t1, s1 = infer env a1 in let t2, s2 = infer ((x, t1):: subst_tenv s1 env) a2 in t2, compose s2 s1 | Prim (f, al) -> failwith "Laissé en exercice ..." ;;

let a = Liaison ("f", Fonction ("x", Ident "x"), App (Ident "f", Ident "f"))
in infer [] a;;
# - : texp * subst = Tint, [4, Tint; 3, Tint]

Exercice 9   Implémenter le cas des primitive dans l'algorithme d'inférence.
Réponse
Voir aussi l'algorithme complet.



Versions impératives

En pratique, on utilise des versions impératives des algorithmes d'unification et d'inférence, ce qui simplifie nettement les algorithmes et les rend beaucoup plus efficaces.

Généralisation

On étend les types avec des schémas de types de " (at et on redéfinit les environnements de typage pour autoriser des schémas de types.
  A ::=     Environnenent de typage
    Ø   Environnement vide
    x : t, A   Liaison de type monomorphe
    x : s, A   Liaison de type polymorphe
On modifie la règles Let et on ajoute une nouvelle forme de la règle Var:

Let
A |- a1 : t1        A, x : " (vl (t1) \ vl(A))  t1 |- a2 : t2
A |- let  x = a1  in  a2 : t2

Var
x : " (a1, ... ant
A |- x : t [a1 ¬ t1, ... an ¬ tn]





This document was translated from LATEX by HEVEA and HACHA.