Notes du cours de DEA : Typage et programmation

Informations

• Publié par: Thaub
• Nombre de lectures: 66
• Langue: Français

Extrait

Notes du cours de DEA
\Typage et programmation"
Xavier Leroy
[e-mail]
Version du December 13, 2001
http://pauillac.inria.fr/~xleroy/dea/Contents
1 Mini-ML: evaluation et typage 4
1.1 Syntaxe de mini-ML . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
1.2 Evaluation de mini-ML: semantique operationnelle a\ grands pas" . . . . . . . . . . 5
1.2.1 Les valeurs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
1.2.2 Rappels sur les regles d’inferences . . . . . . . . . . . . . . . . . . . . . . . . 6
1.2.3 Les regles d’evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
1.2.4 Determinisme de l’evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
1.3 Typage de mini-ML . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
1.3.1 L’algebre de types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
1.3.2 Les regles de typage { typage monomorphe . . . . . . . . . . . . . . . . . . . 11
1.3.3 Schemas de types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
1.3.4 Les regles de typage { typage polymorphe a la ML . . . . . . . . . . . . . . . 13
1.3.5 Quelques proprietes des regles de typage . . . . . . . . . . . . . . . . . . . . . 14
2 Suret^ e du typage et semantique a reduction 16
2.1 Distinguer erreurs d’execution et non-terminaison . . . . . . . . . . . . . . . . . . . . 16
2.1.1 Tout programme bien type s’evalue-t’il en une valeur? . . . . . . . . . . . . . 16
2.1.2 Regles d’erreurs en semantique operationnelle structurelle . . . . . . . . . . . 17
2.2 Semantique a reductions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
2.3 Suret^ e du typage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.3.1 La relation \^etre moins typable" . . . . . . . . . . . . . . . . . . . . . . . . . 21
2.3.2 Hypotheses sur les operateurs . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
2.3.3 Typage et substitution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
2.3.4 Preservation du typage par reduction . . . . . . . . . . . . . . . . . . . . . . 24
2.3.5 Les formes normales bien typees sont des valeurs . . . . . . . . . . . . . . . . 25
2.3.6 Pour nir . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
3 Inference de types 27
3.1 Introduction a l’inference de types . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
3.2 Inference de types pour mini-ML avec typage monomorphe . . . . . . . . . . . . . . 28
3.2.1 Construction du systeme d’equations . . . . . . . . . . . . . . . . . . . . . . . 29
3.2.2 Lien entre typages et solutions des equations . . . . . . . . . . . . . . . . . . 30
3.2.3 Resolution des equations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
3.2.4 L’algorithme d’inference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
3.3 Inference de types pour mini-ML avec typage polymorphe . . . . . . . . . . . . . . . 32
13.3.1 L’algorithme W de Damas-Milner-Tofte . . . . . . . . . . . . . . . . . . . . . 33
3.3.2 Proprietes de l’algorithme W . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
3.3.3 Typage polymorphe de ML par expansion des let . . . . . . . . . . . . . . . 38
3.3.4 Complexite du typage polymorphe de ML . . . . . . . . . . . . . . . . . . . . 40
4 Extensions simples de mini-ML 41
4.1 Les n-uplets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
4.2 Les types concrets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
4.3 Les enregistrements declares . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
4.4 Les contraintes de types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
4.5 Les references et autres structures de donnees mutables . . . . . . . . . . . . . . . . 46
4.6 Les exceptions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
5 La programmation imperative 47
5.1 Les references . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
5.2 Semantique a reduction pour les references . . . . . . . . . . . . . . . . . . . . . . . . 48
5.3 Typage des references . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
5.4 Restreindre la generalisation aux expressions non expansives . . . . . . . . . . . . . . 52
5.5 Preuve de suret^ e du typage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
5.6 Autres approches . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
5.6.1 Les references monomorphes . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
5.6.2 Les variables faibles de Standard ML . . . . . . . . . . . . . . . . . . . . . . . 58
5.6.3 Systemes d’e ets et de regions . . . . . . . . . . . . . . . . . . . . . . . . . . 59
5.6.4 Variables dangereuses et typage des fermetures . . . . . . . . . . . . . . . . . 59
5.7 Les exceptions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
5.8 Continuations et operateurs de contr^ ole . . . . . . . . . . . . . . . . . . . . . . . . . 61
6 Les enregistrements extensibles 62
6.1 Semantique a reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
6.2 Typage simpli e des enregistrements extensibles . . . . . . . . . . . . . . . . . . . . 63
6.3 T avec rangees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
6.3.1 L’algebre de types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
6.3.2 Regles de typage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
6.3.3 Sortes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
6.3.4 Regles de typages avec sortes . . . . . . . . . . . . . . . . . . . . . . . . . . . 69
6.4 Suret^ e du typage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69
6.5 Inference de types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70
6.5.1 Uni cation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70
6.5.2 Inference de types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72
6.6 Les sommes ouvertes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74
7 Programmation par objets et classes 75
7.1 Un calcul d’objets sans classes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
7.1.1 Syntaxe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
7.1.2 Regles de reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
7.1.3 L’algebre de types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
27.1.4 Regles de typage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
7.1.5 Suret^ e du t . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
7.1.6 Inference de types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
7.2 Sous-typage et subsomption explicite . . . . . . . . . . . . . . . . . . . . . . . . . . . 79
7.3 Classes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81
7.3.1 Evaluation des classes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81
7.3.2 Typage des classes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81
7.4 Les types recursifs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83
7.4.1 Presentations des types recursifs . . . . . . . . . . . . . . . . . . . . . . . . . 84
7.4.2 Sous-typage et types recursifs . . . . . . . . . . . . . . . . . . . . . . . . . . . 85
7.4.3 Inference en presence de types recursifs . . . . . . . . . . . . . . . . . . . . . 86
7.5 Inference par contraintes de sous-typage . . . . . . . . . . . . . . . . . . . . . . . . . 86
7.5.1 Regles de typage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86
7.5.2 Construction du systeme de contraintes . . . . . . . . . . . . . . . . . . . . . 87
7.5.3 Lien entre typages et solutions des equations . . . . . . . . . . . . . . . . . . 88
7.5.4 Coherence d’un systeme de contraintes . . . . . . . . . . . . . . . . . . . . . . 88
7.5.5 Algorithme d’inference de types . . . . . . . . . . . . . . . . . . . . . . . . . . 90
8 Systemes de modules 94
8.1 Un calcul de modules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94
8.2 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95
8.2.1 Semantique par traduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95
8.2.2 Semantique a reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95
8.3 Regles de typage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97
8.3.1 Equivalence entre types de base . . . . . . . . . . . . . . . . . . . . . . . . . . 97
8.3.2 Typage du langage de base . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98
8.3.3 Sous-typage entre types de modules . . . . . . . . . . . . . . . . . . . . . . . 99
8.3.4 Typage du langage de modules . . . . . . . . . . . . . . . . . . . . . . . . . . 101
A Corriges des exercices du chapitre 1 108
B Corriges des exercices du chapitre 2 114
C Corriges des exe