From 78e291d6022ee7ed56c85c20e70259615d54097c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Tue, 13 Apr 2021 00:38:09 +0100 Subject: [PATCH] WIP --- thesis.bib | 12 ++++++ thesis.tex | 122 +++++++++++++++++++++++++++++++++++------------------ 2 files changed, 93 insertions(+), 41 deletions(-) diff --git a/thesis.bib b/thesis.bib index c786f76..e556fb2 100644 --- a/thesis.bib +++ b/thesis.bib @@ -2434,6 +2434,18 @@ year = {2015} } +# Abstract machines +@article{BiernackaBD03, + author = {Malgorzata Biernacka and Dariusz Biernacki and Olivier Danvy}, + title = {An Operational Foundation for Delimited Continuations}, + volume = {10}, + OPTdoi = {10.7146/brics.v10i41.21809}, + number = {41}, + journal = {BRICS Report Series}, + year = {2003}, + OPTmonth = dec +} + # Partial evaluation with control @inproceedings{LawallD94, author = {Julia L. Lawall and diff --git a/thesis.tex b/thesis.tex index e6e8b2a..77f105d 100644 --- a/thesis.tex +++ b/thesis.tex @@ -10820,13 +10820,13 @@ on work in the following previously published papers. The particular presentation in this chapter is adapted from item~\ref{en:ch-am-HLA20}. -\section{Machine configurations} +\section{Configurations with generalised continuations} \label{sec:machine-configurations} The abstract machine is formally defined in terms of configurations. A -configuration $\cek{M \mid \env \mid \shk \circ \shk'}$ is a triple -consisting of a computation term $M \in \CompCat$, an environment -$\env \in \MEnvCat$, and a two generalised continuations -$\kappa,\kappa' \in \MGContCat$. +configuration $\cek{M \mid \env \mid \shk \circ \shk'} \in \MConfCat$ +is a triple consisting of a computation term $M \in \CompCat$, an +environment $\env \in \MEnvCat$, and a pair of generalised +continuations $\kappa,\kappa' \in \MGContCat$. % The complete abstract machine syntax is given in Figure~\ref{fig:abstract-machine-syntax}. @@ -10835,38 +10835,69 @@ The control and environment components are completely standard as they are similar to the components in \citeauthor{FelleisenF86}'s original CEK machine modulo the syntax of the source language. % -The structure of the continuation component is new. This component -comprises two generalised continuations, where the latter continuation -is an entirely administrative object that only manifests during effect -forwarding. The continuation component The latter continuation is -always the identity, except when forwarding an operation, in which -case it is used to keep track of the extent to which the operation has -been forwarded. -% -We write $\cek{M \mid \env \mid \shk}$ as syntactic sugar for $\cek{M - \mid \env \mid \shk \circ []}$ where $[]$ is the identity -continuation. -% - -Values consist of function closures, type function closures, records, -variants, and captured continuations. -% -A continuation $\shk$ is a stack of frames $[\shf_1, \dots, -\shf_n]$. We annotate captured continuations with input types in order -to make the results of Section~\ref{subsec:machine-correctness} easier -to state. Each frame $\shf = (\slk, \chi)$ represents pure -continuation $\slk$, corresponding to a sequence of let bindings, +However, the structure of the continuation component is new. This +component comprises two generalised continuations, where the latter +continuation $\kappa'$ is an entirely administrative object that +materialises only during operation invocations as it is used to +construct the reified segment of the continuation up to an appropriate +enclosing handler. For the most part $\kappa'$ is empty, therefore we +will write $\cek{M \mid \env \mid \shk}$ as syntactic sugar for +$\cek{M \mid \env \mid \shk \circ []}$ where $[]$ is the empty +continuation (an alternative is to syntactically differentiate between +regular and administrative configurations by having both three-place +and four-place configurations as for example as \citet{BiernackaBD03} +do). +% + +An environment is either empty, written $\emptyset$, or an extension +of some other environment $\env$, written $\env[x \mapsto v]$, where +$x$ is the name of a variable and $v$ is a machine value. +% +The machine values consist of function closures, recursive function +closures, type function closures, records, variants, and reified +continuations. The three abstraction forms are paired with an +environment that binds the free variables in the their bodies. The +records and variants are transliterated from the value forms of the +source calculi. Figure~\ref{fig:abstract-machine-val-interp} defines +the value interpretation function, which turns any source language +value into a corresponding machine value. +% +A continuation $\shk$ is a stack of generalised continuation frames +$[\shf_1, \dots, \shf_n]$. Each frame $\shf = (\slk, \chi)$ represents +pure continuation $\slk$, corresponding to a sequence of let bindings, inside handler closure $\chi$. % -A pure continuation is a stack of pure frames. A pure frame $(\env, x, -N)$ closes a let-binding $\Let \;x=[~] \;\In\;N$ over environment -$\env$. A handler closure $(\env, H)$ closes a handler definition $H$ -over environment $\env$. +A pure continuation is a stack of pure frames. A pure frame +$(\env, x, N)$ closes a let-binding $\Let \;x=[~] \;\In\;N$ over +environment $\env$. The pure continuation structure is similar to the +continuation structure of \citeauthor{FelleisenF86}'s original CEK +machine. +% +There are three kinds of handler closures, one for each kind of +handler. A deep handler closure is a pair $(\env, H)$ which closes a +deep handler definition $H$ over environment $\env$. Similarly, a +shallow handler closure $(\env, H^\dagger)$ closes a shallow handler +definition over environment $\env$. Finally, a parameterised handler +closure $(\env, (q.\,H))$ closes a parameterised handler definition +over environment $\env$. As a syntactic shorthand we write $H^\depth$ +to range over deep, shallow, and parameterised handler +definitions. Sometimes $H^\depth$ will range over just two kinds of +handler definitions; it will be clear from the context which handler +definition is omitted. +% +We extend the clause projection notation to handler closures and +generalised continuation frames, i.e. +% +\[ + \ba{@{~}l@{~}c@{~}l@{~}c@{~}l@{~}l} + \theta^{\mathrm{ret}} &\defas& (\sigma, \chi^{\mathrm{ret}}) &\defas& \hret, &\quad \text{where } \chi = (\env, H^\depth)\\ + \theta^{\ell} &\defas& (\sigma, \chi^{\ell}) &\defas& \hell, &\quad \text{where } \chi = (\env, H^\depth) + \el +\] % -We write $\nil$ for an empty stack, $x \cons s$ for the result of -pushing $x$ on top of stack $s$, and $s \concat s'$ for the -concatenation of stack $s$ on top of $s'$. We use pattern matching to -deconstruct stacks. +Values are annotated with types where appropriate to facilitate type +reconstruction in order to make the results of +Section~\ref{subsec:machine-correctness} easier to state. % % \begin{figure}[t] @@ -10874,13 +10905,15 @@ deconstruct stacks. \begin{syntax} \slab{Configurations} & \conf \in \MConfCat &::= & \cek{M \mid \env \mid \shk \circ \shk'} \\ \slab{Value\textrm{ }environments} &\env \in \MEnvCat &::= & \emptyset \mid \env[x \mapsto v] \\ -\slab{Values} &v, w \in \MValCat &::= & (\env, \lambda x^A . M) \mid (\env, \Lambda \alpha^K . M) \\ - & &\mid& \Record{} \mid \Record{\ell = v; w} \mid (\ell\, v)^R \mid \shk^A \mid (\shk, \slk)^A \medskip\\ +\slab{Values} &v, w \in \MValCat &::= & (\env, \lambda x^A . M) \mid (\env, \Rec^{A \to C}\,x.M)\\ + & &\mid& (\env, \Lambda \alpha^K . M) \\ + & &\mid& \Record{} \mid \Record{\ell = v; w} \mid (\ell\, v)^R \\ + & &\mid& \shk^A \mid (\shk, \slk)^A \medskip\\ \slab{Continuations} &\shk \in \MGContCat &::= & \nil \mid \shf \cons \shk \\ \slab{Continuation\textrm{ }frames} &\shf \in \MGFrameCat &::= & (\slk, \chi) \\ \slab{Pure\textrm{ }continuations} &\slk \in \MPContCat &::= & \nil \mid \slf \cons \slk \\ \slab{Pure\textrm{ }continuation\textrm{ }frames} &\slf \in \MPFrameCat &::= & (\env, x, N) \\ -\slab{Handler\textrm{ }closures} &\chi \in \MHCloCat &::= & (\env, H) \mid (\env, H)^\dagger \mid (\env, (q.\,H)) \medskip \\ +\slab{Handler\textrm{ }closures} &\chi \in \MHCloCat &::= & (\env, H) \mid (\env, H^\dagger) \mid (\env, (q.\,H)) \medskip \\ \end{syntax} \caption{Abstract machine syntax.} @@ -10910,7 +10943,7 @@ deconstruct stacks. \end{figure} % -\section{Machine transitions} +\section{Generalised continuation-based machine semantics} \label{sec:machine-transitions} % \begin{figure}[p] @@ -11013,7 +11046,7 @@ deconstruct stacks. \[ \bl \ba{@{~}l@{\quad}l@{~}l} - \multicolumn{2}{l}{\textbf{Identity continuation}}\\ + \multicolumn{2}{l}{\textbf{Initial continuation}}\\ \multicolumn{3}{l}{\quad\shk_0 \defas [(\nil, (\emptyset, \{\Return\;x \mapsto x\}))]} \medskip\\ % @@ -11032,7 +11065,12 @@ deconstruct stacks. The abstract machine semantics defining the transition function $\stepsto$ is given in Fig.~\ref{fig:abstract-machine-semantics}. % -It depends on an interpretation function $\val{-}$ for values. +We write $\nil$ for an empty stack, $x \cons s$ for the result of +pushing $x$ on top of stack $s$, and $s \concat s'$ for the +concatenation of stack $s$ on top of $s'$. We use pattern matching to +deconstruct stacks. +% +% It depends on an interpretation function $\val{-}$ for values. % The machine is initialised (\mlab{Init}) by placing a term in a configuration alongside the empty environment and identity @@ -11342,7 +11380,7 @@ type $A$, or get stuck failing to handle an operation appearing in $E$. We now make the correspondence between the operational semantics and the abstract machine more precise. -\section{Correctness} +\section{Machine correctness} \label{subsec:machine-correctness} Fig.~\ref{fig:config-to-term} defines an inverse mapping $\inv{-}$ @@ -11400,6 +11438,8 @@ If $\typc{}{M : A}{E}$ and $M \reducesto^+ N \not\reducesto$, then $M \stepsto^+ \conf$ with $\inv{\conf} = N$. \end{corollary} +\section{Related work} + \part{Expressiveness} \chapter{Interdefinability of effect handlers}