Première Partie : Noyau fonctionnel
Chapitre 1 : Introduction au l-calcul
Le l-calcul a été inventé par Alonzo Church en 1932
(il était déjà présent en germe dans le travail de Frege au début
du siècle). Le but de Church était de définir
la notion de calculabilité effective au moyen de la
l-définissabilité. Plus tard, il apparut que la notion ainsi
introduite était équivalente aux notions de calculabilité au sens de
Turing (machine de Turing) et de Gödel-Herbrand (fonctions récursives).
Cette coïncidence
incite à penser qu'il existe une notion de calculabilité
universelle, indépendante des formalismes particuliers : c'est la thèse de
Church.
Le but de cette section est de présenter brièvement le
l-calcul, qui sert de base théorique à tout langage fonctionnel
bien conçu. Plus qu'un cours formel, il s'agit d'une introduction
qu'on espère motivante et qui pourra inciter le lecteur intéressé à
consulter la littérature pour plus de détails (voir bibliographie).
C'est pourquoi on n'y trouvera guère de démonstrations.
Chapitre 2 : Introduction au l-calcul typé
On a vu que le l-calcul est la pure théorie de la
fonctionalité. Mais on peut vouloir associer à chaque variable d'un
terme un type qui indique sa nature fonctionnelle, c'est-à-dire ses
domaine et codomaine. C'est naturel quand on pense aux mathématiques où
on s'intéresse rarement à une fonction indépendamment de son ensemble
de départ et de son ensemble d'arrivée.
Les types permettent de retrouver cette idée dans le l-calcul.
De plus, ils ont un intérêt calculatoire, car
l'intérêt d'un système de types pour le l-calcul (d'un point
de vue théorique) est d'assurer la forte normalisation des termes
typables. Ce sera le cas du système que nous allons voir, qui est le plus
simple de tous. C'est pourquoi on l'appelle le système des types simples.
Dans cette optique, le l-calcul est vu comme un langage de
programmation, et les types assurent la terminaison des programmes typables
(indépendamment de la stratégie de réduction).
Chapitre 3 : Typage d'un mini-ML
Un compilateur ML se décompose de manière classique en :
-
une analyse lexicale puis syntaxique du texte source en entrée qui construit un arbre de syntaxe;
- un vérificateur de types qui infère les types des expressions et détecte donc les erreurs
de typage;
- un producteur de code assembleur, souvent d'une machine abstraite;
- et d'une phase d'assemblage pour exécuter ce code sur un processeur existant.
On se propose dans cette section de définir la syntaxe abstraite d'un langage appelé mini-ML,
qui est un sous-ensemble de Caml-light et de montrer son mécanisme de typage, qui à des simplifications
près est celui de Caml-light. Mini-ML correspond au noyau fonctionnel de Caml-light sans
le filtrage. Il ne contient ni exceptions ni traits impératifs. Cette dernière restriction
simplifie le vérificateur de types sans en changer la nature profonde. L'algorithme d'unification
est assez différent de celui déjà vu pour le typage du l-calcul car il appliquera
directement, en faisant une modification physiques sur les types, les substitutions de variables de type.
Le programme de vérification de types s'inspire des deux exemples de Michel Mauny que l'on peut lire dans
la présentation d'une ``spécification CAML d'un sous-ensemble de CAML'' et du langage ASL de la documentation Caml-light (voir bibliographie).
Chapitre 4 : Panorama des langages fonctionnels
Chapitre 5 : Evaluation d'un mini-ML
Un interprète ML se décompose en :
-
une analyse lexicale puis syntaxique du texte source en entrée qui construit un arbre de syntaxe;
- un vérificateur de types qui infère les types des expressions et détecte donc les erreurs de typage;
- un évaluateur d'expressions bien typée qui calcule effectivement la
valeur demandée
On étudiera dans cette section uniquement la partie évaluation, sachant que
les deux premières parties ont déjà été traitées pour la partie typage.
On travaillera toujours sur le sous-ensemble de mini-ML(3.14). Cet
exemple s'inspire des exemples donnés dans
la présentation d'une ``spécification CAML d'un sous-ensemble de CAML''
et dans le livre ``Approche fonctionnelle de la programmation'' (voir bibliographie). Les sources de l'evaluateur se trouvent dans le catalogue \~emmanuel/96-97/EVAL. Le Makefile permet de construire l'exécutable complet
de l'interprète. Celui-ci est plus complet que la description de mini-ML.
On ne s'intéressea ici qu'à la partie mini-ML.
Chapitre 6 : Compilation
Références
- [AJ87]
-
L. Augustsson and T. Johnsson.
Lml users manual.
Technical report, Goteborg University - Department of Computer
Science, 1987.
- [Aug87]
-
L. Augustsson.
Compiling Lazy Funtional Languages PartII.
PhD thesis, Chalmers University of Technology Goteborg, 1987.
- [Bar84]
-
Barendregt.
The lambda-calculus: its syntax and semantics.
North Holland, 1984.
- [Chu41]
-
A. Church.
The Calculi of lambda-conversion.
Princeton University Press, 1941.
- [HS86]
-
Hindley and Seldin.
Introduction to Lambda-Calculus and Combinators.
Cambridge Press, 1986.
- [Hue89]
-
G. Huet.
Initiation au l-calcul.
Notes de cours, 1989.
- [HW90]
-
P. Hudak and P. Waddler.
Report on the programming language haskell, a non-strict, purely
functional language.
Technical report, April 1990.
- [Ler92]
-
Xavier Leroy.
Typage polymorphe d'un langage algorithmique.
Thèse de doctorat, Université Paris 7, 1992.
- [Mil78]
-
R. Milner.
A theory of type polymorphism in programming.
J. Comput. Syst. Sci., 1978.
- [Par88]
-
M. Parigot.
Preuves et Programmes : les Mathematiques comme Langage de
Programmation.
aperçu des mathématiques, (CNRS), 1988.
- [Str77]
-
Strachey.
Denotational Semantic.
MIT Press, 1977.
- [Tur85]
-
D.A. Turner.
Miranda: A non-strict functional language with polymorphic types.
FPCA - Lecture Notes in Computer Science 201, 1985.
Ce document a été traduit de LATEX par
HEVEA et HACHA.