summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorDavid A. Madore <david+git@madore.org>2023-12-16 19:40:22 +0100
committerDavid A. Madore <david+git@madore.org>2023-12-16 19:40:22 +0100
commit3a33c1cfd1dbf1fbe00861a8ea960c3b77e82290 (patch)
treeed3ee83ec7afd178a0e93c8f3e19877b7627d183
parent86109ea5434971e01a8625c0140db2af4fafc0b1 (diff)
downloadinf110-lfi-3a33c1cfd1dbf1fbe00861a8ea960c3b77e82290.tar.gz
inf110-lfi-3a33c1cfd1dbf1fbe00861a8ea960c3b77e82290.tar.bz2
inf110-lfi-3a33c1cfd1dbf1fbe00861a8ea960c3b77e82290.zip
Say something about the value restriction.
-rw-r--r--transp-inf110-02-typage.tex40
1 files changed, 37 insertions, 3 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index d298f6b..288863d 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -5068,10 +5068,44 @@ let twice = fun f -> fun x -> f(f x) in (twice ((+)1) 42, twice not true) ;;\\
\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}{(b)} on « \alert{généralise} » chaque variable de
+type (non présente 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.
+variables de type fraîches à ces places (ce qui le rend polymorphe).
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{La « restriction de valeur »}
+
+\itempoint La solution trouvée pour rendre \texttt{let} polymorphe
+(transp. précédent) apporte ses propres difficultés quand le langage
+permet les effets de bord (variables mutables) : considérons
+l'expression OCaml :
+
+\smallskip
+
+{\tt let r = ref (fun x -> x) in r := (fun x -> x+1) ; (!r) true ;;}
+
+\smallskip
+
+Ici, \alert{on ne veut pas} généraliser \texttt{r} à pouvoir servir à
+la fois comme \texttt{(int -> int) ref} et comme \texttt{(bool ->
+ bool) ref} car le code précédent causerait l'appel d'une fonction
+\texttt{int -> int} sur une valeur de type \texttt{bool} (crash
+potentiel !).
+
+\bigskip
+
+\itempoint La solution dans un langage comme OCaml est la
+« restriction de valeur » : le $v$ dans « \texttt{let $v$=$x$ in
+ $t$} » n'est rendu polymorphe (i.e., n'est « généralisé ») que
+lorsque $x$ est une « valeur statique » déterminable à la compilation.
+
+\bigskip
+
+\itempoint Dans un langage comme Haskell, le problème ne se pose pas,
+car toutes les fonctions et valeurs sont pures.
\end{frame}
%