diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 84 |
1 files changed, 84 insertions, 0 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 422ad34..d298f6b 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -1202,6 +1202,7 @@ et \end{frame} % \begin{frame} +\label{typing-vs-beta-reduction} \frametitle{Typage et $\beta$-réduction} On rappelle que la « $\beta$-réduction » désigne le remplacement en @@ -4991,4 +4992,87 @@ d'unification, p.ex., si $\zeta_1 = ({?} \rightarrow {?})$ et $\zeta_2 \end{frame} % +\begin{frame} +\frametitle{Types récursifs ?} + +\itempoint On a imposé lors de la résolution de la contrainte $\zeta_1 += \zeta_2$, lorsque $\zeta_1$ est une variable $\eta$, que $\zeta_2$ +ne fasse pas intervenir $\eta$. + +\medskip + +\itempoint Ceci sert à empêcher d'inférer un type p.ex. à $\lambda +x.xx$ (il fallait résoudre $\eta_1 = (\eta_1 \to \eta_2)$). De fait, +ce terme n'est pas typable dans le $\lambda$CST, sinon $(\lambda x.xx) +(\lambda x.xx)$ le serait, contredisant la normalisation forte du +$\lambda$CST. + +\medskip + +\itempoint On peut néanmoins étendre l'algorithme de H-M à de tels +\alert{types récursifs sans constructeur}, c'est ce que fait +\texttt{ocaml -rectypes} : + +{\tt +\$ ocaml -rectypes\\ +fun x -> x x ;;\\ +- : ('a -> 'b as 'a) -> 'b = <fun> +} + +\smallskip + +{\footnotesize (Ceci doit faire de OCaml un interpréteur du + $\lambda$-calcul \alert{non typé}, au moins pour une certaine + notion d'évaluation.)\par} + +\smallskip + +Mais c'est une mauvaise idée de s'en servir : mieux vaut définir un +type récursif explicite. + +\end{frame} +% +\begin{frame} +\frametitle{Le problème du polymorphisme du « let »} + +\itempoint Dans les langages fonctionnels, « \texttt{let $v$=$x$ in + $t$} » peut être vu comme un sucre syntaxique pour « \texttt{(fun $v + \mapsto t$)$x$} » (i.e., $(\lambda v.t)x$, +cf. transp. \ref{typing-vs-beta-reduction}). + +\medskip + +\itempoint Ceci pose un problème au typage à la H-M : mettons qu'on +veuille utiliser l'entier de Church $\overline{2} := \lambda fx +. f(fx)$, typé par H-M comme $(\alpha\to\alpha) \to +(\alpha\to\alpha)$, avec deux types $\alpha$ différents, par exemple +en OCaml : + +\smallskip + +{\footnotesize\tt +let twice = fun f -> fun x -> f(f x) in (twice ((+)1) 42, twice not true) ;;\\ +{\color{purple}- : int * bool = (44, true)}\\ +(fun twice -> (twice ((+)1) 42, twice not true))(fun f -> fun x -> f(f x)) ;;\\ +{\color{purple}\alert{Error}: This expression has type bool -> bool\\ + but an expression was expected of type int -> int\\ + Type bool is not compatible with type int} +\par} + +\smallskip + +{\footnotesize Dans l'expression \texttt{fun twice -> ...}, le type de + \texttt{twice} est fixé et ne peut pas être polymorphe.\par} + +\medskip + +\itempoint Pour réparer ce problème, très grossièrement : +\textcolor{blue}{(a)} on type d'abord $x$, puis +\textcolor{blue}{(b)} on « \alert{généralise} » chaque variable +(n'apparaissant pas dans le contexte d'ensemble), c'est-à-dire que +\textcolor{blue}{(c)} chaque apparition de $v$ dans $t$ reçoit des +variables de type différentes. + +\end{frame} +% \end{document} |