# Mini-typeur · Carnet 2 — Résoudre des contraintes ## Notre question Dans `fn(x) { x + 1.0 }`, personne n'a écrit le type de `x`. Nous avons pourtant une information : l'addition exige un nombre. Avant de parcourir les fonctions, nous allons construire l'outil qui transforme ces contraintes en types. > **Repères.** [Slides 13 à 21](https://ap-2026.noce.fr/slides/AP9-typeur.html#13) : inconnues, substitution, unification, occurs-check. Elixir : maps `%{}` pour la substitution, `MapSet` pour les ensembles d'inconnues. Poly, chap. 5. Vous partez d'arbres d'AP2 écrits à la main ; le squelette du projet fournit le lexer et le parser pour tester ensuite depuis le texte. À partir du carnet 2, copiez vos propres modules précédents aux emplacements indiqués, car chaque Livebook a sa propre session. Réévaluez la cellule entière après avoir modifié un module ; les vérifications signalent une erreur tant que les fonctions demandées ne sont pas écrites. Prédisez d'abord leurs résultats. Vous pouvez ajouter des fonctions auxiliaires. > 💡 Nous choisirons en cours le point de passage selon votre avancement. ```elixir defmodule Check do def equal(actual, expected) do if actual != expected do raise "Attendu #{inspect(expected)}, obtenu #{inspect(actual)}" end :ok end def error({:error, _}), do: :ok def error(value), do: raise("Une erreur était attendue : #{inspect(value)}") end ``` ## Nommer ce que l'on ne connaît pas encore Une *variable de type* `t0` représente un type encore inconnu ; elle ne représente pas une valeur du programme. Nous la codons `{:var, 0}`. Le type d'une fonction est `{:fun, [types_des_paramètres], type_du_résultat}`. Les arguments forment une liste : nos fonctions ont une arité fixe et ne sont pas automatiquement curryfiées. Une *substitution* est une map d'identifiants vers des types. Par ex. `%{0 => {:var, 1}, 1 => :float}` signifie `t0 = t1` et `t1 = Float`. Appliquer la substitution doit donc donner `Float` pour `t0`, même si la map ne contient pas directement cette valeur sous la clé 0. ### Dérouler un exemple Cherchons à rendre égaux `fn(t0) -> t0` et `fn(Float) -> t1`. | Étape | Contrainte traitée | Substitution connue | | --- | --- | --- | | Décomposer les fonctions | arguments, puis résultats | `%{}` | | Comparer les arguments | `t0 = Float` | `%{0 => :float}` | | Résoudre les résultats | `Float = t1` | `%{0 => :float, 1 => :float}` | | Relire le type initial | `fn(Float) -> Float` | inchangée | Si l'on traite les résultats en premier, on peut obtenir une map de forme différente. Les types résolus doivent néanmoins être les mêmes. Prédisez ce qui se passe en remplaçant le dernier `t1` par `Bool`. ## Le souci du type qui se contient lui-même Pour `t0 = fn(t0) -> Float`, remplacer `t0` créerait une expansion sans fin. Le contrôle d'occurrence (*occurs-check*) refuse de lier une inconnue à un type qui contient déjà cette inconnue. Le type de `fn(x) { x(x) }` nous conduira à ce souci à le carnet suivant. Nous ne construisons pas ici des types récursifs. Attention : `t0 = t0` est déjà satisfait ! Ce cas doit être reconnu avant de chercher une occurrence à l'intérieur du type. ## Concevoir le solveur > 💡 Une substitution est une map : `Map.fetch(sub, id)` rend > `{:ok, type}` ou `:error`, et `Map.put(sub, id, type)` produit la nouvelle > substitution. Une absence n'est pas une erreur de programme : l'inconnue > peut simplement rester libre. > `MapSet.new([0, 0, 1])` contient les identifiants 0 et 1 sans doublon. > `MapSet.union/2` réunit deux ensembles ; `MapSet.member?/2` teste si un > identifiant s'y trouve. Ces outils servent à exprimer l'occurs-check. Copiez **votre module `MiniTypes` du carnet 1**, puis ajoutez trois fonctions publiques et les auxiliaires nécessaires : - `resolve(type, sub)` applique transitivement la substitution à tout le type, y compris aux paramètres et au résultat d'une fonction. - `free(type)` rend un `MapSet` des identifiants des inconnues présentes. - `unify(left, right, sub)` rend `{:ok, nouvelle_substitution}` ou une erreur ; donnez au troisième argument la valeur par défaut `%{}`. Résolvez d'abord les deux côtés avec la substitution courante. Des types égaux n'ajoutent aucune contrainte. Une inconnue peut être liée à l'autre type après l'occurs-check. Deux fonctions de même arité se décomposent en contraintes sur leurs paramètres puis leur résultat. Deux types concrets différents, ou des arités différentes, sont incompatibles. Commencez par les types concrets et une inconnue, puis traitez les fonctions. Conservez vos règles du carnet 1 ; on les adaptera aux inconnues au carnet 3. ```elixir # Copiez ici votre module MiniTypes du carnet 1. # Ajoutez resolve/2, free/1 et unify/3 dans ce même module. # Prévoyez une valeur par défaut %{} pour le troisième argument de unify. ``` ## Vérifier la transitivité et l'occurs-check Le test d'égalité directe ne suffit pas. Les cas ci-dessous forcent une chaîne de remplacements, une occurrence profonde et une différence d'arité. ```elixir Check.equal(MiniTypes.infer({:number, 2.0}), {:ok, :float}) a = {:var, 0} b = {:var, 1} Check.equal(MiniTypes.unify(a, a), {:ok, %{}}) {:ok, sub} = MiniTypes.unify(a, b) {:ok, sub} = MiniTypes.unify(b, :float, sub) Check.equal(MiniTypes.resolve({:fun, [a], b}, sub), {:fun, [:float], :float}) Check.equal(MiniTypes.free({:fun, [a, :float], {:fun, [b], a}}), MapSet.new([0, 1])) {:ok, sub} = MiniTypes.unify({:fun, [a], a}, {:fun, [:float], b}) Check.equal(MiniTypes.resolve(a, sub), :float) Check.equal(MiniTypes.resolve(b, sub), :float) Check.error(MiniTypes.unify(:float, :bool)) Check.error(MiniTypes.unify({:fun, [a], a}, {:fun, [], :float})) Check.error(MiniTypes.unify(a, {:fun, [:float], {:fun, [a], :bool}})) {:ok, sub} = MiniTypes.unify(a, b) Check.error(MiniTypes.unify(b, {:fun, [a], :float}, sub)) ``` ## Indices **Premier indice.** Résoudre une inconnue consiste à chercher sa clé dans la map et à recommencer sur le remplacement éventuel. Résoudre une fonction demande un parcours de ses types enfants. **Deuxième indice.** Pour unifier les paramètres de deux fonctions, faites circuler la substitution obtenue après chaque paire. La paire suivante doit voir les contraintes ajoutées par les précédentes. **Troisième indice.** Calculez `free(type)` récursivement et testez l'appartenance de l'identifiant avant une liaison. Effectuez ce test sur le type déjà résolu, sinon un alias peut cacher l'occurrence. Décrivez avec vos mots la différence entre « type encore inconnu » et « type quelconque à chaque utilisation ». La distinction deviendra décisive au carnet 4. Si vous avancez vite, permutez l'ordre des contraintes du tableau et comparez les types finaux, plutôt que l'ordre ou la forme exacte des clés de la map. ## Avant de passer au carnet suivant Conservez votre tentative, un résultat prédit puis observé et une explication avec vos mots. Au carnet suivant, vous copierez votre propre code dans les cellules indiquées ; aucun module n'est importé implicitement d'un autre notebook. Vous pouvez reporter vos règles dans le squelette `mini-typeur` (`lib/`), puis utiliser ses tests de paliers : `mix test`, `mix test --include argent`, `mix test --include argent --include or`. Le squelette et les notebooks ont des noms de modules différents : adaptez les appels plutôt que de copier un fichier sans le relire. Ces carnets préparent le sujet Types du projet noté d’AP9, hors du rendu AP1–AP3. Le projet commence en semi-autonomie et se termine à la maison. Les supports restent des bases à affiner d’ici janvier ; le périmètre, le barème et l’échéance seront précisés avant le lancement. D’ici là, gardez vos essais dans `entrainement/`. Pour toute question : [aurelien.noce@minesparis.psl.eu](mailto:aurelien.noce@minesparis.psl.eu).