(**
Langages, sémantiques et modèles d'exécution.
Thibaut Balabonski @ Université Paris-Sud, M2 FIIL.
Cours 3, 25 septembre 2018.
Transformations monadiques
Ces notes reprennent des éléments du cours de Xavier Leroy.
*)
(**
Exceptions
----------
Les exceptions sont une structure de contrôle utile pour la gestion des
erreurs, mais aussi pour toute situation dans laquelle il est pertinent
d'interrompre un calcul en cours.
*)
(* Calcul du produit des éléments d'une liste des entiers. *)
let product (lst : int list) : int =
let rec prod : int list -> int = function
| [] -> 1
| hd :: tl -> hd * prod tl
in
prod lst
(* Ce calcul va parcourir toute la liste, même si un résultat de 0 est garanti
par la présence d'un 0. *)
let _ = product [ 0; 1; 2; 3; 4; 5; 6 ]
(* Version avec interruption : si la valeur 0 est rencontrée dans la liste,
interrompre le parcours et directement renvoyer le résultat 0. *)
let product (lst : int list) : int =
let rec prod : int list -> int = function
| [] -> 1
| 0 :: tl -> raise Exit
| hd :: tl -> hd * prod tl
in
try prod lst with Exit -> 0
(**
Sémantique pour les exceptions.
En reprenant le format précédent de sémantique à grands pas
e ⟹ v
il faut réfléchir à nouveau aux issues possibles du calcul.
Dans le cas du λ-calcul, un terme pouvait :
- produire une valeur comme résultat
- mener à un calcul divergent (infini)
Maintenant, on a en plus la possibilité de lever une exception, qui donne
un deuxième genre de résultat.
Résultat :
r ← v // valeur
| raise v // exception, à laquelle est aussi attachée une valeur
Règles de sémantique :
a ⟹ v
----------------------- La construction try/with renvoie la valeur
try a with x -> b ⟹ v calculée par son expression principale...
a ⟹ raise v' b{x←v'} ⟹ r ... sauf si cette expression produit une
--------------------------------- exception, auquel cas on évalue le code
try a with x -> b ⟹ r de rattrapage.
On a également des règles pour la propagation des exceptions
a ⟹ raise v Si le membre gauche d'une application produit une exception,
--------------- alors pas besoin d'évaluer le membre droit.
a b ⟹ raise v
a ⟹ v' b ⟹ raise v
--------------------------
a b ⟹ raise v
*)
(**
Transformation en style par passage d'exceptions.
Cette sémantique peut être associée à une transformation de programmes
partant d'un langage fonctionnel avec exceptions et allant vers un langage
fonctionnel avec simplement du filtrage.
On donne un type union ['a res] pour les résultats :
- V(v) pour les valeurs de type ['a]
- E(v) pour les exceptions
*)
type 'a res =
| V of 'a
| E of 'a
(**
Règles de transformation.
Base fonctionnelle
⟦N⟧ = V(N)
⟦x⟧ = V(x)
⟦λx.a⟧ = V(λx.⟦a⟧)
⟦let x=a in b⟧ = match ⟦a⟧ with
| E(x) -> E(x)
| V(x) -> ⟦b⟧
⟦a₁ a₂⟧ = match ⟦a₁⟧ with
| E(e₁) -> E(e₁)
| V(v₁) -> match ⟦a₂⟧ with
| E(e₂) -> E(e₂)
| V(v₂) -> v₁ v₂
Règles des constructions spécifiques aux exceptions
⟦raise a⟧ = match ⟦a⟧ with
| E(e) -> E(e)
| V(v) -> E(v)
⟦try a with x -> b⟧ = match ⟦a⟧ with
| E(x) -> ⟦b⟧
| V(v) -> V(v)
Traduction des types
⟦τ⟧ = τ pour les types de base
⟦τ₁ ⟶ τ₂⟧ = ⟦τ₁⟧ ⟶ ⟦τ₂⟧ res
Si on a un jugement de typage
Γ ⊢ a : τ
alors on obtient après traduction
⟦Γ⟧ ⊢ ⟦a⟧ : ⟦τ⟧ res
*)
let product (lst: int list) : int =
let rec prod : int list -> int res = function
| [] -> V(1)
| 0::tl ->
begin match E(0) with
| E(e) -> E(e)
| V(v) -> E(v)
end
| hd::tl ->
begin match prod tl with
| E(e) -> E(e)
| V(v) -> V(hd * v)
end
in
match prod lst with
| E(e) -> 0
| V(v) -> v
(**
Réductions administratives.
Une application directe de la traduction est susceptible de former des
match/with pour lesquels la forme V ou E des arguments est connue.
On peut opérer les simplifications suivantes :
match E(v) with E(x) -> b | V(x) -> c ⟶ b{x←v}
match V(v) with E(x) -> v | V(x) -> c ⟶ c{x←v}
*)
let product (lst: int list) : int =
let rec prod : int list -> int res = function
| [] -> V(1)
| 0::tl -> E(0)
| hd::tl ->
begin match prod tl with
| E(e) -> E(e)
| V(v) -> V(hd * v)
end
in
match prod lst with
| E(e) -> 0
| V(v) -> v
(**
Correction de la transformation (on note [N] = N et [λx.a] = λx.⟦a⟧)
1/ Si a ⟹ v, alors ⟦a⟧ ⟹ V([v])
2/ Si a ⟹ raise v, alors ⟦a⟧ ⟹ E([v])
La divergence est également préservée.
Preuve par induction simultanée, avec le lemme de substitution
⟦a{x←v}⟧ = ⟦a⟧{x←[v]}
*)
(**
État
----
Le trait caractéristique de la programmation impérative est la capacité de
modifier la valeur d'une variable ou le contenu d'une structure de données
après sa définition. On appelle *état* la configuration à un point donné.
Version minimale : références, c'est-à-dire cellules d'indirection
(ou tableaux à un élément pouvant être modifiés en place).
ref a : création d'une nouvelle référence avec la valeur initiale [a]
!a : valeur contenue dans la référence [a]
a := b : modification du contenu de [a] avec la valeur de [b]
*)
let mk_pseudo_random_generator seed =
let state = ref seed in
fun n ->
let _ = state := (!state * 1023 + 19) mod 97 in
!state mod n
(**
Sémantique des références
Les sémantiques à base de substitutions ne reflètent pas correctement le
partage impliqué par les références :
let r = ref 1 in r := 2; !r
n'est pas équivalent à
(ref 1) := 2; !(ref 1)
Il faut à la place expliciter l'indirection représentée par une référence :
- la valeur d'une expression [ref a] est une *adresse* l
- un environnement global, la *mémoire*, associe aux adresses des valeurs
On a donc un nouveau type de valeurs : les adresses, et l'évaluation
concerne des paires (terme, mémoire).
Réduction à petits pas (ou sémantique à réductions).
Une étape de réduction est formée par l'application de l'une des règles
suivantes dans un contexte quelconque :
(λx.a) v / s ⟶ a{x←v} / s
ref v / s ⟶ l / s[l←v] avec l ∉ Dom(s)
!l / s ⟶ s(l) / s
l := v / s ⟶ () / s[l←v]
Remarque : l'opération d'affectation implique l'adjonction du type [unit],
dont l'unique valeur est [()].
*)
(**
Transformation en style par passage d'état.
Cette sémantique peut être associée à une transformation de programmes
partant d'un langage fonctionnel avec des références impératives vers un
langage fonctionnel pur.
Chaque expression est transformée en une fonction prenant en paramètre une
représentation de l'état courant et renvoyant une paire formée par la
valeur résultat et l'état modifié.
*)
type value =
| I of int
| L of int
| Unit
type store = int * (int * value) list
type result = value * store
(**
Règles de transformation.
Base fonctionnelle
⟦N⟧ = λs.(N, s)
⟦x⟧ = λs.(x, s)
⟦λx.a⟧ = λs.(λx.⟦a⟧, s)
⟦let x=a in b⟧ = λs.let (x, s') = ⟦a⟧ s in ⟦b⟧ s'
⟦a₁ a₂⟧ = λs.let (v₁, s₁) = ⟦a₁⟧ s in
let (v₂, s₂) = ⟦a₂⟧ s₁ in
v₁ v₂ s₂
Règles des constructions spécifiques aux références.
On se donne trois opérations réalisant concrètement la mémoire :
- read l s : renvoie la valeur associée à l'adresse [l] dans [s]
- write l v s : renvoie l'état modifié en associant [v] à l'adresse [l]
- alloc v s : renvoie (l, s') où [s'] est un nouvel état dans lequel la
*nouvelle* adresse est associée à [v]
⟦ref a⟧ = λs.let (v, s') = ⟦a⟧ s in alloc v s'
⟦!a⟧ = λs.let (v, s') = ⟦a⟧ s in (read v s', s')
⟦a₁ := a₂⟧ = λs.let (v₁, s₁) = ⟦a₁⟧ s in
let (v₂, s₂) = ⟦a₂⟧ s in
(ε, write v₁ v₂ s₂)
Traduction des types
⟦τ⟧ = τ
⟦τ₁ ⟶ τ₂⟧ = ⟦τ₁⟧ ⟶ store ⟶ ⟦τ₂⟧ x store
Si on a un jugement de typage
Γ ⊢ a : τ
alors on obtient après traduction
⟦Γ⟧ ⊢ ⟦a⟧ : store ⟶ ⟦τ⟧ x store
*)
(**
Réductions administratives.
(λs'.b)s ⟶ b{s←s'} si [s] variable
let (x, s') = (a, s) in b ⟶ let x=a in b{s'←s}
let x=v in b ⟶ b{x←v}
let x=y in b ⟶ b{x←y}
*)
(**
Monades
-------
Les transformations que nous avons vues présentent une structure commune.
** Pour les valeurs
Exceptions État Continuations
⟦N⟧ = V(N) ⟦N⟧ = λs.(N,s) ⟦N⟧ = λk.k N
⟦x⟧ = V(x) ⟦x⟧ = λs.(x,s) ⟦x⟧ = λk.k x
⟦λx.a⟧ = V(λx.⟦a⟧) ⟦λx.a⟧ = λs.(λx.⟦a⟧,s) ⟦λx.a⟧ = λk.k (λx.⟦a⟧)
Dans tous les cas on renvoie la valeur N, x ou λx.⟦a⟧,
empaquetée d'une certaine manière.
** Pour les liaisons
⟦let x=a in b⟧ = match ⟦a⟧ with E(x) -> E(x) | V(x) -> ⟦b⟧
⟦let x=a in b⟧ = λs.let (x,s') = ⟦a⟧ s in ⟦b⟧ s'
⟦let x=a in b⟧ = λk.⟦a⟧ (λx.⟦b⟧ k)
Dans tous les cas on récupère la valeur de ⟦a⟧, on la lie à x et on
poursuit avec l'évaluation de ⟦b⟧.
** Pour les applications
⟦a₁ a₂⟧ = match ⟦a₁⟧ with E(e₁) -> E(e₁) | V(v₁) ->
match ⟦a₂⟧ with E(e₂) -> E(e₂) | V(v₂) ->
v₁ v₂
⟦a₁ a₂⟧ = λs.let (v₁, s₁) = ⟦a₁⟧ s in
let (v₂, s₂) = ⟦a₂⟧ s₁ in
v₁ v₂ s₂
⟦a₁ a₂⟧ = λk.⟦a₁⟧ (λv₁.⟦a₂⟧ (λv₂.v₁ v₂ k))
On lie ⟦a₁⟧ à une variable v₁, puis on lie ⟦a₂⟧ à une variable ⟦v₂⟧,
et on effectue l'application v₁ v₂.
*)
(**
Généralisation
Une monade est définie par un type paramétré
α mon
représentant des calculs produisant une valeur de type α,
et par trois opérations ret, bind et run ayant les profils suivants :
ret : ∀α. α ⟶ α mon
[ret a] encapsule une expression [a : τ] dans un calcul trivial de
type [τ mon] produisant immédiatement la valeur de [a].
bind : ∀αβ. α mon ⟶ (α ⟶ β mon) ⟶ β mon
[bind a (λx.b)] effectue le calcul [a : α mon], lie sa valeur à [x : α]
puis effectue le calcul [b : β mon].
run : ∀α. α mon ⟶ α
[run a] exécute le program monadique [a] et renvoie sa valeur.
Les opérations ret et bind doivent vérifier des équations de la forme
bind (ret a) f == f a
bind a (λx.ret x) == a
bind (bind a (λx.b)) (λy.c) == bind a (λx.bind b (λy.c))
La relation == signifie intuitivement que les termes se comportent de
la même façon. Il faudra préciser la définition.
*)
(**
Exemples.
** La monade d'exception (ou monade d'erreur)
type α mon = V of α | E of exn
ret a = V(a)
bind m f = match m with E(x) -> E(x) | V(x) -> f x
run m = match m with V(x) -> x
raise x = E(x)
trywith m f = match m with E(x) -> f x | V(x) -> V(x)
Ici, bind encode la propagation d'exceptions dans des expressions composées.
** La monade d'état
type α mon = state ⟶ α x state
ret a = λs.(a,s)
bind m f = λs.let (x,s') = m s in f x s'
run m = let (x,s) = m ε in x
ref x = λs.alloc x s
!r = λs.(read r s,s)
r := x = λs.((),write r x s)
Ici, bind encode le passage de l'état d'une composante à l'autre d'une
expression composée.
** La monade de continuation
type α mon = (α ⟶ answer) ⟶ answer
ret a = λk.k a
bind m f = λk.m (λv.f v k)
run m = m (λx.x)
callcc f = λk.f k k
throw x y = λk.x y
*)
(**
Transformation monadique générale
⟦N⟧ = ret N
⟦x⟧ = ret x
⟦λx.a⟧ = ret (λx.⟦a⟧)
⟦let x=a in b⟧ = bind ⟦a⟧ (λx.⟦b⟧)
⟦a₁ a₂⟧ = bind ⟦a₁⟧ (λv₁.bind ⟦a₂⟧ (λv₂.v₁ v₂))
Transformation sur les types
⟦τ⟧ = τ pour les types de base
⟦τ₁ ⟶ τ₂⟧ = ⟦τ₁⟧ ⟶ ⟦τ₂⟧ mon
Et si Γ ⊢ a : τ
alors ⟦Γ⟧ ⊢ ⟦a⟧ : ⟦τ⟧ mon
On peut étendre cette transformation à d'autres constructions comme les
opérateurs binaires :
⟦a₁ op a₂⟧ = bind ⟦a⟧ (λv₁.bind ⟦b⟧ (λv₂.ret (v₁ op v₂)))
La plupart des constructions particulières des exemples précédents peuvent
être reconstruites avec la règle d'application.
Par exemple :
⟦raise a⟧ = bind (ret raise) (λr.bind ⟦a⟧ (λv.r v))
⟶ bind ⟦a⟧ (λv.raise v)
Le cas qui reste particulier est celui de try/with, qui demande une règle
spécifique
⟦try a with x -> b⟧ = trywith ⟦a⟧ (λx.⟦b⟧)
*)
(**
Propriétés de la transformation.
Transformation monadique [v] d'une valeur
[N] = N
[λx.a] = λx.⟦a⟧
Lemme de traduction des valeurs
Pour toute valeur v,
⟦v⟧ = ret [v]
De plus [v] est une valeur
Lemme de substitution
Pour toute valeur v,
⟦a{x←v}⟧ = ⟦a⟧{x←[v]}
À propos des réductions
Si a se réduit, est-ce que ⟦a⟧ aussi ?
- pour la monade d'exception, oui
- pour les monades d'état et de continuation, non
Dans ces deux derniers cas il faut mettre le terme dans un contexte
approprié :
- ⟦a⟧ s avec s une mémoire pour la monade d'état
- ⟦a⟧ k avec k une continuation pour la monade de continuation
À la place, on raisonne sur une relation d'équivalence == vérifiant les
propriétés suivantes
1/ (λx.a) v == a{x←v} (β-réduction)
2/ bind (ret v) (λx.b) == b{x←v} (première loi monadique)
3/ Si a == a' alors bind a (λx.b) == bind a' (λx.b)
(compatibilité contexte)
4/ Si a == ret v alors run a ⟹ v
Correction de la transformation monadique
Si
a ⟹ v
alors
⟦a⟧ == ret [v]
*)