diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 129 |
1 files changed, 128 insertions, 1 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index e075e92..2776a21 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -3296,7 +3296,8 @@ prend en argument une fonction $g$ et \begin{itemize} \item\alert{capture} sa propre continuation (= celle du retour du call/cc), -\item\alert{passe} celle-ci en argument de la fonction $g$. +\item\alert{passe} celle-ci en argument de la fonction $g$, et renvoie + soit la valeur de retour de $g$ soit celle passée à la continuation. \end{itemize} \medskip @@ -3345,6 +3346,132 @@ $\rightarrow$ 84 \end{frame} % +\begin{frame} +\frametitle{Quel est le type de call/cc ?} + +\itempoint\alert{Une continuation ne retourne jamais}. On peut donc +la typer comme $\alpha \to \bot$ ou bien $\alpha \to \beta$ avec +$\beta$ un type arbitraire. + +\medskip + +\itempoint La fonction $g$ passée au call/cc doit renvoyer le même +type $\alpha$ qu'accepte la continuation qu'on lui a passée : donc +$(\alpha\to\beta)\to\alpha$. + +\medskip + +\itempoint La fonction call/cc elle-même renvoie ce même type +$\alpha$ : donc elle a pour type +$((\alpha\to\beta)\to\alpha)\to\alpha$. + +\medskip + +\itempoint C'est le type correspondant à la \textbf{loi de Peirce} +$((A\Rightarrow B)\Rightarrow A)\Rightarrow A$, une des formulations +de la \alert{logique classique}. + +\medskip + +\textcolor{blue}{\textbf{Moralité :}} la présence du call/cc +transforme la logique du typage de logique intuitionniste en logique +classique. + +\medskip + +{\footnotesize Ceci est dit de façon informelle, mais on peut + introduire une variante du $\lambda$-calcul, le $\lambda\mu$-calcul, + qui rend précise cette idée. Le $\lambda\mu$-calcul simplement typé + garantit encore la terminaison des programmes : on ne peut pas faire + de boucles avec le seul call/cc \emph{bien typé}.\par} + +\end{frame} +% +\begin{frame} +\frametitle{Oui mais il y a de la triche !} + +{\footnotesize Le tiers exclu $A \lor \neg A$ dit moralement « soit je + te donne une valeur de type $\alpha$ soit je te donne une promesse + qu'il n'en existe pas (type $\alpha\to 0$) ». En $\lambda$CST on ne + peut pas faire ça !} + +\bigskip + +Regardons comment le call/cc permet d'implémenter le tiers exclu $A +\lor \neg A$ : +\[ +\texttt{callcc}\; +\bigg(\lambda (k:(\alpha+(\alpha\to 0))\to 0).\;\iota^{(\alpha,\alpha\to 0)}_2\Big(\lambda (v:\alpha).\,k(\iota^{(\alpha,\alpha\to 0)}_1 v)\Big)\bigg) +\] +\[ +\text{a pour type~:~}\quad +\alpha + (\alpha\to 0) +\] + +{\footnotesize La fonction en argument du call/cc est a pour type + $((\alpha + (\alpha\to 0)) \to 0) \to (\alpha + (\alpha\to 0))$, + c'est-à-dire qu'elle correspond à une preuve de $(\neg (A\lor\neg + A)) \Rightarrow (A\lor\neg A)$ (intuitionist\textsuperscript{t} + valable).\par} + +\bigskip + +Que fait ce code ? +\begin{itemize} +\item il renvoie \alert{provisoirement} $\iota_2^{(\alpha,\alpha\to + 0)}(\cdots)$, où $(\cdots)$ définit une promesse qu'il n'y a pas de + valeur de type $\alpha$, +\item si on invoque cette promesse (avec une valeur $v$ de type + $\alpha$, donc !), il utilise la continuation $k$ pour « revenir + dans le temps » et changer d'avis et renvoie finalement + $\iota_1^{(\alpha,\alpha\to 0)}(v)$. +\end{itemize} + +\end{frame} +% +\begin{frame} +\frametitle{Oui mais il y a de la triche : quelle est la morale ?} + +{\footnotesize + +En SML/NJ : + +{\tt +val callcc = fn g => SMLofNJ.Cont.callcc (fn k => g (fn v => SMLofNJ.Cont.throw k v))\\ +datatype ('a,'b) sum = Inj1 of 'a | Inj2 of 'b\\ +val exclmiddle = callcc (fn k => Inj2 (fn v => k (Inj1 v))) +;; +} + +\par} + +\medskip + +\centerline{*} + +\textcolor{blue}{\textbf{Moralité :}} + +\medskip + +\itempoint Il est facile de tenir ses promesses quand on peut voyager +dans le temps avec l'aide de call/cc. + +\medskip + +\itempoint Le call/cc change la logique du typage en logique +classique, mais l'intérêt des types somme est grandement diminué : les +valeurs ne sont pas stables. + +\medskip + +\itempoint La logique classique n'a pas la propriété de la +disjonction : on a $\vdash A\lor \neg A$ en logique classique, mais ni +$\vdash A$ ni $\vdash \neg A$ (pour $A$ opaque). Elle n'est pas +constructive. On peut lui appliquer Curry-Howard, mais c'est moins +intéressant. + +\end{frame} +% % TODO: % - Kripke % - CPS et fragment négatif |