Implémentation d'un évaluateur et typeur pour le lambda-calcul en Scala, couvrant la représentation des termes par AST, l'alpha-conversion, la substitution, la réduction en stratégie Left-to-Right Call-by-Value (LtR-CbV) et l'inférence de types par génération d'équations et unification. Le projet inclut également des extensions vers les traits impératifs (références mutables) et le polymorphisme faible.
Architecture du projet
Le code est organisé en modules distincts reflétant les étapes du pipeline d'évaluation :
- ast —
PTerm(termes : Var, Abs, App, Let, IfZero…) etPType(types : TypeArr, RefType, ListType, ForAll…) viasealed traitpour une extensibilité contrôlée. - utils —
AlphaConverter(renommage des variables liées avec compteur global),PrettyPrinterTermetPrettyPrinterType(affichage lisible),TypeUtils. - eval —
Substitution,LtRCbVReducer,Normalizer(réduction jusqu'à forme normale ou détection de divergence via timeout). - types —
TypeInference(génération d'équations de typage),Unification(résolution),TypeVarGenerator.
Composantes implémentées
Alpha-conversion et substitution
L'alpha-conversion utilise un compteur global pour garantir des noms de variables uniques, évitant les captures lors des substitutions. La substitution gère explicitement les variables liées et libres — les cas complexes d'imbrication dans Abs et Let ont causé des échecs dans certains tests, identifiés comme dues à une gestion insuffisante des conflits de noms en contexte multi-niveaux.
Réduction LtR-CbV et normalisation
La réduction suit la stratégie Left-to-Right Call-by-Value : les arguments sont évalués avant application. La normalisation itère la réduction jusqu'à atteindre une forme normale ou déclencher un timeout (détection de divergence). Les termes simples passent tous les tests ; les termes combinant Ref, Assign et Deref échouent partiellement en raison d'une synchronisation inadéquate de l'état mémoire mutable entre opérations.
Inférence de types par unification
L'inférence repose sur la génération d'équations de typage suivie de leur résolution par unification (cas explicites pour TypeArr, ListType, RefType). C'est la partie la plus défaillante du projet : 12 tests sur 14 échouent, principalement à cause d'un ordre incorrect dans les équations d'unification et d'une gestion incomplète de ForAll et WeakType (polymorphisme faible / non-expansivité).
Bilan et retours d'expérience
| Composante | Résultat |
|---|---|
| AST des termes (Var, Abs, App) | Réussi |
| Pretty printers | Réussi |
| Alpha-conversion | Réussi |
| Substitution | Réussi |
| Réduction LtR-CbV | Partiel — échecs sur termes complexes |
| Normalisation | Partiel — fonctionne pour cas simples |
| Inférence de types | Échec — 12/14 tests échouent |
| Unification | Échec — 4/9 tests échouent |
| Polymorphisme faible (WeakType) | Non implémenté |
| Traits impératifs (Ref, Deref, Assign) | Partiel |
Deux décisions ont pesé sur le résultat final :
- Migration OCaml → Scala en milieu de projet — motivée par l'envie d'explorer Scala, cette décision a introduit un coût d'adaptation non négligeable sur les modules d'inférence et d'unification, pour lesquels OCaml aurait été plus naturel.
- Absence de TDD — sans tests écrits en amont, la correction d'un module entraînait fréquemment des régressions dans d'autres, particulièrement visible entre la réduction LtR-CbV et l'inférence de types.
