diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 56 |
1 files changed, 45 insertions, 11 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 380d40d..eacec62 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -3781,30 +3781,64 @@ terminale propre. \medskip -\itempoint La conversion vers CPS impose de préciser complètement -l'ordre d'évaluation. Par exemple, on a défini $\langle -x,y\rangle^{\cps} = \lambda k.\, x^{\cps}(\lambda x_0.\, y^{\cps} -(\lambda y_0.\, k\langle x_0,y_0\rangle))$ qui évalue $x$ avant $y$, -mais on pouvait aussi $\lambda k.\, y^{\cps} (\lambda y_0.\, -x^{\cps}(\lambda x_0.\, k\langle x_0,y_0\rangle))$ pour inverser -l'ordre. +\itempoint La conversion vers CPS fixe l'ordre d'évaluation des +valeurs. Par exemple, on a défini $\langle x,y\rangle^{\cps} = +\lambda k.\, x^{\cps}(\lambda x_0.\, y^{\cps} (\lambda y_0.\, k\langle +x_0,y_0\rangle))$ qui évalue $x$ avant $y$, mais on pouvait aussi +$\lambda k.\, y^{\cps} (\lambda y_0.\, x^{\cps}(\lambda x_0.\, +k\langle x_0,y_0\rangle))$ pour inverser l'ordre. \medskip +{\footnotesize + +\itempoint La conversion vers CPS fixe même une stratégie +d'évaluation : on a choisi « call-by-value » ici, mais on aurait pu +prendre « call-by-name » : + +\begin{tabular}{c|c} +« call-by-value »&« call-by-name »\\\hline +$v^{\cps} = \lambda k.kv$&$v^{\cps} = \lambda k.vk$ (ou juste $v$)\\ +&mais pour une \emph{valeur} : $x^{\cps} = \lambda k.kx$\\ +$(\lambda v.t)^{\cps} = \lambda k.\, k(\lambda v.\, t^{\cps})$ +&$(\lambda v.t)^{\cps} = \lambda k.\, k(\lambda v.\, t^{\cps})$\\ +$(fx)^{\cps} = \lambda + k.\,f^{\cps}(\lambda f_0.\, x^{\cps}(\lambda x_0.\, f_0 x_0 k))$ +&$(fx)^{\cps} = \lambda + k.\,f^{\cps}(\lambda f_0.\, f_0 x^{\cps} k)$\\ +$(P\Rightarrow Q)^\diamond = (P^\diamond\Rightarrow \mathop{\sim}\mathop{\sim}Q^\diamond)$ +&$(P\Rightarrow Q)^\diamond = (\mathop{\sim}\mathop{\sim}P^\diamond\Rightarrow \mathop{\sim}\mathop{\sim}Q^\diamond)$ +\end{tabular} + +\par} + +\end{frame} +% +\begin{frame} +\frametitle{Continuation Passing Style : remarques informatiques (suite)} + \itempoint Le CPS donne le call/cc « pour rien ». En fait, en style CPS, chaque fonction a contrôle complet sur l'exécution de tout le programme (il n'y a plus de pile !). \medskip -\itempoint Ceci peut servir de point de départ pour la compilation +\itempoint Le CPS peut servir de point de départ pour la compilation (Appel, \textit{Compiling with Continuations}, 1992). \medskip -\itempoint Utile pour séquencer explicitement les évaluations. Voir -notamment les promesses de JavaScript, et la monade -\texttt{Control.Monad.Cont} de Haskell. +\itempoint On peut concevoir un langage où chaque fonction a +p.ex. \alert{deux} continuations : une « continuation de succès » et +une « continuation d'échec », qu'on chaîne avec des opérateurs « et » +et « ou » : c'est essentiellement le Prolog (où ces opérateurs sont +notés ‘\texttt{,}’ et ‘\texttt{;}’). + +\medskip + +\itempoint Le CPS est utile pour séquencer explicit\textsuperscript{t} +les évaluations. Voir notamment les promesses de JavaScript, et la +monade \texttt{Control.Monad.Cont} de Haskell. \end{frame} % |