(**
Langages, sémantiques et modèles d'exécution.
Thibaut Balabonski @ Université Paris-Sud, M2 FIIL.
Cours 4, 2 octobre 2017.
Types
*)
(**
λ-calcul simplement typé
------------------------
Les types apportent une classification des différentes expressions d'un
programme.
Les types manipulés sont donnés par la grammaire :
T ::= B (type de base, par exemple [int])
| T₁ ⟶ T₂ (fonction de T₁ dans T₂)
Quel est le type de [t a] ?
- il faut que [t] soit une fonction
- il faut que [a] corresponde au type attendu en entrée par [t]
t : T ⟶ U a : T
--------------------------------
t a : U
Quel est le type de [x] ?
- cela dépend d'un contexte qui définit le type de cette variable
- techniquement, on appelle ça un environnement (de typage)
On parle donc toujours de typage "dans un environnement".
On écrit les jugements de typage :
Γ ⊢ t : T
Dans l'environnement Γ, le programme t est bien typé, de type T
On peut compléter la règle d'application
Γ ⊢ t : T ⟶ U Γ ⊢ a : T
---------------------------------
Γ ⊢ t a : U
Règle pour la variable : Dernier cas : type d'une fonction λx.b
Γ(x) = T Γ, x : T ⊢ b : U
----------- -------------------
Γ ⊢ x : T Γ ⊢ λx.b : T ⟶ U
*)
(**
λ-calcul pur, types simples : vérification du bon typage.
Pour faciliter la vérification, on peut considérer que chaque abstraction
comporte une annotation de typage donnant le type du paramètre formel.
D'où la nouvelle grammaire :
t ::= x // Variable
| t t // Application
| λx:T. t // Abstraction typée
*)
module Lambda = struct
type typ =
| TypB
| TypArrow of typ * typ
type term =
| Var of string
| Abs of string * typ * term
| App of term * term
(* Ajout d'une construction dérivée : [let x=t₁ in t₂] == [(λx.t₂) t₁] *)
| Let of string * term * term
module Env = Map.Make(String)
type type_env = typ Env.t
let rec type_expression env = function
| Var x ->
Env.find x env
| Abs(x, arg_type, t) ->
let env' = Env.add x arg_type env in
let res_type = type_expression env' t in
TypArrow(arg_type, res_type)
| App(t1, t2) ->
let arg_type, res_type = match type_expression env t1 with
| TypArrow(arg_t, res_t) -> arg_t, res_t
| _ -> failwith "Type fonctionnel attendu"
in
if type_expression env t2 = arg_type
then res_type
else failwith "Application incompatible"
(* Règle dérivée du codage [let x=t₁ in t₂] == [(λx.t₂) t₁] *)
| Let(x, t1, t2) ->
let env' = Env.add x (type_expression env t1) env in
type_expression env' t2
let idB = Abs("x", TypB, Var "x")
let doubleB = Abs("f", TypArrow(TypB, TypB),
Abs("x", TypB,
App(Var "f", App(Var "f", Var "x"))))
let doubleIdB = Let("d", doubleB, App(Var "d", idB))
let ddoubleIdB = Let("d", doubleB, App(App(Var "d", Var "d"), idB))
let _ = type_expression Env.empty idB
let _ = type_expression Env.empty doubleB
let _ = type_expression Env.empty (App(doubleB, idB))
(* let _ = type_expression Env.empty (App(idB, doubleB)) *)
let _ = type_expression Env.empty doubleIdB
(* let _ = type_expression Env.empty ddoubleIdB *)
let _ = print_string "Exemples Lambda ok\n"
end
(**
Slogan de Milner :
"Well-typed programs do not go wrong"
Lien entre les types, c'est-à-dire une analyse "statique" qui s'applique
au code source du programme, et l'exécution du programme, c'est-à-dire son
comportement "dynamique".
Comment traduire cette propriété dans nos sémantiques ?
Pour la sémantique par évaluation t ⟹ v : difficile de traduire le slogan
de Milner. Un programme qui ne bloque pas peut soit donner une valeur,
soit diverger.
Pour la sémantique par réduction :
- Si un programme t est bien typé, alors soit c'est une valeur, soit on a
une étape de réduction t ⟶ t'. (Progression)
- Si un programme t est bien typé, et t ⟶ t', alors t' est bien typé.
(Subject reduction / Préservation)
Ces deux propriétés ensembles permettent d'itérer : partant d'un terme bien
typé, on va avoir une exécution qui préserve le bon typage, jusqu'à une
valeur ou divergence.
Préservation du typage pour le λ-calcul :
Si Γ ⊢ t : T et t ⟶ t',
alors Γ ⊢ t' : T
Par récurrence sur la dérivation de Γ ⊢ t : T
Cas Γ ⊢ x : T (avec Γ(x)=T)
Ce cas est impossible car il n'y a pas de réduction x ⟶ t'
Cas Γ ⊢ λx.b : T ⟶ U
Ce cas est encore impossible car λx.b est une valeur, et pas de réduction
Cas Γ ⊢ t a : U, avec Γ ⊢ t : T ⟶ U et Γ ⊢ a : T
Quelles sont les réductions possibles ?
1. t ⟶ t''
Hypothèse de récurrence : Γ ⊢ t'' : T ⟶ U
Si on considère t' = t'' a
Par la règle de typage des applications : Γ ⊢ t'' a : U
2. a ⟶ a' (avec t' = t a')
Hypothèse de récurrence : Γ ⊢ a' : T
Par la même règle : Γ ⊢ t a' : U
3. t=λx.b, a=v, et (λx.b)v ⟶ b{x←v}
Par hypothèse Γ ⊢ t=λx.b : T ⟶ U
Or une seule règle permet de dériver un type pour une fonction,
on a donc aussi Γ, x : T ⊢ b : U
On a encore l'hypothèse Γ ⊢ a=v : T
Peut-on en déduire quelque chose sur le type de b{x←v}
Le lemme de préservation du typage par substitution dit exactement
Γ ⊢ b{x←v} : U
Fin de la preuve de préservation du typage par réduction.
Lemme : préservation du typage par substitution
Si
Γ ⊢ t : T, Γ(x) = U et Γ ⊢ u : U
alors
Γ ⊢ t{x←u} : T
Preuve par récurrence sur Γ ⊢ t : T
Cas Γ ⊢ t=y : T avec Γ(y) = T
Si x != y, alors y{x←u} = y, et Γ ⊢ y{x←u} : T
Si x = y, y{x←u} = x{x←u} = u, et Γ ⊢ y{x←u} : U
Mais on a aussi : Γ(x) = T, Γ(y) = U, x = y, et donc T = U
Cas Γ ⊢ λy.b : T₁ ⟶ T₂, avec Γ, y:T₁ ⊢ b : T₂
Par α-équivalence, on fait en sorte que x!=y
Si x != y,
t{x←u} = λy.(b{x←u})
On a comme hypothèses :
- Γ, y:T₁ ⊢ b : T₂
- Γ(x) = U
On peut donc appliquer l'hypothèse de récurrence, on obtient
Γ, y:T₁ ⊢ b{x←u} : T₂
Donc par règle de typage des fonctions :
Γ ⊢ λy.(b{x←u}) : T₁ ⟶ T₂
On a donc bien Γ ⊢ (λy.b){x←u} : T₁ ⟶ T₂
Cas Γ ⊢ r a : T, avec Γ ⊢ r : T' ⟶ T et Γ ⊢ : a : T'
Objectif : Γ ⊢ (r a){x←u} : T
Hypothèses de récurrence :
- Γ ⊢ r{x←u} : T' ⟶ T
- Γ ⊢ a{x←u} : T'
On peut combiner les deux hypothèses de récurrence avec la règle de typage
pour l'application :
Γ ⊢ r{x←u} a{x←u} : T
Par définition de la substitution, r{x←u} a{x←u} = (r a){x←u}
Fin de la preuve du lemme.
Progression : immédiat pour le λ-calcul.
Donc : préservation du typage + progression
⟹ on obtient la sûreté du typage pour le λ-calcul
*)
(**
Extension avec des entiers, des paires, des opérateurs, et des
annotations de types.
Détail de l'ajout des paires : on étend le formalisme avec de nouveaux termes,
de nouvelles valeurs, de nouvelles règles de réduction et de nouveaux types.
Construire une paire : (t₁, t₂)
Projection sur la i-ème composante : πᵢ(t)
Règles de réduction :
- π₁(t₁, t₂) ⟶ t₁
- π₂(t₁, t₂) ⟶ t₂
Questions :
- Faut-il de nouvelles formes de types ?
- Quelles sont les règles de typage de ces nouvelles constructions ?
Nouvelle forme de types : T₁ * T₂
Γ ⊢ t₁:T₁ Γ ⊢ t₂:T₂
-----------------------
Γ ⊢ (t₁, t₂) : T₁ * T₂
Γ ⊢ t : T₁ * T₂
---------------
Γ ⊢ π₁(t) : T₁
Ensemble des valeurs (avant, était juste v ::= λx.b)
Nouvelle forme de valeur : (v₁, v₂)
On pourrait prouver un lemme de classification :
- Une valeur de type T₁ * T₂ est nécessairement de la forme (v₁, v₂)
- Une valeur de type T₁ ⟶ T₂ est nécessairement de la forme λx.b
Ce lemme de classification sert pour la preuve de la propriété de progression.
*)
module LambdaPair = struct
type typ =
| TypInt
| TypArrow of typ * typ
| TypPair of typ * typ
type term =
| Var of string
| Abs of string * typ * term
| App of term * term
| Const of int
| Op of string
| Pair of term * term
| Typed of term * typ
module Env = Map.Make(String)
type type_env = typ Env.t
let rec type_expression env = function
| Var x ->
Env.find x env
| Abs(x, arg_type, t) ->
let env' = Env.add x arg_type env in
let res_type = type_expression env' t in
TypArrow(arg_type, res_type)
| App(t1, t2) ->
let arg_type, res_type = match type_expression env t1 with
| TypArrow(arg_t, res_t) -> arg_t, res_t
| _ -> failwith "Type fonctionnel attendu"
in
if type_expression env t2 = arg_type
then res_type
else failwith "Application incompatible"
| Const _ ->
TypInt
| Op "+" ->
TypArrow(TypPair(TypInt, TypInt), TypInt)
| Op op ->
failwith ("Pas d'opérateur " ^ op)
| Pair(t1, t2) ->
TypPair(type_expression env t1, type_expression env t2)
| Typed(t, ty) ->
if type_expression env t = ty
then ty
else failwith "Annotation incompatible"
end
(**
Exercice 1 : ajouter un type somme.
*)
(**
Inférence de types par résolution de contraintes
------------------------------------------------
On oublie les annotations de types, et on essaye simplement de s'assurer
qu'il existe une série d'annotations rendant le programme bien typé.
Pour effectuer cette analyse, on procède en deux étapes :
- construction d'un ensemble de contraintes d'égalité entre types
- résolution des contraintes par unification
Pour exprimer dans les contraintes des types par encore connus, on ajoute des
variables de type à la syntaxe des types.
*)
module LambdaInfer = struct
type typ =
| TypVar of string
| TypArrow of typ * typ
type term =
| Var of string
| Abs of string * term
| App of term * term
(* Une contrainte est une paire de type (ty₁, ty₂) à interpréter comme
l'égalité ty₁ = ty₂ à satisfaire. *)
type type_constraint = typ * typ
module CSet = Set.Make(struct type t=type_constraint let compare=compare end)
let cset_map f cset =
CSet.fold (fun c cset -> CSet.add c cset) cset CSet.empty
(* Environnement de typage *)
module Env = Map.Make(String)
type type_env = typ Env.t
(* Fonction auxiliaire de création d'une nouvelle variable de type *)
let fresh_type_variable =
let cpt = ref 0 in
fun () -> incr cpt; Printf.sprintf "?%d" !cpt
(**
Génération de contraintes :
- Dans le cas d'une variable, pas de nouvelle contrainte (on renvoie le
type enregistré dans l'environnement).
- Dans le cas d'une abstraction on crée une nouvelle variable de type pour
le type du paramètre, et on enrichit l'environnement pour l'analyse du
corps de la fonction.
- Dans le cas d'une application on introduit une contrainte : le type
du membre gauche doit être égal à un type de fonction, dont le type
d'entrée est le type du membre droit. On crée une nouvelle variable de
type pour le type du résultat.
*)
let generate_constraints t =
(* Renvoie une paire : type de l'expression et ensemble de contraintes. *)
let rec gen (env: type_env) : term -> typ * CSet.t = function
| Var x -> Env.find x env, CSet.empty
| Abs(x, t) -> let x_type = TypVar (fresh_type_variable ()) in
let t_type, cset = gen (Env.add x x_type env) t in
TypArrow(x_type, t_type), cset
| App(t1, t2) -> let res_type = TypVar (fresh_type_variable ()) in
let t1_type, cset1 = gen env t1 in
let t2_type, cset2 = gen env t2 in
let cset =
CSet.add
(t1_type, TypArrow(t2_type, res_type))
(CSet.union cset1 cset2)
in
res_type, cset
in snd (gen Env.empty t)
(* Résolution des contraintes *)
let rec free x = function
| TypVar y -> x <> y
| TypArrow(ty1, ty2) -> free x ty1 && free x ty2
let rec type_substitution x t = function
| TypVar y as u ->
if x=y
then t
else u
| TypArrow(ty1, ty2) ->
TypArrow(type_substitution x t ty1, type_substitution x t ty2)
let resolve_constraints cset =
let constraints = ref cset in
while not (CSet.is_empty !constraints) do
let s, t = CSet.choose !constraints in
constraints := CSet.remove (s, t) !constraints;
match s, t with
| TypVar x, _ when free x t ->
constraints := cset_map (type_substitution x t) !constraints
| _, TypVar x when free x s ->
constraints := cset_map (type_substitution x s) !constraints
| TypArrow(s1, s2), TypArrow(t1, t2) ->
constraints := CSet.add (s1, t1) (CSet.add (s2, t2) !constraints)
| _ -> failwith "Contraintes insolubles"
done
let typecheck_expression t = resolve_constraints (generate_constraints t)
let idB = Abs("x", Var "x")
let doubleB = Abs("f", Abs("x", App(Var "f", App(Var "f", Var "x"))))
let autoApply = Abs("x", App(Var "x", Var "x"))
let _ = typecheck_expression idB
let _ = typecheck_expression doubleB
let _ = typecheck_expression (App(doubleB, idB))
let _ = typecheck_expression (App(idB, doubleB))
let _ = typecheck_expression (App(idB, idB))
let _ = print_string "Exemples LambdaInfer ok\n"
(* let _ = typecheck_expression autoApply *)
end
(**
Polymorphisme.
*)
(**
Lambda-calcul avec [let] polymorphes.
Version simple : on n'exprime pas explicitement le polymorphisme mais on
duplique les termes liés par [let] pour typer chaque version indépendamment.
*)
module LambdaLetPoly = struct
type typ =
| TypVar of string
| TypArrow of typ * typ
type term =
| Var of string
| Abs of string * term
| App of term * term
| Let of string * term * term
type type_constraint = typ * typ
module CSet = Set.Make(struct type t=type_constraint let compare=compare end)
let cset_map f cset =
CSet.fold (fun c cset -> CSet.add c cset) cset CSet.empty
module Env = Map.Make(String)
type type_env = typ Env.t
let fresh_type_variable =
let cpt = ref 0 in
fun () -> incr cpt; Printf.sprintf "?%d" !cpt
module VarSet = Set.Make(String)
let rec free_variables = function
| Var x ->
VarSet.singleton x
| Abs(x, b) ->
VarSet.remove x (free_variables b)
| App(t1, t2) ->
VarSet.union (free_variables t1) (free_variables t2)
| Let(x, t1, t2) ->
VarSet.union (free_variables t1) (VarSet.remove x (free_variables t2))
(* [rename x t] renvoie un nouveau nom supposé frais pour [x] et le renommage
correspondant de [t]. *)
let fresh_variable =
let cpt = ref 0 in
fun x -> incr cpt; Printf.sprintf "%s_r%i" x !cpt
let rename_variable x t =
let y = fresh_variable x in
let rec rename = function
| Var z as t ->
if x=z then Var y else t
| Abs(z, b) as t ->
if z=x then t else Abs(z, rename b)
| App(t1, t2) ->
App(rename t1, rename t2)
| Let(z, t1, t2) ->
if z=x then Let(z, rename t1, t2)
else Let(z, rename t1, rename t2)
in
y, rename t
(* [term_substitution x u t] substitue par [u] les occurrences de [x] dans [t]
en évitant les captures. *)
let term_substitution x u t =
let rec subst = function
| Var y as t ->
if x=y then u else t
| Abs(y, b) as t ->
if x=y then t
else if VarSet.mem y (free_variables u)
then let z, b' = rename_variable y b in
Abs(z, subst b')
else Abs(y, subst b)
| App(t1, t2) ->
App(subst t1, subst t2)
| Let(y, t1, t2) ->
if x=y
then Let(y, subst t1, t2)
else if VarSet.mem y (free_variables u)
then let z, t2' = rename_variable y t2 in
Let(z, subst t1, subst t2')
else Let(y, subst t1, subst t2)
in
subst t
(* Pour simuler du polymorphisme, on substitue tout terme lié par [let]
avant d'analyser son type. *)
let generate_constraints t =
(* Renvoie une paire : type de l'expression et ensemble de contraintes. *)
let rec gen (env: type_env) : term -> typ * CSet.t = function
| Var x -> Env.find x env, CSet.empty
| Abs(x, t) -> let x_type = TypVar (fresh_type_variable ()) in
let t_type, cset = gen (Env.add x x_type env) t in
TypArrow(x_type, t_type), cset
| App(t1, t2) -> let res_type = TypVar (fresh_type_variable ()) in
let t1_type, cset1 = gen env t1 in
let t2_type, cset2 = gen env t2 in
let cset =
CSet.add
(t1_type, TypArrow(t2_type, res_type))
(CSet.union cset1 cset2)
in
res_type, cset
(* Règle dérivée du même codage, plus β-réduction.
[let x=t₁ in t₂] == [(λx.t₂) t₁] ⟶β [t₂{x←t₁}] *)
| Let(x, t1, t2) ->
gen env (term_substitution x t1 t2)
in snd (gen Env.empty t)
let rec free x = function
| TypVar y -> x <> y
| TypArrow(ty1, ty2) -> free x ty1 && free x ty2
let rec type_substitution x t = function
| TypVar y as u ->
if x=y
then t
else u
| TypArrow(ty1, ty2) ->
TypArrow(type_substitution x t ty1, type_substitution x t ty2)
let resolve_constraints cset =
let constraints = ref cset in
while not (CSet.is_empty !constraints) do
let s, t = CSet.choose !constraints in
constraints := CSet.remove (s, t) !constraints;
match s, t with
| TypVar x, _ when free x t ->
constraints := cset_map (type_substitution x t) !constraints
| _, TypVar x when free x s ->
constraints := cset_map (type_substitution x s) !constraints
| TypArrow(s1, s2), TypArrow(t1, t2) ->
constraints := CSet.add (s1, t1) (CSet.add (s2, t2) !constraints)
| _ -> failwith "Contraintes insolubles"
done
let typecheck_expression t = resolve_constraints (generate_constraints t)
let idB = Abs("x", Var "x")
let doubleB = Abs("f", Abs("x", App(Var "f", App(Var "f", Var "x"))))
let doubleIdB = Let("d", doubleB, App(Var "d", idB))
let ddoubleIdB = Let("d", doubleB, App(App(Var "d", Var "d"), idB))
let autoApply = Abs("x", App(Var "x", Var "x"))
(* Pour du polymorphisme en actes ici il faut une abstraction non annotée,
ce qu'on n'a pas autorisé tant qu'il n'y a pas d'inférence. *)
let _ = typecheck_expression idB
let _ = typecheck_expression doubleB
let _ = typecheck_expression (App(doubleB, idB))
let _ = typecheck_expression (App(idB, doubleB))
let _ = typecheck_expression doubleIdB
let _ = typecheck_expression ddoubleIdB
let _ = print_string "Exemples LambdaLetPoly ok\n"
(* let _ = typecheck_expression autoApply *)
end