From 86109ea5434971e01a8625c0140db2af4fafc0b1 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Sat, 16 Dec 2023 19:05:17 +0100
Subject: Briefly mention the problem of let-bound polymorphism.

---
 transp-inf110-02-typage.tex | 84 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 84 insertions(+)

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
@@ -4989,6 +4990,89 @@ de types produits, sommes, $1$ et $0$ ($\rightarrow$ nvx cas d'échecs
 d'unification, p.ex., si $\zeta_1 = ({?} \rightarrow {?})$ et $\zeta_2
 = ({?} \times {?})$).
 
+\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}
-- 
cgit v1.2.3