summaryrefslogtreecommitdiffstats
path: root/transp-inf110-02-typage.tex
diff options
context:
space:
mode:
authorDavid A. Madore <david+git@madore.org>2023-12-12 20:47:47 +0100
committerDavid A. Madore <david+git@madore.org>2023-12-12 20:47:47 +0100
commitfc401219084fdd6c2acfd914f5025bed8f1a3337 (patch)
tree9575812719c517bb6323c9d26c13f7eb5e1a3a0b /transp-inf110-02-typage.tex
parent25cceb3ae06dbf9323cb5b9437f2a26647192d19 (diff)
downloadinf110-lfi-fc401219084fdd6c2acfd914f5025bed8f1a3337.tar.gz
inf110-lfi-fc401219084fdd6c2acfd914f5025bed8f1a3337.tar.bz2
inf110-lfi-fc401219084fdd6c2acfd914f5025bed8f1a3337.zip
Discuss continuation-passing-style.
Diffstat (limited to 'transp-inf110-02-typage.tex')
-rw-r--r--transp-inf110-02-typage.tex55
1 files changed, 53 insertions, 2 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 2776a21..08cf5a9 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -2256,7 +2256,7 @@ En OCaml :
{\tt
type void = | ;;
let exfalso = fun (r:void) -> match r with \_ -> . ;;
-}
+\par}
\par}
@@ -2338,7 +2338,7 @@ fun u -> (match (pi1 u) with Inj1 v -> Inj1 v\\
\ \ | Inj2 v\_ -> (match (pi2 u) with Inj1 w -> Inj1 w\\
\ \ \ \ | Inj2 w\_ -> Inj2 (v\_,w\_))) ;;\\
{\color{purple}- : ('a, 'b) sum * ('a, 'c) sum -> ('a, 'b * 'c) sum = <fun>}
-}
+\par}
\end{frame}
%
@@ -3472,6 +3472,57 @@ intéressant.
\end{frame}
%
+\begin{frame}
+\frametitle{Continuation Passing Style}
+
+\textcolor{brown}{Et si le langage n'a pas de call/cc ?}
+
+\medskip
+
+\itempoint Tous les langages n'ont pas de continuations de première
+classe (« réifiées »), mais dans un langage fonctionnel, on peut
+réécrire le code en « Continuation Passing Style » :
+\begin{itemize}
+\item au lieu d'écrire des fonctions qui \alert{renvoient une valeur}
+ $v$, on les fait \alert{prendre en argument} une autre fonction $k$,
+ qui est une continuation-de-fait, et appellent cette fonction sur la
+ valeur $v$ ;
+\item donc aucune fonction ne renvoie jamais rien : elle termine en
+ invoquant son argument continuation-de-fait ou, plus souvent, en
+ invoquant une autre fonction en lui passant une continuation-de-fait
+ construite exprès pour continuer le calcul {\footnotesize (ceci rend
+ le style excessivement lourd et pénible)} ;
+\item ceci ne fonctionne bien que dans un langage supportant la
+ récursion terminale propre (car \alert{tous} les appels deviennent
+ terminaux).
+\end{itemize}
+
+\smallskip
+
+{\footnotesize \itempoint C'est plus ou moins le concept des
+ « promesses » de JavaScript, par exemple.\par}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Continuation Passing Style : exemple en OCaml}
+
+{\footnotesize\tt
+let sum\_cps = fun x -> fun y -> fun k -> k(x+y) ;;\\
+{\color{purple}val sum\_cps : int -> int -> (int -> 'a) -> 'a = <fun>}\\
+let minus\_cps = fun x -> fun y -> fun k -> k(x-y) ;;\\
+{\color{purple}val minus\_cps : int -> int -> (int -> 'a) -> 'a = <fun>}\\
+let rec fibonacci\_cps = fun n -> fun k -> if n <= 1 then k n\\
+\ \ else minus\_cps n 1 (fun n1 -> minus\_cps n 2 (fun n2 ->\\
+\ \ \ \ fibonacci\_cps n1 (fun v1 -> fibonacci\_cps n2 (fun v2 ->\\
+\ \ \ \ \ \ sum\_cps v1 v2 k)))) ;;\\
+{\color{purple}val fibonacci\_cps : int -> (int -> 'a) -> 'a = <fun>}\\
+fibonacci\_cps 8 (fun x -> x) ;;\\
+{\color{purple}- : int = 21}
+\par}
+
+\end{frame}
+%
% TODO:
% - Kripke
% - CPS et fragment négatif