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