Le modèle à enregistrement.
Postscript, PDF Didier Rémy Polytechnique, INRIA
Cours (super, frames) [man]
[doc] [type-index] Exercices
  1. Modélisation du calcul
  2. Calculs d'objets
  3. Sémantique
  4. Codage avec enregistrements
  5. Typage et sous-typage
  6. Prototypes
  7. Encapsulation
  1. Réduction (*)
  2. Évaluateur du calcul d'objets (**)
  3. Enregistrements extensibles (**)
  4. Objets avec des enregistrements (**)



Prélude

Le but de ce cours est de mieux comprendre ce que sont les objets:
    ·Quelle est l'essence du mécanisme de la programmation avec objets?
    ·Comment peut-on l'étudier formellement?
Pour cela, nous nous placerons un langage dépouillé de toutes les constructions non essentielles appelé calcul.

Nous nous étudierons, succinctement:
    ·Le lambda-calcul comme modèle de la programmation fonctionnelle.
    ·Un calcul d'objet.
    ·Le codage des objets dans un lambda-calcul avec enregistrements.
    ·Les problèmes de typage.
    ·L'encapsulation.


Modélisation du calcul

Les calculs sont des simplifications des langages de programmation pour permettre leur étude formelle. Ils ne retiennent que les constructions essentielles (ce qui peut dépendre du contexte d'étude) et font abstraction des détails et des constructions dérivées ou dérivables. Ainsi, les constructions d'un calcul sont en petit nombre et aussi orthogonales (indépendantes) que possible.

En contrepartie, un calcul ne permet en général d'écrire que de petits exemples: pour passer d'un calcul à un langage de programmation, on ajoute du sucre syntaxique et des constructions dérivées permettant d'abréger certaines écritures ou combinaisons fréquentes

Le lambda calcul

C'est le modèle des langages fonctionnels: il ne retient que les opérations d'abstraction et d'application:
e ::=   x      Variable (ou constante)
|   c      Constante (ou primitive)
|   fun  (xe      Fonction
|   e1 e2      Application

On peut bien sûr étendre le lambda-calcul avec quelques types primitifs (entiers, caractères, chaînes, etc.), des types construits (tuples, enregistrements), etc.

Réduction

On définit la sémantique opérationnelle du calcul par réécriture des programmes sur eux-mêmes (c'est l'approche la plus simple).

On identifie un sous-ensemble remarquable des programmes complètement évalués, appelés valeurs. Dans le lambda-calcul les valeurs notées par la lettre v sont les fonctions fun  (xe et les constantes c.

Une réduction élémentaire est une réduction en tête, appelé radical opérée à un emplacement autorisé appelé contexte d'évaluation.

Réductions en tête (appel par valeur)

Une réduction élémentaire en tête est:
    ·La b-réduction,
(fun  (xe) v ® e {x ¬ v}
L'expression v {x ¬ e} désigne l'expression v dans laquelle toute occurrence de la variable x est remplacée par v
    ·Une d-réduction est une réduction de la forme
c1 c2 ® c3
pour certains triplets (c1, c2, c3) Î d Ici c1 doit être une primitive, c2 un tuple de constantes et c3 des constantes. Par exemple l'opération successeur est définie en ajoutant l'ensemble des paires (succ, n, n +1)n Î IN dans d.

(On peut facilement généraliser à des opérations binaires.)


Contextes d'évaluation (appel par valeur)

Les emplacements où la réduction est autorisée sont décrits par des contextes d'évaluation, ie. des programmes avec un trou noté {}, définis par la grammaire:
E ::=   {}      Position où se passe la réduction
|   E e      Évaluation à gauche en premier, puis
|   v E      Évaluation à droite si
           la partie gauche est une valeur
En appel par valeur, on ne réduit jamais sous une abstraction; l'argument doit être réduit en une valeur avant de le passer à la fonction.

Ici, on a fixé l'ordre d'évaluation de gauche à droite, ce qui rend la réduction déterministe a fortiori (il n'y a qu'une seule chaîne de réécriture possible).

Évaluation

Une évaluation est une chaîne de réductions élémentaires:
e0 ® e1 ® ... en
Lorsque en est irréductible, on ne peut plus étendre la chaîne.

Exemple
(fun  (x)  x) (fun  (y)  y)
((fun  (zz) 3) ®
(x {x ¬ fun  (yy}) ((fun  (zz) 3) º
(fun  (yy)
((fun  (z)  z) 3)
®
(fun  (yy) (z {z ¬ 3}) º
(fun  (y)  y) 3
®
(y {y ¬ 3}) º
3

Exercise 1   Réduire le terme (fun  (z)  fun  (t)  fun  (f)  (z t) f) (fun  (x)  fun  (yx) 1 2.
Answer
Par quel terme peut-on remplacer (fun  (x)  fun  (yx) pour que le résultat final soit 2? Commenter.
Answer
Exercise 2   Donner un exemple de programme erroné (qui ne se réduit pas sans pour autant être une valeur).
Answer
Donner un exemple de programme qui boucle (qui se réduit indéfiniment).
Answer

Déterminisme

En général, il existe plusieurs chaînes de réduction possibles.

Une bonne propriété du calcul est son caractère déterministe qui dit que si une chaîne de réduction issue de e0 termine sur une expression irréductible en, alors toutes les chaînes possibles issues de e0 terminent également (en un nombre fini d'étapes), sur la même expression e0.

Ci-dessus, le caractère déterministe est assuré a fortiori par la forme des contextes d'évaluation: il n'y a jamais qu'un seule façon d'étendre une chaîne de réduction.

Terminaison et erreurs

En pratique, on souhaite souvent qu'une réduction se termine sur une valeur v (une valeur est toujours choisie irréductible). Ce qui n'est bien sûr pas garanti.

Non terminaison

Une évaluation peut boucler, ie. elle peut être étendue indéfiniment. (Si le calcul est complet, ie. s'il permet d'écrire tous les algorithmes possibles, alors la terminaison de l'évaluation est indécidable.)

Erreurs

Une évaluation peut aussi produire une erreur, ce qui est modélisé par une réduction qui termine sur une expression irréductible qui n'est pas une valeur. Par exemple, (fun  (xx) 2 (fun  (yy) produit une erreur: 2 (fun  (yy).

Pour en savoir plus

Le lambda-calcul est au coeur de la formalisation de la plupart des langages de programmation. Ses propriétés formelles ont été étudiés très en détail.

Il peut être muni de différentes stratégies d'évaluation (appel par nom, évaluation paresseuses) modélisant l'évaluation dans différents langages, et d'une évaluation dite forte permettant de réduire sous les abstractions modélisant par exemple les optimisations à la compilation.

Pour en savoir plus, voir
    ·Les cours de compilation en Majeure 2
    ·Le D.E.A. Programmation: Sémantique, Preuves et Langages


Calculs d'objets

Le lambda-calcul ne rend pas bien compte de la notion d'objet, en particulier des appels récursifs et de la liaison tardive.

C'est pour pouvoir étudier directement les objets que des calculs dédiés ont été introduits. Seules les constructions essentielles des langages à objets sont retenues.

Par exemple, les variables d'instance ne seront pas modélisées (elles peuvent s'écrire comme des méthodes qui n'utilisent pas self). Un calcul simplifié va aussi ignorer les champs mutables, du moins dans un premier temps. Ceux-ci peuvent ensuite être facilement réintroduits dans un calcul étendu ou dans un vrai langage.

L'abstraction et l'application ne sont pas des constructions primitives, parce qu'elles seront codables par des objets.

Un calcul d'objets (non typé)

Ce calcul est dû à Abadi-Cardelli.

Un objet est un petit enregistrement de méthodes pouvant s'appeler récursivement.
e ::=   x      Variable
|   á li = V (xiei ñi =1n      Objet
|   e.l      Envoi de message
|   e.l Ü V (xe'      Modification/ajout d'une méthode
Une méthode V (xe lie la variable x à self. Ici, chaque méthode peut utiliser un nom différent pour self. La construction p.l Ü V (xe remplace (ou ajoute) la méthode l dans p avec la définition V (xe.

N.B.: on considère les objets modulo commutation des champs.

Exemple (dans le calcul avec fonctions)

Un point (approche fonctionnel):
p =def á x = 1,
  getx = V (z) . z.x,
  setx = V (z)  fun  (y)  (z.x Ü y) ñ
Un point qui bouge (liaison tardive):
q =def( p.
  bouge Ü V (z)  (z.setx (z.getx + 1)) )
Le point qui bouge s'évalue (voir les règles ci-dessous) en
q ® á x = 1,
  getx = V (z) . z.x,
  setx = V (z)  fun  (y)  (z.x Ü y)
  bouge = V (z)  (z.setx (z.getx + 1)) ñ
L'expression p.bouge s'évalue en le nouvel objet:
q ® á x = 2,
  getx = V (z) . z.x,
  setx = V (z)  fun  (y)  (z.x Ü y)
  bouge = V (z)  (z.setx (z.getx + 1)) ñ
et (p.bouge).bouge.getx s'évalue en 3.

Sémantique opérationnelle


Les valeurs sont les objets.

Réduction élémentaire

On note m une collection de méthodes (li = V (xiei)iÎ I.
á l = V (xe; m ñ.l ®   e {x ¬ á l = V (xe; m ñ}
á l = V (xe; m ñ.l Ü V (x')  e' ®   á l = V (x')  e'; m ñ
á m ñ.l Ü V (x')  e' ®   á l = V (x')  e'; m ñ      lÏdom (m)


Contextes d'évaluation (évaluation en tête)
E ::= {} | E.l Ü V (xe | E.l

Exemple d'évaluation

On omet V (x)  dans V (xe quand x n'apparaît pas dans e.
(á f = V (x)  x.a.geth ñ.a Üá h = 3; geth=V (x)  x.h ñ)
.f ®
á f = V (xx.a.geth; a = á h = 3; geth =V (xx.h ñ ñ.f º
á f = V (x)  x.a.geth; a = á h = 3; geth=V (x)  x.h ñ ñ.f
®
(x.a.geth) {x ¬ á f = V (xx.a.geth; a = á h = 3; geth =V (xx.h ñ ñ} º
á f = V (x)  x.a.geth; a = á h = 3; geth=V (x)  x.h ñ ñ.a
.geth ®
á h = 3; geth=V (x)  x.h ñ.geth
®
(x.h) {x ¬ á h = 3; geth =V (xx.h ñ} º
á h = 3; geth=V (x)  x.h ñ.h
®
3
Exercise 3  [Évaluateur du calcul d'objets]   Le but de cet exercice est d'écrire un évaluateur pour le calcul d'objets.

On représente les expressions du langage par le type Ocaml suivant:
type expr =
  (* Variables *)
  | Var of variable | Int of int
  (* Objets *)
  | Obj of (label * methode) list
  (* Envoi de message *)
  | Mes of expr * label
  (* Modification/Ajout de méthode *)
  | Mod of expr * label * methode
and methode = variable * expr
and variable = string
and label = string
;;
Par exemple, l = V (xx.m est représenté par le terme: Obj [ "l", ("x"Mes (Var "x""m"))]. Définir, en Ocaml, le terme représentant le programme:
(á f = V (xx.a.geth ñ.a Ü V (_) á h = 3; geth =V (xx.h ñ).f
Answer
Définir un évaluateur pour le calcul.

(C'est-à-dire définir une fonction récursive
eval qui prend en arguments un environnement d'évaluation env une expression expr et retourne le résultat de l'évaluation de l'expression expr dans l'environnement env. L'environnement d'évaluation est une liste d'association entre des variables et leur valeur. L'environnement représente la substitution qu'il faudrait appliquer au terme à évaluer.)
Answer

Héritage (simple) dans le calcul d'objet

Dans le calcul d'objet, l'héritage (simple) est modélisé par la (re)définition de méthodes.

Par exemple on peut fabriquer un bipoint q à partir d'un point p:
p =def á x = 3; getx = V (zz.x ñ
q =def (p.y Ü 5).gety Ü V (zz.y
Ce calcul ne modélise pas directement l'héritage multiple.

Codage des fonctions (non typé)

Une fonction est un objet avec une méthode qui contient le corps de la fonction:
[[fun  (xe]] = á fun = V (x[[e]] ñ
La valeur de l'argument sera mémorisé à coté du code de la fonction dans un champ arg. Aussi, l'accès à une variable devient:
[[x]] = x.arg
L'application place l'argument à coté de la fonction (fabrication d'une fermeture) et lance l'exécution.
[[e1 e2]] = ([[e1]].arg Ü V (x[[e2]]).fun
NB: ce codage est en appel par nom (l'argument n'est pas évalué avant d'être remplacé dans le corps de la fonction).

Ajout de champs valeur

On ajoute une construction e.l Ü e' (ici e' ne dépend pas de self), avec pour règle de réduction, et contextes d'évaluations:
(v.l Ü v) ® (v.l Ü V (xv)
E ::= ... | E.l Ü e | v.l Ü E

À la différence des méthodes, les champs sont évalués avant d'être ajoutés à l'objet.

L'application en appel par valeur peut être codée par:
[[e1 e2]] = ([[e1]].arg Ü [[e2]]).fun

NB: En Ocaml, les champs ne sont pas abstraits par rapport à self justement parce qu'ils sont évalués avant d'être ajoutés à l'objet! Pour voir self dans un champ, il faut abstraire par rapport à self, mais cela a aussi pour effet de geler l'évaluation.

Objets » fermetures


Codage de l'application [[(fun  (xe1) e2]]

Juste avant d'être lancé, l'application devient un objet
á fun = V (x) . [[e1]], arg = [[e2]] ñ
C'est la fermeture du corps de la fonction avec la valeur de l'argument (voir le cours langage et programmation ou le cours de compilation).

Fonctions mutuellement récursives (à plusieurs arguments)

Elles sont compilées vers un objet unique:
    ·les variables libres (définies en dehors du corps de la fonction) sont placés dans des variables d'instances.
    ·les fonctions sont des méthodes.
Le corps de chaque fonction a accès aux autres fonctions et aux variables libres.

Codage dans le lambda-calcul

On montre ici le codage réciproque du calcul d'objet dans le lambda-calcul. L'intérêt est de vérifier le slogan:
Les objets sont des enregistrements de fonctions!
Toutefois, il faut au préalable étendre le lambda-calcul avec des enregistrements extensibles.

Calcul avec enregistrements extensibles

Pour modéliser les objets, on ajoute des enregistrements extensibles. On se donne un ensemble dénombrable d'étiquettes, et trois nouvelles constructions:
e ::=   ...      Comme dans le lambda-calcul
|   li = ei }      Enregistrement
|   x with l = e }      Ajout ou modification de champ
|   x.l      Accès
Les enregistrements sont des fonctions partielles des étiquettes vers les valeurs (comme des tables d'association où les clés seraient des étiquettes).

Sémantique des enregistrements

On ajoute { li = vi } parmi les valeurs. On considère les valeurs-enregistrements modulo commutation des champs.

Contextes d'évaluation
E ::=   ...      Comme avant
|   li = vi; l = E; lj = ei }      On évalue de gauche à droite
|   E with l = e }      On évalue à gauche,
|   v with l = E }      Puis à droite
|   E.l


Radical     (soit m de la forme (li = vi)iÎ I)
l = v; m }.l ®   v
{ { l = v; m } with l = v' } ®   l = v'; li= vi }
{ { m } with l = v } ®   l = v; m }      (si l ¹ li)
Exercise 4  [Enregistrements extensibles finis]   Dans cet exercice, on veut faire découvrir le mécanisme de typage des enregistrements extensibles (sous-jacent au mécanisme de typage des objets). On se limite à un nombre fini de champs.

Pour simplifier, on se limite au cas de deux champs
a et b. On définit le type enregistrements
type ('a, 'b) ab = { a : 'a; b : 'b };;
En utilisant le type option, donner des une valeur représentant a1 correspondant à l'enregistrement  { a = 1 } définit sur une seul champ, puis une valeur a2 représentant l'enregistrement  { a = 1; b = true }.
Answer
Écire la fonction get_a qui accède au vrai contenu du champ a en supposant qu'il soit présent. Quel est le problème rencontré (par rapport au typage)?
Answer
On remplace le type option par les deux types indépendants suivant:
type 'a pre = Pre of 'a;;
type abs = Abs;;
Redéfinir a1 et a2 en utilisant ces types plutôt que le type option.
Answer
Écrire la fonction get_a qui accède au champ a seulement s'il est présent, et la fonction with_a qui ajoute à un enregistrement le champ a (comme la construction { { m } with l = v })? Définir les valeurs correpondantes pour le champ b ainsi que la valeur correspondant à l'enregistrement vide.
Answer
Reconstuire la valeur  { a = 1; b = true } à partir des primitives précédentes:
Answer

Codage des objets (non typé)

On peut coder les objets dans le lambda-calcul avec enregistrements extensibles comme des enregistrements de fonctions.
[[á li = V (xiei ñ]] = { li = fun  (xi[[ei]] }
La (re)définition de méthode est une redéfinition de champ:
[[e.l =V (xe']] = { [[e]] with l = fun  (x[[e']] }
L'envoi de message est une auto-application:
[[e.l]] = [[e]].l [[e]]

NB: Le codage de l'héritage dans le calcul d'objet fourni donc également un codage de l'héritage simple dans les enregistrements extensibles. Pour l'héritage multiple, il faut une opération de concaténation des enregistrements, primitive ou simulée.

Exercise 5  [Codage des objets avec des enregistrements]   Comme on ne possède pas des enregistrements extensibles, on se contente des enregistrements simples.

Définir un type enregistrement permettant de coder un objet point comme ci-dessus (avec champ
x et deux méthodes getx et setx). Puis donner une fonction qui prend un entier x0 et retourne le point d'abcisse x0:
Answer
Définir une fonction getx qui prend un point et lui envoie le message getx ainsi qu'une fonction setx définie de façon similaire.
Answer
Quel serait le type bpoint d'un point avec une méthode bouge? Pourquoi ne peut-on pas réutiliser le code de la fonction point ci-dessus pour créer un point qui bouge.
Answer
On pourra essayer de corriger ces deux problèmes en utilisant des enregistrement extensibles (par exemple, en se limitant aux 4 champs x, getx, setx et bouge).

Problèmes de typage

Jusqu'à présent, nous avons complètement ignoré le typage.

Le but d'un système de typage est d'éliminer tout risque d'évaluation bloquée. Le prix est une restriction de l'expressivité du langage.

Il existe différents systèmes de typage pour les objets ayant des une expressivité différente.

Certaines constructions, indépendemment correctement typées peuvent entré en conflit et être mal typées lorsqu'elles cohabitent.

Sous-typage en largeur et méthodes binaires
Conflit!
Le sous-typage en largeur (oubli de champs) en présence de méthode binaire n'est pas correct en général (voir Les points difficiles de la programmation avec objets.

Problèmes de (sous-)typage


Sous-typage en profondeur et redéfinition de méthodes
Conflit!
Une méthode m1 peut utiliser une méthode m2 avec un type t. Par sous-typage en profondeur, on peut affaiblir le type t en un type t'. La redéfinition de la méthode m2 avec le type t' serait incorrecte car elle briserait l'hypothèse faite par m1.

Sous-typage en largeur et ajout de méthodes
Conflit!
Une méthode m1 peut utiliser une méthode m2 avec un type t. Par sous-typage en largeur, on peut oublier que m2 est définie, et la redéfinir avec une méthode m3 d'un autre type t', ce qui briserait l'hypothèse faite par m1.

Problèmes de typage (solutions)


Interdire certaines combinaisons

On peut interdire globalement et simultanément
    ·Le sous-typage en profondeur ou la redéfinition de méthode,
    ·Le sous-typage en largeur ou l'ajout de méthode.




Enrichir l'information de type

On peut garder des informations plus précises sur les types et distinguer les méthodes selon qu'elles sont (1) implémentées, (2) utilisées dans la vue interne, ou (3) utilisées dans la vue externe. De même on peut se souvenir si les contraintes sont exactes ou si le sous-typage a été utilisé, etc.

Cela donne des systèmes de types plus précis, mais aussi en général trop complexes...

Problèmes de typage (prototypes)


Distinguer objets et prototypes

Pour pallier au problème ci-dessus, on peut distinguer:
    ·Les prototypes: ce sont des objets auxquels on peut ajouter des méthodes, mais pas envoyer de message, ni les sous-typer.
    ·Les objets: on ne peut plus ajouter de méthodes, mais on peut envoyer des messages et les sous-typer.
On passe d'un prototype à un objet par sous-typage (opération irréversible).
Solution en peigne!
Malgré tout, cela ne résout pas tous les problèmes.

Les vues


Utilisation de vues

Elles permettent de renommer les noms de méthodes et ainsi de les dissocier de leur implémentation. Un même nom peut avoir plusieurs implémentations. On peut oublier un nom, et le redéfinir, mais avec une nouvelle implémentation (sans écraser l'implémentation précédente).

NB: Les langages avec vues sont encore compliqués ou limités, et la conception d'un langage avec vues simple et expressif reste du domaine de la recherche...

Les solutions consistent à ajouter une indirection supplémentaire; on distingue donc les noms de méthodes et leur emplacement d'une part, l'allocation d'un emplacement et sa définition d'autre part.

Méthodes relogeables


  Un objet p =def dDD est le dictionnaire externe, Di et Dk sont des dictionnaires internes.
d =def
æ
ç
ç
è
i = [c |® i, b |® j], rain
j = ..., storm
k = [b |® k], wind
ö
÷
÷
ø
D =def [a |® j, b |® k]

Problème de typage (codage)

Le codage des objets avec des types enregistrement ne préserve pas le typage: la tranformation d'une méthode en une fonction abstraite par rapport à self en fait une méthode binaire, ce qui interdit la possibilité de sous-typage.

Il existe des codages plus compliqués qui préservent le typage.

Encapsulation

L'encapsulation des données est la possibilité de cacher l'état interne des objets, ie. la représentation des données et de ne montrer que leur interface vers le monde extérieur.

C'est une composante importante des objets que nous n'avons pas encore détaillée. Il y a principalement trois approches:
    ·Cacher les variables d'instance.
    ·Cacher leur type, en utilisant des types existentiels.
    ·Cacher leur type, par sous-typage en largeur.
Une dernière solution est de ne pas avoir d'encapsulation... C'est le cas par exemple de l'approche avec surcharge. L'encapsulation peut également être laissée au langage de modules.

Encapsulation (par abstraction de valeur)

C'est l'approche la plus facile: les variables d'instances ne sont jamais accessibles de l'extérieurs, de façon analogue aux liaisons locales:
let résultat =
  let x = 1 and y = 2  in
  x + y;;
Cette approche impose que les variables d'instances soient une construction primitive. Elle est compliquée par rapport aux liaisons locale par la possibilité d'héritage.

C'est la solution retenue en Ocaml.

En Java, l'approche correspond à cacher les valeurs, mais elle est plus complexe: elle utilise la notion de package, qui se situe plus au niveau des modules que des classes.

Encapsulation (par abstraction de type)

Un objet est une paire (r,m) composée des variables d'instance I et des méthodes M.

Dans la classe self a un type de la forme R × M.

L'état interne est caché à l'extérieur, ie. un objet de cette classe a un type existentiel de la forme $ (R) (R × M).

Toutefois, les méthodes de M dépendent aussi du type de R et simultanément du type externe de l'objet; la vérité est donc un peu plus compliquée... rec a. $ (R) (R × M(R, a))

Cette méthode est utilisée pour le codage des objets avec des enregistrements.

Encapsulation (par sous-typage)

On utilise le sous-typage en largeur. C'est l'approche retenue dans le calcul d'objet.

Elle ne s'applique qu'en l'absence de méthodes binaires, ou bien il faut utiliser un système de typage plus riche pour garantir que la variable d'instance n'a pas été utilisée de façon externe à l'intérieur de la class (ie. en accédant à un objet qui n'est pas self mais du même type que self).


This document was translated from LATEX by HEVEA and HACHA.