diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 63 |
1 files changed, 58 insertions, 5 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 653b8bb..d27fac7 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -4827,35 +4827,54 @@ il renvoie un type et modifie $\Gamma,\mathscr{C}$ : {\footnotesize\itempoint Ceci s'adapte sans difficulté au cas où on dispose d'annotations de type partielles.\par} +\medskip + +\itempoint Le typage final s'obtiendra en appliquant la substitution +trouvée dans la deuxième phase. + \end{frame} % \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 +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 +\medskip \itempoint Soit le terme à typer $\lambda fx.f(\lambda g.gx)$. On -collecte successivement les types et contraintes suivants :\quad +collecte 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 +\medskip \itempoint Soit le terme à typer $\lambda x.xx$. On collecte -successivement les types et contraintes suivants :\quad +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$. +\medskip + +\itempoint Soit le terme à typer $t := (\lambda xy.x) (\lambda +x'y'.x')$. On collecte les types et contraintes suivants :\quad +$x:\eta_1$,\quad $y:\eta_2$,\quad $x':\eta_3$,\quad $y':\eta_4$\quad +enfin $t:\eta_5$ avec $(\eta_1 \to \eta_2 \to \eta_1) = ((\eta_3 \to +\eta_4 \to \eta_3) \to \eta_5)$. + +\smallskip + +{\footnotesize \textcolor{orange}{Attention :} ce terme aurait pu être + écrit $(\lambda xy.x) (\lambda xy.x)$ : les deux $x$ \alert{ne sont + pas le même} !\par} + \end{frame} % \begin{frame} @@ -4892,4 +4911,38 @@ reste des contraintes : \end{frame} % +\begin{frame} +\frametitle{Résolution des contraintes : exemple} + +Reprenons l'exemple $t := (\lambda xy.x) (\lambda x'y'.x')$. La +première phase a donné : $x:\eta_1$, $y:\eta_2$, $x':\eta_3$, +$y':\eta_4$ et le type final $\eta_5$ avec la constrainte $(\eta_1 \to +\eta_2 \to \eta_1) = ((\eta_3 \to \eta_4 \to \eta_3) \to \eta_5)$. + +\smallskip + +\begin{itemize} +\item On examine la seule contrainte $(\eta_1 \to \eta_2 \to \eta_1) = + ((\eta_3 \to \eta_4 \to \eta_3) \to \eta_5)$ : ceci retire cette + contrainte et on rajoute $\eta_1 = (\eta_3 \to \eta_4 \to \eta_3)$ + et $(\eta_2 \to \eta_1) = \eta_5$. +\item On examine $\eta_1 = (\eta_3 \to \eta_4 \to \eta_3)$ : comme + $\eta_1$ est une variable, et n'apparaît pas à droite, on enregistre + la substitution $\eta_1 \mapsto (\eta_3 \to \eta_4 \to \eta_3)$ et + on l'applique à la contrainte restante qui devient $(\eta_2 \to + \eta_3 \to \eta_4 \to \eta_3) = \eta_5$. +\item Comme $\eta_5$ est une variable et n'apparaît pas à gauche, on + enregistre la substitution $\eta_5 \mapsto (\eta_2 \to \eta_3 \to + \eta_4 \to \eta_3)$ et il ne reste plus de contrainte. +\end{itemize} + +\medskip + +Finalement, on a typé : $\vdash (\lambda (x:\eta_3 \to \eta_4 \to +\eta_3).\,\lambda(y:\eta_2).\,x) \; (\lambda +(x':\eta_3).\,\lambda(y':\eta_4).\,x') \; : \penalty-1000\; \eta_2 \to +\eta_3 \to \eta_4 \to \eta_3$. + +\end{frame} +% \end{document} |