Start describing the Hindley-Milner algorithm.

1 files changed, 113 insertions, 4 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 8479808..b0d3028 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -1043,6 +1043,7 @@ vaut encore après tout renommage des variables libres.
 \end{frame}
 %
 \begin{frame}
+\label{constructing-the-typing-derivation}
 \frametitle{Construction de la dérivation}
 
 La dérivation du jugement de typage $\Gamma \vdash M : \sigma$ d'un
@@ -4712,7 +4713,7 @@ pour le calcul propositionnel intuitionniste.
   ($\lambda$CST), pour nous, porte \emph{toutes} les annotations de
   type.\par}
 
-\medskip
+\smallskip
 
 \itempoint Donné un type du $\lambda$CST, on appelle
 \textbf{désannotation} de celui-ci le type du $\lambda$-calcul non
@@ -4732,7 +4733,7 @@ problème, donné un terme du $\lambda$-calcul non typé, de :
 \begin{itemize}
 \item décider s'il est typable, i.e., est la désannotation d'un terme
   du $\lambda$CST,
-\item si oui, retrouver son type et toutes les annotations,
+\item si oui, retrouver son type et toutes les annotations, et même
 \item trouver la solution la « plus générale » possible (p.ex.,
   $\lambda x.x$ doit retrouver $\lambda(x:\alpha).x$ et pas
   $\lambda(x:\alpha\to\beta).x$).
@@ -4744,9 +4745,117 @@ problème, donné un terme du $\lambda$-calcul non typé, de :
 car Damas a prouvé sa correction) ou \textbf{algorithme W} (ou
 \textbf{J}, c'est quasi pareil) accomplit ces buts.
 
+\medskip
+
+\itempoint On fait ainsi des « types opaques » du $\lambda$CST un vrai
+polymorphisme.
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{L'algorithme de Hindley-Milner : esquisse}
+
+L'algorithme de Hindley-Milner procède en deux phases :
+
+\medskip
+
+\itempoint\textbf{Première phase : collection des contraintes} :
+donnée un terme à typer, on \alert{alloue une variable de type}
+fraîches à chaque nouvelle variable introduite ou application et on
+\alert{enregistre une contrainte} (équation) à chaque application.
+Cette phase n'échoue pas.
+
+\smallskip
+
+{\footnotesize P.ex.: sur $\lambda x.\lambda y.xy$, on va enregistrer
+  successivement les types $x:\eta_1$,\quad $y:\eta_2$,\quad
+  $xy:\eta_3$ et la contrainte $\eta_1 = (\eta_2\to\eta_3)$, et
+  renvoyer $\eta_1 \to \eta_2 \to \eta_3$.\par}
+
+\medskip
+
+\itempoint\textbf{Deuxième phase : résolution des contraintes par
+  unification} : on cherche une « substitution » des variables de type
+qui résout toutes les contraintes.
+
+\smallskip
+
+Pour ça, on prend de façon répétée une équation $\zeta_1 = \zeta_2$ du
+jeu de contraintes et on cherche à la satisfaire : si $\zeta_1$ ou
+$\zeta_2$ est une variable, c'est facile, sinon, on \alert{décompose}
+chacune ($\zeta_i = (\xi_i \to \chi_i)$) en produisant de nouvelles
+contraintes ($\xi_1=\xi_2$ et $\chi_1=\chi_2$).  \alert{Cette phase
+  peut échouer.}
+
+\medskip
+
+\itempoint L'algorithme termine, donne une solution s'il en existe
+une, et même la « \textbf{solution principale} » dont toutes les
+autres se dérivent par substitution.
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Collection des contraintes}
+
+La première phase de l'algorithme de H-M fonctionne comme la
+vérification de type du $\lambda$CST
+(transp. \ref{constructing-the-typing-derivation}) mais en
+introduisant des variables de type « fraîches » au vol et en
+collectant des contraintes au fur et à mesure.
+
+\medskip
+
+Soit $t$ le terme à typer : l'algo est écrit ici en style impératif et
+opère sur un contexte $\Gamma$ et un jeu de contraintes $\mathscr{C}$,
+il renvoie un type et modifie $\Gamma,\mathscr{C}$ :
+\begin{itemize}
+\item si $t = v$ est une variable, elle doit être dans le
+  contexte : renvoyer son type ;
+\item si $t = \lambda v.e$ est une abstraction, allouer une nouvelle
+  variable de type $\eta$, ajouter $v:\eta$ au contexte, appliquer
+  l'algorithme récursivement à $e$, qui donne $\zeta$, et renvoyer
+  $\eta \to \zeta$ ;
+\item si $t = fx$ est une application, appliquer l'algorithme
+  récursivement à $f$ et $x$, qui donne $\zeta$ et $\xi$, allouer une
+  nouvelle variable de type $\eta$, ajouter l'équation $\zeta =
+  (\xi\to\eta)$ aux contraintes et renvoyer $\eta$.
+\end{itemize}
+
+\medskip
+
+{\footnotesize\itempoint Ceci s'adapte sans difficulté au cas où on
+  dispose d'annotations de type partielles.\par}
+
 \end{frame}
 %
-% TODO:
-% - inférence de type de Hindley-Milner
+\begin{frame}
+\frametitle{Collection des contraintes : exemples}
+
+\itempoint Soit le terme à typer $\lambda xyz.xz(yz)$.  On collecte
+successivement les types et contraintes suivants :\quad
+$x:\eta_1$,\quad $y:\eta_2$,\quad $z:\eta_3$,\quad $xz:\eta_4$ avec
+$\eta_1 = (\eta_3\to\eta_4)$,\quad $yz:\eta_5$ avec $\eta_2 =
+(\eta_3\to\eta_5)$,\quad $xz(yz):\eta_6$ avec $\eta_4 =
+(\eta_5\to\eta_6)$,\quad et on renvoie finalement le type $\eta_1 \to
+\eta_2 \to \eta_3 \to \eta_6$.
+
+\bigskip
+
+\itempoint Soit le terme à typer $\lambda fx.f(\lambda g.gx)$.  On
+collecte successivement les types et contraintes suivants :\quad
+$f:\eta_1$,\quad $x:\eta_2$,\quad $g:\eta_3$,\quad $gx:\eta_4$ avec
+$\eta_3 = (\eta_2\to\eta_4)$,\quad $f(\lambda g.gx):\eta_5$ avec
+$\eta_1 = ((\eta_3\to\eta_4) \to \eta_5)$,\quad et on renvoie
+finalement le type $\eta_1 \to \eta_2 \to \eta_5$.
+
+\bigskip
+
+\itempoint Soit le terme à typer $\lambda x.xx$.  On collecte
+successivement les types et contraintes suivants :\quad
+$x:\eta_1$,\quad $xx:\eta_2$ avec $\eta_1 = (\eta_1 \to \eta_2)$,\quad
+et on renvoie finalement le type $\eta_1 \to \eta_2$.
+
+\end{frame}
 %
 \end{document}