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 :

ÉtapeQuestionIdée nouvelleVérification dans le squelette
Règles, bronzeQuelles conditions imposent les opérations et case ?Une règle par forme d’arbre, sur des types déjà connusmix test
Unification, début d’argentComment 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 égalesmix test --include argent, en regardant d’abord les tests « la substitution » et « l’unification » de argent_test.exs
Fonctions, fin d’argentComment les usages contraignent-ils un paramètre ?Une inconnue fraîche par paramètre, puis les contraintes du corps et des appelsmix test --include argent
Polymorphisme, orQuand 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 letmix 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.

Ouvrir le fascicule (PDF)