Barely start writing about Hindley-Milner.

1 files changed, 42 insertions, 0 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 6acf11d..d0347c4 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -4695,6 +4695,48 @@ pour le calcul propositionnel intuitionniste.
 
 \end{frame}
 %
+\section{Inférence de type à la Hindley-Milner}
+\begin{frame}
+\frametitle{L'algorithme de Hindley-Milner : description sommaire}
+
+{\footnotesize Rappel : le $\lambda$-calcul simplement typé
+  ($\lambda$CST), pour nous, porte \emph{toutes} les annotations de
+  type.\par}
+
+\medskip
+
+\itempoint Donné un type du $\lambda$CST, on appelle
+\textbf{désannotation} de celui-ci le type du $\lambda$-calcul non
+typé obtenu en retirant toutes les annotations de type : p.ex.
+\[
+\lambda(x:\alpha).\,
+\lambda(f:((\alpha\to\beta)\to\beta)\to\gamma).\,
+f(\lambda(h:\alpha\to\beta).hx)
+\]
+de type $\alpha \to ((\alpha\to\beta)\to\beta)\to\gamma \to \gamma$ se
+désannote en $\lambda xf.\, f(\lambda .hx)$.
+
+\medskip
+
+\itempoint L'\textbf{inférence de type} pour le $\lambda$CST est le
+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 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$).
+\end{itemize}
+
+\medskip
+
+\itempoint L'\textbf{algorithme de Hindley-Milner} (ou Damas-Milner,
+car Damas a prouvé sa correction) ou \textbf{algorithme W} (ou
+\textbf{J}, c'est quasi pareil) accomplit ces buts.
+
+\end{frame}
+%
 % TODO:
 % - inférence de type de Hindley-Milner
 %