Postscript réduit compressé(original compressé)
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épendemment de l'orginie de l'erreur, on peut observer la manisfestation de l'erreur.
    · L'évaluation est bloquée (produit une erreur)
    · Le résultat retourne une valeur, mais celle-ci est incorrecte.
    · Le programme ne termine pas.
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'évalue 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 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 contiendrait que et tous les programmes corrects et serait 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), modulaires des expressions qui permet d'en déduire la forme des valeurs qui peut ê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,
    · Tous les entiers sont du type int,
    · Toutes les chaînes sont du type string,

Les booléens sont du type bool,
    · Les fonctions sont d'un type fonctionnel t ® t. Toutefois, il existe plusieurs types fonctionnles, par exemple int ® int (la fonction successeur) string ® string ® string (la fonction concat), int ® string (la conversion d'un entier en une chaîne), etc.
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éside 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ésentent 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 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 simplifié 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 -> bool où libre 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 variables de programmes vers les types. Concrètement,
  A ::=     Envirommenent de typage
    Ø   Environnement vide
    x : t, A   Déclaration du type d'une variable
On étend la notion de variables (de type) libres aux contextes.
Exercice 5   Le type des environnements de typage est 

type tenv = (var * 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érver

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 minimal à imposé 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
où 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 envoit
  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 -> subst où restrict_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 var
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, [ ]

  | Var 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", Var "x"), App (Var "f", Var "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 une version impérative de l'algorithme d'unification et d'inférence, ce qui simplifie nettement les algorithmes et les rend plus efficaces.

Généralisation

On étend les types avec des schémas de types de " (a) t et on redéfinit les environnements de typage pour autoriser des schémas de types.
  A ::=     Envirommenent 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, ... an)  t
A |- x : t [a1 ¬ t1, ... an ¬ tn]




This document was translated from LATEX by HEVEA and HACHA.