Current state of my thesis |
Final versionAvailable in gzipped postscript and pdf. |
SummaryThe topic of this thesis is the conception of a system of mixin modules for call-by-value languages. Mixin modules are a notion of modules that seems amenable to solve several problems of existing module systems, notably that of ML. In particular, they allow mutually recursive definitions to span module boundaries, and feature mechanisms for modifying existing modules, thus making incremental programming possible. In call-by-value languages, mixin modules conflict with the usual notion of recursive definition. Generally, such languages restrict recursive definitions to a certain class of expressions, typically functions, whereas arbitrary recursive definitions can appear dynamically with mixin modules. This makes mixin modules difficult to design in the context of most existing call-by-value languages. In a first part, we characterize the usual class of recursive definitions allowed by call-by-value languages. We extend this class so as to preserve the efficiency of our language. We obtain an enriched lambda-calculus, and study its compilation and typing. In a second part, building on this base, we define a high-level kernel language of call-by-value mixin modules. We formalize a type system for this language, and prove its soundness. Finally, we give a translation function from our language of mixin modules to the enriched lambda-calculus of the first part. RésuméLe sujet de cette thèse est la conception d'un système de modules mixins pour les langages en appel par valeur. Les modules mixins sont une notion de modules qui semble à même de résoudre plusieurs problèmes des systèmes de modules existants, notamment celui de ML. En particulier, ils permettent aux définitions mutuellement récursives de s'étaler sur plusieurs modules et offrent des mécanismes pour modifier des modules existants, rendant ainsi possible la programmation incrémentale. Dans les langages en appel par valeur, les modules mixins entrent en conflit avec la notion habituelle de définition récursive. Généralement, ces langages restreignent les définitions récursives à une certaine classe d'expressions, typiquement les fonctions, alors que des définitions récursives arbitraires peuvent apparaître dynamiquement avec les modules mixins. Cela rend la définition des modules mixins difficile dans la plupart des langages en appel par valeur connus. Dans une première partie, nous caractérisons la classe habituelle de définitions récursives permise par les langages en appel par valeur. Nous étendons cette classe de façon à préserver l'efficacité de notre langage. Nous obtenons un lambda-calcul enrichi dont nous étudions la compilation et le typage en détails. Dans une deuxième partie, munis de cette base, nous définissons un langage noyau de modules mixins en appel par valeur de haut niveau. Nous formalisons un système de types pour ce langage, dont nous prouvons la sûreté. Enfin, nous donnons une fonction de traduction de notre langage de modules mixins vers le lambda-calcul enrichi de la première partie. |