# Mini-typeur · Carnet 4 — Réutiliser une fonction à plusieurs types

## Notre question

Nous avons trouvé le type `fn(t0) -> t0` de la fonction identité. Peut-on l'utiliser
sur un nombre puis sur un booléen dans le même programme ? Nous allons distinguer
une inconnue partagée d'une variable quantifiée réinstanciée à chaque utilisation.

> **Repères.** [Slides 30 à 38](https://ap-2026.noce.fr/slides/AP9-typeur.html#30) : schémas, généralisation, instanciation. Elixir : `MapSet.difference/2`, une map de renommage construite avec `Enum.reduce/3`. 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
```

## Constater la limite du type partagé

Prédisez le résultat du programme et rappelez l'erreur de typage du carnet 3 :

```text
let id = fn(x) { x }
let n = id(1.0)
id(True)
```

L'exécution rend `True`. Mais notre ancien typeur partageait la même inconnue
entre les deux appels : le premier imposait `t0 = Float`, puis le second
`Float = Bool`. Il nous faut une règle autorisant certains types à être renouvelés.

Un *schéma de type* `∀a. fn(a) -> a` signifie que chaque utilisation peut choisir
un nouveau type pour `a`. Il est représenté par `{[0], {:fun, [{:var, 0}], {:var, 0}}}`.
La liste contient les identifiants quantifiés ; une liste vide reste monomorphe.
Les deux occurrences de `a` dans **une même instance** doivent rester identiques.

### Suivre les deux appels

| Moment | Type manipulé | Effet |
| --- | --- | --- |
| Définition de `id` | `fn(t0) -> t0` | `t0` est indépendant du contexte |
| Liaison `let` | `∀t0. fn(t0) -> t0` | généralisation |
| Premier usage | `fn(t1) -> t1` | instance neuve, puis `t1 = Float` |
| Second usage | `fn(t2) -> t2` | autre instance, puis `t2 = Bool` |

*Instancier* signifie remplacer seulement les variables quantifiées par des
inconnues neuves. Cela ne revient pas à changer le type de la fonction originale.

## Pourquoi ne pas tout généraliser ?

Considérez `fn(x) { let y = x let n = y(1.0) y(True) }`. `y` est un alias du
paramètre `x`. Les deux noms désignent une seule fonction passée par l'appelant.
Si l'on renouvelait son type à chaque usage, on accepterait sans justification
qu'un paramètre ordinaire soit utilisable à tous les types. Nous conservons donc
les paramètres **monomorphes**, même à travers un alias.

La généralisation ne quantifie que les inconnues libres du type qui ne sont
pas libres dans l'environnement :

```text
variables à quantifier = libres(type résolu) − libres(environnement résolu)
```

Pour un schéma, ses variables quantifiées ne sont pas libres. Exemple : si
l'environnement contient `x : t0` et que la valeur a le type `fn(t1) -> t0`,
on peut quantifier `t1`, mais pas `t0`.

### Le piège de l'environnement qui a changé de forme

Supposons que l'environnement contienne `f : t0` et que la substitution impose
`t0 = fn(Float) -> t1`. La variable libre pertinente est désormais `t1`.
Calculer les variables libres **avant** d'appliquer la substitution autoriserait
une généralisation incorrecte. Résolvez donc aussi les types de l'environnement,
en protégeant les variables déjà quantifiées de chaque schéma.

## Concevoir la généralisation et l'instanciation

> 💡 `MapSet.difference(left, right)` garde les éléments de `left` absents
> de `right`. `Enum.map(items, fn item -> ... end)` construit une liste en
> transformant chaque élément. Si chaque transformation consomme un compteur
> d'inconnues, transmettez aussi ce compteur, par récursion ou avec
> `Enum.map_reduce/3` ; des appels indépendants ne partageraient pas cet état.

Copiez **votre module `MiniTypes` du carnet 3**. Ajoutez deux fonctions publiques :

- `generalize(type, env, sub)` rend `{ids_quantifiés, type_résolu}`. Calculez les
  ensembles décrits plus haut ; triez les identifiants pour rendre les exemples
  faciles à lire.
- `instantiate({ids, type}, state)` rend `{type_neuf, nouvel_état}`. Réservez une
  inconnue neuve pour chaque identifiant quantifié, puis appliquez simultanément
  ce remplacement au type. Les inconnues non quantifiées restent partagées.

Modifiez ensuite deux règles du parcours : `let` généralise le type de sa valeur
**avant** de l'ajouter à l'environnement, tandis que la lecture d'un nom instancie
le schéma trouvé. Les paramètres des fonctions restent associés à `{[], type}`.

`MapSet.difference/2` exprime la différence d'ensembles. Pour résoudre le type
d'un schéma existant, retirez temporairement de la substitution ses identifiants
quantifiés (`Map.drop/2`) : ils sont liés localement par le schéma.

```elixir
# Copiez ici votre module MiniTypes du carnet 3.
# Ajoutez generalize/3 et instantiate/2.
# Modifiez les clauses visit/3 de name et let.
# Les paramètres de fn gardent des schémas {[], type}.
```

## Vérifier ce que l'on partage, et ce que l'on renouvelle

Énoncez pour chaque test la règle qu'il protège. Le dernier contre-exemple force
la résolution de l'environnement avant la généralisation ; un typeur acceptant
seulement l'exemple de `id` ne serait pas encore suffisant.

```elixir
a = {:var, 0}
b = {:var, 1}
Check.equal(MiniTypes.generalize({:fun, [b], a}, %{"x" => {[], a}}, %{}),
  {[1], {:fun, [b], a}})
Check.equal(MiniTypes.generalize(b, %{"f" => {[], a}}, %{0 => {:fun, [:float], b}}),
  {[], b})
Check.equal(MiniTypes.generalize(b, %{"id" => {[0], {:fun, [a], a}}}, %{0 => b}),
  {[1], b})
scheme = {[0], {:fun, [a], a}}
{first, state} = MiniTypes.instantiate(scheme, %{next: 10, sub: %{}})
{second, _state} = MiniTypes.instantiate(scheme, state)
Check.equal(first, {:fun, [{:var, 10}], {:var, 10}})
Check.equal(second, {:fun, [{:var, 11}], {:var, 11}})

identity = {:fn, ["x"], {:name, "x"}}
poly = {:let, "id", identity,
  {:let, "n", {:call, {:name, "id"}, [{:number, 1.0}]},
    {:call, {:name, "id"}, [{:bool, true}]}}}
Check.equal(MiniTypes.infer(poly), {:ok, :bool})
parameter = {:fn, ["f"],
  {:let, "n", {:call, {:name, "f"}, [{:number, 1.0}]},
    {:call, {:name, "f"}, [{:bool, true}]}}}
Check.error(MiniTypes.infer(parameter))
alias_parameter = {:fn, ["x"], {:let, "y", {:name, "x"},
  {:let, "n", {:call, {:name, "y"}, [{:number, 1.0}]},
    {:call, {:name, "y"}, [{:bool, true}]}}}}
Check.error(MiniTypes.infer(alias_parameter))
resolved_environment = {:fn, ["f"],
  {:let, "g", {:call, {:name, "f"}, [{:number, 1.0}]},
    {:let, "n", {:call, {:name, "g"}, [{:number, 1.0}]},
      {:call, {:name, "g"}, [{:bool, true}]}}}}
Check.error(MiniTypes.infer(resolved_environment))
Check.error(MiniTypes.infer({:fn, ["x"], {:call, {:name, "x"}, [{:name, "x"}]}}))
captured = {:fn, ["x"], {:let, "keep", {:fn, ["y"], {:name, "x"}},
  {:let, "n", {:call, {:name, "keep"}, [{:number, 1.0}]},
    {:call, {:name, "keep"}, [{:bool, true}]}}}}
{:ok, {:fun, [input], output}} = MiniTypes.infer(captured)
Check.equal(input, output)
```

## Indices et comparaison des trois moteurs

**Premier indice.** Pour les variables libres d'un schéma, calculez celles de
son type résolu puis retirez sa liste d'identifiants quantifiés. Réunissez les
ensembles obtenus pour tous les noms de l'environnement.

**Deuxième indice.** Pour instancier, construisez d'abord une map
`ancien_identifiant => nouvelle_inconnue` : toutes les occurrences du même
identifiant recevront ainsi le même remplacement.

**Troisième indice.** Le compteur d'inconnues est global au parcours. Un nouvel
identifiant ne doit pas entrer en collision avec une inconnue ou une variable
quantifiée déjà créée. Les tests d'instanciation partent de 10 pour rendre cette
condition visible ; le parcours normal maintient lui-même ce compteur.

Dans le README de votre projet, donnez un exemple accepté, un exemple refusé et une
trace de contraintes, puis comparez votre typeur à l'interpréteur d'AP2 et à la machine d'AP3. Expliquez pourquoi votre système accepte l'identité à deux
types mais refuse le paramètre `f` appliqué tantôt à un nombre, tantôt à un booléen.
Cette combinaison de contraintes, unification et polymorphisme de `let` constitue
le cœur du système Hindley–Milner étudié ici, sans surcharge ni sous-typage.

### Pour aller plus loin

Essayez `fn(x) { let keep = fn(y) { x } let a = keep(1.0) keep(True) }`.
Le paramètre ignoré `y` peut être généralisé ; le type de `x` doit rester partagé.
Construisez l'AST et expliquez le type final. Vous pouvez aussi enrichir les
messages d'erreur pour afficher la contrainte à l'origine du conflit.

## Avant de passer au carnet suivant

Conservez votre tentative, un résultat prédit puis observé et une explication
avec vos mots. Comparez enfin votre typeur à l'interpréteur et à la machine sur un même
programme, avec une trace et un contre-exemple.

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).