From 6c1a67ff774a704a6fd936a4cad1d8cb015a63eb Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Tue, 12 Dec 2023 18:21:59 +0100
Subject: A brief description of continuations and call/cc.

---
 transp-inf110-02-typage.tex | 113 +++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 111 insertions(+), 2 deletions(-)

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index fef2c93..e075e92 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -3233,12 +3233,121 @@ $\mathsf{K}y$.
   les seules fonctions $\mathsf{S}$, $\mathsf{K}$, $\mathsf{I}$.
   {\tiny(Mais personne ne serait assez fou pour faire ça.)}\par}
 
+\end{frame}
+%
+\section{Le call/cc et la logique classique}
+\begin{frame}
+\frametitle{Qu'est-ce qu'une continuation ?}
+
+\itempoint Dans un langage de programmation, la \textbf{continuation}
+de l'appel d'une fonction $f$ est « l'état de la machine qui attend
+que $f$ renvoie une valeur ».
+
+\medskip
+
+On peut y penser comme (une copie de) la \alert{pile d'appels} jusqu'à
+l'appel de $f$.
+
+\medskip
+
+\itempoint Certains langages donnent la \alert{citoyenneté de première
+  classe} aux continuations, i.e., permettent de les passer, stocker
+et invoquer explicitement :
+\begin{itemize}
+\item\alert{capturer} la contin\textsuperscript{ion} de $f$ revient à
+  garder une copie de la pile d'appels de $f$,
+\item\alert{invoquer} la contin\textsuperscript{ion} avec une valeur
+  $v$ a pour effet de faire retourner à $f$ la valeur $v$ (même si
+  elle avait \alert{déjà} terminé),
+\item c'est une sorte de \texttt{goto} jusqu'au point à $f$ termine,
+  avec restauration de la pile (en C : \texttt{getcontext} pour
+  capturer, \texttt{setcontext} pour restaurer).
+\end{itemize}
+
+\medskip
+
+{\footnotesize
+
+\itempoint Variante : capturer la continuation revient à créer un fil
+d'exécution (\textit{thread}) mis en attente au moment du retour de
+$f$, l'invoquer revient à terminer le fil actuel et réactiver le fil
+en attente, avec en lui transmettant $v$ : il va de nouveau créer un
+fil en attente, puis considérer $v$ comme valeur de retour de $f$.
+
+\par}
+
+\medskip
+
+\itempoint Les continuations permettent d'implémenter le multitâche
+coopératif.
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{La fonction call/cc}
+
+\itempoint « call/cc » = « call-with-current-continuation »
+
+\medskip
+
+\itempoint La fonction call/cc existe dans plusieurs langages de
+programmation (notam\textsuperscript{t} : Scheme, SML/NJ, Ruby) : elle
+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$.
+\end{itemize}
+
+\medskip
+
+\itempoint En Scheme, la continuation se présente comme une fonction,
+qu'on peut appeler avec un argument $v$ :
+\begin{itemize}
+\item la continuation elle-même ne termine jamais (puisque c'est,
+  justement, une continuation : elle \alert{remplace} la pile d'appels
+  par celle qui a été capturée),
+\item alle a pour effet de faire retourner $v$ au call/cc qui l'a
+  créée.
+\end{itemize}
+
+\medskip
+
+{\footnotesize
+
+\itempoint En SML/NJ, la fonction s'appelle
+\texttt{SMLofNJ.Cont.callcc} et les continuations doivent être
+invoquées avec la fonction \texttt{throw} ; mais on peut facilement
+créer une fonction analogue à celle du Scheme :
+
+{\tt
+val callcc = fn g => SMLofNJ.Cont.callcc (fn k => g (fn v => SMLofNJ.Cont.throw k v))
+}
+
+\par}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Exemples en Scheme}
+
+{\tt
+(define call/cc call-with-current-continuation)\hfill ;; Shorthand\\
+(call/cc (lambda (k) 42))\hfill ;; Return normally\\
+$\rightarrow$ 42\\
+(call/cc (lambda (k) (k 42)))\hfill ;; Return by invoking continuation\\
+$\rightarrow$ 42\\
+(call/cc (lambda (k) (+ (k 42) 1)))\hfill ;; (+ \_ 1) never reached\\
+$\rightarrow$ 42\\
+(* (call/cc (lambda (k) (k 42))) 2)\hfill ;; Nothing weird here\\
+$\rightarrow$ 84
+\par}
+
 \end{frame}
 %
 % TODO:
 % - Kripke
-% - fragment négatif
-% - call/cc
+% - CPS et fragment négatif
 % - inférence de type de Hindley-Milner
 %
 \end{document}
-- 
cgit v1.2.3