Notre interpréteur d’AP2 exécute un programme et notre machine d’AP3 exécute
son bytecode. Peut-on refuser certains programmes avant de les lancer ? C’est
le rôle d’un typeur : un programme qui, à partir de règles, déduit le type
de chaque expression (Float, Bool, une fonction de Float vers Bool…)
sans calculer aucune valeur. Vous construirez ce typeur, puis expliquerez
précisément ce qu’il garantit et ce qu’il laisse ouvert. Le projet commence
en semi-autonomie pendant AP9 et se termine à la maison. Cette première
version décrit le parcours ; le barème et l’échéance seront précisés avant
le lancement en janvier. Les paliers bronze, argent et or décrivent l’ordre
des idées, pas des niveaux de note.
Partir d’un projet qui compile
Téléchargez le squelette mini-typeur, extrayez-le
dans votre dépôt de travail et ouvrez son dossier dans VS Code. Vous devez
y voir mix.exs, lib/ et test/. Dans le terminal de ce dossier :
mix compile
mix test
Le projet compile sans dépendance externe. Au départ, les sept tests du palier bronze échouent en signalant les fonctions « à implémenter » ; les dix-neuf tests des paliers suivants restent exclus tant que vous ne les demandez pas. Ces échecs annoncent le travail à faire, pas une installation ratée. Le README explique les commandes, les contrats et les erreurs attendues. Elixir et Mix sont ceux préparés avant AP6.
Le lexer, le parser et l’affichage des types sont fournis :
MiniTypeur.Syntaxe.parse("1.0") rend l’arbre {:number, 1.0}, le même AST
qu’en AP2. Vous pouvez donc travailler sans avoir terminé votre parser d’AP2.
Les essais directs sur des AST écrits à la main restent utiles pour isoler
une règle.
Suivre quatre étapes, dans un seul projet
Les quatre carnets Types expliquent chaque algorithme et proposent des indices successifs. Le projet Mix est votre version de référence : vous pouvez lire un carnet et écrire directement dans le fichier indiqué par son README. Si vous préférez essayer une fonction dans Livebook, reportez-la ensuite dans le projet ; il n’est pas demandé de maintenir deux versions.
Chaque étape apporte une idée nouvelle, que son carnet introduit avec un exemple avant de vous faire écrire l’algorithme :
| Étape | Question | Idée nouvelle | Vérification dans le squelette |
|---|---|---|---|
| Règles, bronze | Quelles conditions imposent les opérations et case ? | Une règle par forme d’arbre, sur des types déjà connus | mix test |
| Unification, début d’argent | Comment résoudre des types encore inconnus ? | Une inconnue t0 est un type à déterminer ; unifier deux types, c’est trouver ce qui rend leurs formes égales | mix test --include argent, en regardant d’abord les tests « la substitution » et « l’unification » de argent_test.exs |
| Fonctions, fin d’argent | Comment les usages contraignent-ils un paramètre ? | Une inconnue fraîche par paramètre, puis les contraintes du corps et des appels | mix test --include argent |
| Polymorphisme, or | Quand peut-on renouveler les inconnues à chaque usage ? | Un nom défini par let conserve un schéma, c-à-d. un type dont certaines inconnues sont renouvelées à chaque lecture : c’est le polymorphisme de let | mix test --include argent --include or |
Les commandes sont cumulatives : la dernière lance les trois paliers, alors
que --include or seul laisserait les tests argent exclus.
Le README donne la correspondance entre MiniTypes dans les carnets et les
trois modules du squelette, Regles, Unification et MiniTypeur. L’AST est
identique. Au bronze, utilisez MiniTypeur.Regles.infer/1 ;
MiniTypeur.check/1, qui lit un programme en texte, ne fonctionne qu’une
fois le moteur du palier argent complété. Le
diaporama de référence reprend les notions sans
remplacer les consignes de travail.
Avant de changer de palier, gardez un exemple prédit puis observé et expliquez
la règle qui le justifie. Par ex., pourquoi 1.0 / 0.0 est-il bien typé alors
que son exécution échoue ? Pourquoi le typeur examine-t-il la branche qu’un
case True n’exécutera pas ?
Faire du typeur un projet vérifié et expliqué
Les paliers constituent le parcours principal. Ajoutez ensuite vos propres
contre-exemples dans test/personnel_test.exs, sur le modèle d’un test
fourni, et rédigez COMPTE-RENDU.md dans le projet. Il doit permettre de
relancer vos vérifications, de suivre une trace de contraintes (les égalités
de types que le parcours d’un arbre impose, dans l’ordre où elles
apparaissent), de comprendre l’occurs-check (le refus de lier une inconnue
à un type qui la contient, comme t0 = fn(t0) -> Float, ce qui demanderait
un type infini) et de distinguer une inconnue partagée d’un schéma
polymorphe. Le README propose une trame et des questions pour cela.
Comparez aussi le typeur aux moteurs d’AP2–AP3 sur leur sous-ensemble commun : un programme accepté par tous, un programme exécuté par l’interpréteur mais rejeté par le typeur, et un programme bien typé qui échoue à l’exécution. Les fonctions ne sont pas dans le socle du compilateur d’AP3 ; leur ajout n’est pas un prérequis de cette comparaison.
En fin de séance, conservez votre état d’avancement et le prochain essai à faire. La poursuite à la maison fait partie du projet. Une fois le parcours principal expliqué, le carnet d’extensions propose les paires, les projections ou de meilleurs diagnostics. Ces prolongements ne remplacent pas la vérification des règles déjà écrites.
Le typeur est un sujet au choix dans le catalogue AP9 ; vous n’avez pas à réaliser les autres projets en plus. Quand un bout de syntaxe Elixir vous manque, le poly la reprend, avec un aide-mémoire en fin de volume. Pour toute question, vous pouvez me contacter par email.
Pour les curieux : le fascicule
Un petit fascicule d’approfondissement accompagne ce sujet : les idées derrière le projet, leur histoire, ce qu’elles deviennent dans les systèmes réels et quoi lire ensuite. C’est un cadeau de fin de cours ; rien n’y est à rendre.
