Formalisation du langage

 Formalisation du langage

Le but de cette thèse est d’étudier différentes techniques de sous-typage au dessus d’un langage à la ML (cf. [CD86]). Ces techniques ont toutes pour but d’étendre le nombre de programmes acceptés par le typeur, mais par des biais différents. Nous verrons par la suite qu’en combinant ces approches « orthogonales », nous pouvons obtenir des systèmes de types plus riches permettant de modéliser, sans ajout de construction de langage, des « concepts » de plus haut niveau comme par exemple les « objets ». Pour permettre ces combinaisons, le langage étudié dans cette thèse varie assez peu en fonction des chapitres, tout comme sa sémantique. Il s’agit d’un ML classique étendu avec des « constructeurs de données » et du « filtrage de motifs ».

Le noyau du langage 

Le noyau de notre langage est un simple λ-calcul. Il s’agit d’un langage « à expressions », au sens où tout programme dans notre langage est une expression. L’ensemble e des expressions est défini par la grammaire suivante :
e ::= x | λ x . e | e1 e2

On nomme « λ-terme » une expression de ce langage. Dans cette définition, comme en λ-calcul classique, x représente l’ensemble des variables utilisables dans les programmes, la construction (λ x . e) représente une fonction ayant pour paramètre x et pour corps e, et la construction (e1 e2) représente l’application de la fonction e1 sur l’argument e2. Chaque variable apparaissant dans un λ-terme est alors soit libre, soit liée par λ. Les termes auxquels nous nous intéresserons dans cette thèse seront tous « clos » au sens où ils ne contiendront aucune variable libre.

Le λ-calcul est déjà suffisant pour représenter n’importe quel « calcul ». Il est important de remarquer que l’évaluation d’une expression ne se résume pas à une simple réduction des membres du terme un à un jusqu’à obtenir le résultat comme le serait la réduction d’une expression arithmétique classique. Il est en particulier possible d’encoder en un simple λ-terme un calcul qui boucle infiniment. Un exemple très classique d’un tel terme est :

(λ x . x x) (λ x . x x)

Il est également possible de définir des constantes et des opérateurs sur ces constantes sous forme de λ-termes. Par exemple, il est possible de définir les constantes entières avec la méthode de Church :

0 , λ f x . x
1 , λ f x . f x
2 , λ f x . f (f x)
3 , λ f x . f (f (f x))
…

et les opérateurs successeur, addition et multiplication ainsi :

succ , λ n f x . f (n f x)
(+) , λ m n . m succ n
(ˆ) , λ m n f . m (n f)

Le lecteur pourra vérifier que ces opérateurs, appliqués à des λ-termes représentant des entiers comme définis précédemment, vérifient bien la sémantique standard des opérateurs arithmétiques. Ce genre de technique peut servir à définir de nombreux concepts calculatoires et structures de contrôle, et c’est ce qui fait la puissance et la beauté du λ-calcul. Pour l’expressivité du langage, il serait donc suffisant de se limiter au λ-calcul. Néanmoins, dans le cadre plus concret d’un langage de programmation, tout définir à partir de λ-termes est problématique. La syntaxe du langage peut certes masquer la complexité des λ-termes cachés derrière les valeurs manipulées, mais les performances d’un évaluateur de λ-calcul sont rapidement dépassées par celles d’un calculateur travaillant sur des données représentées dans un format « binaire » plus classique. De plus, du point de vue de l’analyse statique, une représentation de toutes les valeurs sous forme de λ-termes peut affaiblir les vérifications de la cohérence d’un programme. En effet, plusieurs « concepts » différents peuvent être représentés par le même λ-terme et empêcher la détection de certaines confusions dans le code. À l’inverse, il est intéressant d’associer des «types de base » différents aux différentes classes de constantes et d’enrichir le langage en structures de contrôle pour les distinguer lors du typage des programmes.

Les constantes

Comme expliqué précédemment, plutôt que de définir les constantes sous forme de λ-termes, nous préférons étendre la définition des expressions avec un ensemble c de « constantes prédéfinies » :
e +:= c
c ::= () | true | false | n | s
n ::= 0 | 1 | -1 | …
s ::= «  » | …

où « +:= » désigne l’extension d’une règle de grammaire existante avec une ou plusieurs nouvelles constructions de syntaxe. L’ensemble des constantes n’est volontairement pas figé dans le contexte théorique de cette thèse. Bien évidemment, une implémentation concrète d’un langage de programmation, pour qu’elle soit pratique à utiliser, définira un ensemble de constantes bien fourni. Cet ensemble contiendra typiquement les booléens, les entiers, les flottants, les caractères, les chaînes de caractères, etc.

Les primitives

Notre langage étant muni de constantes définies autrement que par des λ-termes, il est nécessaire de l’enrichir de primitives permettant de manipuler ces constantes. Ces primitives correspondent aux opérateurs de base que l’on trouve classiquement dans les langages : les opérateurs logiques sur les booléens, les opérateurs arithmétiques classiques sur les nombres entiers et flottants, des opérateurs de manipulation des chaînes, etc.

