From 9c16b52c71af649970a98341fc2efb2b3fcaa291 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Thu, 14 Dec 2023 22:10:45 +0100
Subject: Barely start writing about Hindley-Milner.

---
 transp-inf110-02-typage.tex | 42 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 42 insertions(+)

(limited to 'transp-inf110-02-typage.tex')

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
@@ -4693,6 +4693,48 @@ pour le calcul propositionnel intuitionniste.
   A\lor\neg\neg A)$ (Scott) sont Medvedev-valides mais non
   démontrables.\par}
 
+\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:
-- 
cgit v1.2.3