From 29389e09bc8c7d5c2dc28d3f8476ca042be1d1fa Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Tue, 23 Jan 2024 23:02:55 +0100
Subject: An exercise on Hindley-Milner type inference.

---
 exercices-inf110.tex | 105 +++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 105 insertions(+)

diff --git a/exercices-inf110.tex b/exercices-inf110.tex
index 0539356..af9a1a7 100644
--- a/exercices-inf110.tex
+++ b/exercices-inf110.tex
@@ -2591,6 +2591,111 @@ on ne peut pas prouver $\neg C$ seul, ni $\neg\neg C$ seul, qui peut
 prendre l'une ou l'autre valeur de vérité).
 \end{corrige}
 
+%
+
+\exercice\ (${\star}{\star}$)\par\nobreak
+
+En appliquant l'algorithme de Hindley-Milner, trouver une annotation
+de type (dans le $\lambda$-calcul simplement typé) au terme suivant du
+$\lambda$-calcul non typé :
+\[
+\lambda k. \, k\,(k\,(\lambda x.x)\,(\lambda y.y))
+\]
+(autrement dit, \texttt{fun k -> k (k (fun x -> x) (fun y -> y))} en
+syntaxe OCaml).
+
+\begin{corrige}
+On prend bien garde au fait qu'il faut parenthéser comme $\lambda
+k. \, k\,((k\,(\lambda x.x))\,(\lambda y.y))$.
+
+Dans une première phase, on collecte les types et contraintes
+suivants : $k:\eta_1$, $x:\eta_2$ donc $\lambda x.x:\eta_2\to\eta_2$,
+puis $k(\lambda x.x):\eta_3$ avec $\eta_1 =
+((\eta_2\to\eta_2)\to\eta_3)$, puis $y:\eta_4$ donc $\lambda
+y.y:\eta_4\to\eta_4$, puis $k(\lambda x.x)(\lambda y.y):\eta_5$ avec
+$\eta_3 = ((\eta_4\to\eta_4)\to\eta_5)$, puis $k(k(\lambda
+x.x)(\lambda y.y)) : \eta_6$ avec $\eta_1 = (\eta_5\to\eta_6)$ ; et le
+type final est $\eta_1 \to \eta_6$.  On a donc les contraintes
+suivantes :
+\[
+\begin{aligned}
+\eta_1 &= ((\eta_2\to\eta_2)\to\eta_3)\\
+\eta_3 &= ((\eta_4\to\eta_4)\to\eta_5)\\
+\eta_1 &= (\eta_5\to\eta_6)\\
+\end{aligned}
+\]
+On examine d'abord la contrainte $\eta_1 =
+((\eta_2\to\eta_2)\to\eta_3)$ : ici, $\eta_1$ est une variable de
+type, et elle n'apparaît pas dans l'autre membre de la contrainte ; il
+n'y a rien à faire à part enregistrer $\eta_1 \mapsto
+((\eta_2\to\eta_2)\to\eta_3)$ dans la substitution et l'appliquer aux
+contraintes qui deviennent donc :
+\[
+\begin{aligned}
+\eta_3 &= ((\eta_4\to\eta_4)\to\eta_5)\\
+((\eta_2\to\eta_2)\to\eta_3) &= (\eta_5\to\eta_6)\\
+\end{aligned}
+\]
+On examine ensuite la contrainte $\eta_3 =
+((\eta_4\to\eta_4)\to\eta_5)$ : de nouveau, $\eta_3$ est une variable
+de type, et elle n'apparaît pas dans l'autre membre de la contrainte :
+on enregistre $\eta_3 \mapsto ((\eta_4\to\eta_4)\to\eta_5)$ et on
+l'applique à la substitution déjà enregistrée qui devient donc $\eta_1
+\mapsto ((\eta_2\to\eta_2)\to(\eta_4\to\eta_4)\to\eta_5)$, ainsi qu'à
+la contrainte restante.  Cette dernière contrainte à examiner est :
+\[
+((\eta_2\to\eta_2)\to(\eta_4\to\eta_4)\to\eta_5) = (\eta_5\to\eta_6)
+\]
+Cette fois-ci les deux membres sont des types complexes, donc elle se
+transforme en deux contraintes (attention au parenthésage !) :
+\[
+\begin{aligned}
+(\eta_2\to\eta_2) &= \eta_5\\
+((\eta_4\to\eta_4)\to\eta_5) &= \eta_6\\
+\end{aligned}
+\]
+On examine à présent $(\eta_2\to\eta_2) = \eta_5$ : ici, $\eta_5$ est
+une variable de type, et elle n'apparaît pas dans l'autre membre de la
+contrainte : on enregistre $\eta_5 \mapsto (\eta_2\to\eta_2)$, et on
+applique cette substitution à ce qui reste de contrainte (qui devient
+donc $((\eta_4\to\eta_4)\to\eta_2\to\eta_2) = \eta_6$) et à ce qu'on a
+déjà déterminé comme substitution (qui devient donc $\eta_1 \mapsto
+((\eta_2\to\eta_2)\to(\eta_4\to\eta_4)\to\eta_2\to\eta_2)$ et $\eta_3
+\mapsto ((\eta_4\to\eta_4)\to\eta_2\to\eta_2)$).  Il reste enfin la
+contrainte $((\eta_4\to\eta_4)\to\eta_2\to\eta_2) = \eta_6$ : de
+nouveau, $\eta_6$ est une variable de type, et elle n'apparaît pas
+dans l'autre membre de la contrainte : on enregistre donc $\eta_6
+\mapsto ((\eta_4\to\eta_4)\to\eta_2\to\eta_2)$, et on a trouvé la
+substitution finale :
+\[
+\begin{aligned}
+\eta_1 &\mapsto ((\eta_2\to\eta_2)\to(\eta_4\to\eta_4)\to\eta_2\to\eta_2)\\
+\eta_3 &\mapsto ((\eta_4\to\eta_4)\to\eta_2\to\eta_2)\\
+\eta_5 &\mapsto (\eta_2\to\eta_2)\\
+\eta_6 &\mapsto ((\eta_4\to\eta_4)\to\eta_2\to\eta_2)\\
+\end{aligned}
+\]
+Il ne reste plus qu'à l'appliquer à tous les types intermédiaires et
+au type final, ce qui donne
+\[
+\begin{aligned}
+&\lambda (k:(\eta_2\to\eta_2)\to(\eta_4\to\eta_4)\to\eta_2\to\eta_2). \, k\,(k\,(\lambda (x:\eta_2).x)\,(\lambda (y:\eta_4).y))\\
+:\quad& ((\eta_2\to\eta_2)\to(\eta_4\to\eta_4)\to\eta_2\to\eta_2)
+\to (\eta_4\to\eta_4)\to\eta_2\to\eta_2
+\end{aligned}
+\]
+ou, si on veut renommer les variables restantes pour être un peu plus
+lisible
+\[
+\begin{aligned}
+&\lambda (k:(\alpha\to\alpha)\to(\beta\to\beta)\to\alpha\to\alpha). \, k\,(k\,(\lambda (x:\alpha).x)\,(\lambda (y:\beta).y))\\
+:\quad& ((\alpha\to\alpha)\to(\beta\to\beta)\to\alpha\to\alpha)
+\to (\beta\to\beta)\to\alpha\to\alpha
+\end{aligned}
+\]
+comme $\lambda$-terme annoté et comme type final.
+\end{corrige}
+
 
 %
 %
-- 
cgit v1.2.3