Typing of call/cc.

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