diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 42 |
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 % |