From 9c16b52c71af649970a98341fc2efb2b3fcaa291 Mon Sep 17 00:00:00 2001 From: "David A. Madore" 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(+) 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