Nous remarquerons que notre définition des primitives ne permet de les utiliser dans une expression que en leur passant immédiatement tous leurs arguments. Certains langages comme OCaml permettent d’utiliser les opérateurs seuls en tant que fonctions. Il est ainsi possible d’écrire « let f = (+) in … » ce qui est équivalent à « let f= (λ x y . x + y) in … ». Nous préférons ne pas introduire cette notation dans notre définition des expressions car cela compliquerait inutilement les règles de typage et de sémantique. Une telle notation peut alors simplement être vue comme du sucre syntaxique, et donc expansée lors de l’analyse syntaxique des programmes.

Tout comme pour les constantes, notre langage sera donc toujours « paramétré » par un ensemble de primitives. Pour pouvoir travailler avec cet ensemble inconnu de primitives, il devra être fourni avec deux fonctions δ1 et δ2 définissant la sémantique des primitives respectivement unaires et binaires (voir la section 1.2), et une fonction T de typage des constantes et des primitives utilisée dans les systèmes de types (voir la section 2.3). Les fonctions T, δ1 et δ2 devront également être liées par une relation de compatibilité pour assurer la validité du typage vis-à-vis de la sémantique.

Les n-uplets

Il est parfois pratique en programmation de regrouper, dans une même valeur, plusieurs valeurs en créant un couple, un triplet, un quadruplet, etc. De telles constructions sont bien sûr encodables avec de simples λ-termes mais pour les mêmes raisons que précédemment, il est en général préférable d’étendre le langage des expressions avec une construction syntaxique spécifique. Pour simplifier les règles de sémantique et de typage, on préférera ne définir que les 2-uplets (ou « couples ») et encoder les n-uplets pour n > 3 comme une imbrication de couples (e1, (e2, (e3, …))). Nous n’ajoutons alors que la construction de couple à notre définition des expressions : e +:= (e1, e2)

Pour extraire les valeurs d’un couple, l’approche standard consiste à étendre le filtrage de motifs (défini en section 1.1.9). Par simplicité pour les règles de sémantique et de typage, nous préférons réserver, dans cette thèse, le filtrage de motifs aux constructeurs de données (voir section 1.1.5) et définir à la place les deux primitives d’arité 1, fst et snd dont la sémantique est respectivement d’extraire le premier et le second élément d’un couple : p 1 +:= fst | snd

Table des matières

Introduction
1 Langage
1.1 Formalisation du langage
1.1.1 Le noyau du langage
1.1.2 Les constantes
1.1.3 Les primitives
1.1.4 Les n-uplets
1.1.5 Les constructeurs de données
1.1.6 La construction « let x = e1 in e2 »
1.1.7 Le let récursif
1.1.8 La conditionnelle
1.1.9 Le filtrage de motifs
1.1.10 La mutabilité
1.1.11 Résumé
1.2 Sémantique
1.2.1 Les « valeurs »
1.2.2 Un « petit pas » pour l’évaluateur
1.2.3 Le contexte d’évaluation
1.2.4 Un « grand pas » pour l’évaluation
1.2.5 Les expressions « bloquées »
1.2.6 Plusieurs pas d’évaluation
1.2.7 La fonction d’évaluation
2 Système de types de base
2.1 Contexte
2.1.1 Principes de base
2.1.2 Approches classiques du sous-typage
2.1.3 Manipulation de contraintes sans résolution
2.2 Formalisme utilisé
2.2.1 Notre approche
2.2.2 Schémas de type
2.2.3 Environnement de typage
2.2.4 Règles d’inférence
2.3 Règles du système de types de base
2.3.1 Règle d’instanciation
2.3.2 Règles de typage
2.3.3 Règles de saturation
2.3.4 Exemple
2.4 Validité du typage
2.4.1 Définitions préliminaires
2.4.2 Terminaison
2.4.3 Théorèmes de validité
2.4.4 Schéma des preuves
2.4.5 Preuve de validité du système de base
2.5 Gestion de la mutabilité
2.5.1 Modification du système de types
2.5.2 De nouvelles primitives
2.5.3 Exemple
2.5.4 Remarques sur la variance
2.6 Renforcement du typage
2.6.1 Motivation
2.6.2 Une nouvelle relation : p«q
2.6.3 Adaptation de la saturation
2.6.4 Remarques
3 Typage affiné du filtrage de motifs
3.1 Contexte
3.2 Motivation
3.3 Modification du langage des contraintes
3.4 Adaptation des règles d’inférence
3.5 Exemple simple d’utilisation
3.6 Adaptation de la preuve de terminaison
3.7 Adaptation de la preuve de validité
3.8 Exemple concret d’application : un encodage des « objets »
4 Amélioration de la généralisation
4.1 Contexte
4.2 Motivation
4.3 Principes généraux du nouveau système de types
4.4 Nouvelles règles d’inférence
4.5 Terminaison de l’algorithme d’inférence
4.6 Adaptation de la preuve de validité
4.7 Signification de la taille limite des clés
Conclusion

Télécharger le rapport complet