# AP9 — Approfondir les types de notre langage

## Choisir votre point de départ

Nous reprenons le langage et les AST d'AP3. Vous pouvez travailler sans lexer,
sans parser et sans nouveau projet Mix. L'objectif est de comprendre une brique
supplémentaire de votre typeur, puis de la vérifier sur des exemples choisis.

Voici des repères, que nous adapterons ensemble pendant la séance :

| Votre point de départ | La prochaine brique à explorer |
| --- | --- |
| Vous découvrez les types | [Règles](https://ap-2026.noce.fr/livebooks/typeur-01-regles.livemd), puis [unification](https://ap-2026.noce.fr/livebooks/typeur-02-unification.livemd). |
| Votre solveur fonctionne | [Fonctions](https://ap-2026.noce.fr/livebooks/typeur-03-fonctions.livemd), puis [polymorphisme](https://ap-2026.noce.fr/livebooks/typeur-04-polymorphisme.livemd). |
| Votre typeur traite le `let` polymorphe | Une extension ci-dessous, selon ce qui vous intéresse. |

Les [slides du typeur](https://ap-2026.noce.fr/slides/AP9-typeur.html) restent
notre référence. Ces supports sont une base préparatoire pour le projet noté
d’AP9, commencé en semi-autonomie puis terminé à la maison. Le périmètre, le
barème et l’échéance seront précisés avant le lancement en janvier.

Écrivez votre point de départ, la brique visée et un exemple que vous voulez
savoir traiter dans cette cellule de texte : …

## Consolider votre version

Si vous travaillez encore dans les carnets Types, terminez la brique choisie
avant de revenir ici. Un exemple accepté, un exemple refusé et une trace
expliquée suffisent à montrer où vous en êtes ; les extensions attendront.

Pour poursuivre dans ce carnet, copiez votre module `MiniTypes` dans la cellule
suivante. Chaque Livebook possède sa propre VM ; les modules ne circulent pas
automatiquement entre les notebooks. Nous utilisons `infer/1` sur des AST :
la fonction `check/1`, qui lit du texte, n'est pas requise.

```elixir
# Copiez ici votre module MiniTypes, puis modifiez cette même cellule.
```

Les cellules suivantes sont des contrats à vérifier après la reprise des
fonctions et du polymorphisme. Ne lancez pas les vérifications d'une extension
que vous n'avez pas choisie ; utilisez-les pour prévoir son comportement.

```elixir
import ExUnit.Assertions
assert MiniTypes.infer({:binary, :plus, {:number, 1.0}, {:number, 2.0}}) == {:ok, :float}
assert {:error, _} = MiniTypes.infer({:binary, :plus, {:bool, true}, {:number, 2.0}})
```

```elixir
identity = {:fn, ["x"], {:name, "x"}}
{:ok, {:fun, [input], output}} = MiniTypes.infer(identity)
assert input == output
program = {:let, "id", identity,
  {:let, "n", {:call, {:name, "id"}, [{:number, 1.0}]},
    {:call, {:name, "id"}, [{:bool, true}]}}}
assert MiniTypes.infer(program) == {:ok, :bool}
```

Expliquez pourquoi les deux appels de `id` peuvent utiliser des types différents.
Que changerait le fait de recevoir `id` comme paramètre d'une fonction ?
Reprenez le contre-exemple du notebook Types 04 au besoin.

## Extension A — Des paires

Une paire contient deux valeurs, qui peuvent avoir des types différents.
Nous ajoutons l'AST `{:pair, gauche, droite}` et le type `{:pair, type_gauche,
type_droite}`. La première forme contient des expressions ; la seconde contient
des types. Nous n'ajoutons aucune syntaxe au lexer ou au parser.

Avant de coder, listez les fonctions qui doivent parcourir une paire. Comment
appliquer une substitution à ses deux composants ? Où chercher les inconnues
libres ? Quelles contraintes naissent de l'égalité entre deux types paires ?

Ajoutez vos clauses aux fonctions existantes. Transmettez la substitution
produite par le premier composant au traitement du second. Une paire et un
flottant sont incompatibles. L'affichage de types avec `format/1` peut attendre.

```elixir
pair = {:pair, {:number, 1.0}, {:bool, true}}
assert MiniTypes.infer(pair) == {:ok, {:pair, :float, :bool}}
a = {:var, 0}
assert MiniTypes.resolve({:pair, a, :bool}, %{0 => :float}) == {:pair, :float, :bool}
assert MiniTypes.free({:pair, a, a}) == MapSet.new([0])
```

```elixir
a = {:var, 0}
{:ok, sub} = MiniTypes.unify({:pair, a, a}, {:pair, :float, :float})
assert MiniTypes.resolve(a, sub) == :float
assert {:error, _} = MiniTypes.unify({:pair, a, a}, {:pair, :float, :bool})
assert {:error, _} = MiniTypes.unify(a, {:pair, a, :float})
assert {:error, _} = MiniTypes.unify({:pair, :float, :bool}, :float)
```

> 💡 Le dernier parcours de `free/1` sert aussi au contrôle d'occurrence.
> Une nouvelle forme oubliée peut autoriser un type qui se contient lui-même.
> Pour généraliser puis instancier une paire, réutilisez les mécanismes d'AP3 :
> vérifiez simplement qu'ils traversent bien cette nouvelle forme.

Proposez un `let` polymorphe dont le type contient une paire, et vérifiez deux
usages différents. Gardez cet exemple et la contrainte qui explique son résultat.

## Extension B — Des projections (après les paires)

Ajoutons `{:first, expression}` et `{:second, expression}`. La première projection
renvoie le type du premier composant, la seconde celui du second. L'expression
peut être un nom ou un appel ; elle n'est pas nécessairement un nœud paire littéral.

Pour `fn(p) { first(p) }`, dessinons la contrainte : le type de `p` doit être
une paire de deux inconnues fraîches, et le résultat doit garder le type du
premier composant. Écrivez cette règle avant vos clauses, puis utilisez votre
unification existante. Nous ne programmons pas d'évaluateur dans ce notebook.

```elixir
pair = {:pair, {:number, 1.0}, {:bool, true}}
assert MiniTypes.infer({:first, pair}) == {:ok, :float}
assert MiniTypes.infer({:second, pair}) == {:ok, :bool}
assert {:error, _} = MiniTypes.infer({:first, {:number, 1.0}})
project = {:fn, ["p"], {:first, {:name, "p"}}}
{:ok, {:fun, [{:pair, left, right}], result}} = MiniTypes.infer(project)
assert result == left
assert left != right
```

Ajoutez un test où la projection reçoit le résultat d'un appel. Que perdrait
une implémentation qui ne reconnaîtrait que la syntaxe `{:pair, ...}` ?

## Extension C — Localiser un refus (indépendante des paires)

Notre erreur indique des types incompatibles, mais pas l'endroit concerné.
Ajoutez une entrée `MiniTypes.infer_at/1` qui garde le succès `{:ok, type}` et
renvoie `{:error, %{reason: raison, path: chemin}}` en cas de refus.

Le chemin part de la racine : `[]` désigne le nœud courant, `[:left]` son fils
gauche, `[:right]` son fils droit et `[:body]` le corps d'un `let`. Pour commencer,
limitez-vous aux nombres, booléens, noms, opérations binaires et `let` ;
documentez cette limite plutôt que d'étendre toutes les formes d'un coup.

Une incompatibilité porte le chemin du nœud qui impose la contrainte ; un nom
absent porte celui du nœud `name`. Une erreur enfant conserve son chemin en
remontant. Aucun numéro de ligne n'est disponible dans nos AST actuels.

```elixir
bad_sum = {:binary, :plus, {:bool, true}, {:number, 2.0}}
assert {:error, %{path: [], reason: _}} = MiniTypes.infer_at(bad_sum)
nested = {:binary, :plus, {:number, 1.0}, bad_sum}
assert {:error, %{path: [:right], reason: _}} = MiniTypes.infer_at(nested)
missing = {:let, "x", {:number, 1.0},
  {:binary, :plus, {:name, "x"}, {:name, "absent"}}}
assert {:error, %{path: [:body, :right], reason: {:undefined_name, "absent"}}} =
  MiniTypes.infer_at(missing)
```

Réutilisez les règles de votre visiteur : la nouveauté est l'information de
localisation qu'il transporte. Ajoutez un cas réussi et un cas d'erreur à gauche.
Comment garderiez-vous une position dans le texte si nous revenions au parser ?

## Préparer notre échange

Conservez la brique terminée avant de poursuivre une autre extension. Notez ce
qui fonctionne, ce qui reste à écrire et les cellules à exécuter pour le vérifier.
Sauvegardez votre carnet et committez les petites étapes fonctionnelles.

À l'oral, montrez un résultat prédit puis observé, une contrainte qui le justifie
et un contre-exemple. Ces traces vous aideront à poursuivre le projet à la maison ;
les attendus définitifs seront précisés avant AP9.
Pour toute question : [aurelien.noce@minesparis.psl.eu](mailto:aurelien.noce@minesparis.psl.eu).