dhil/phd-dissertation
1
0
Fork 0
mirror of https://github.com/dhil/phd-dissertation synced 2026-03-13 02:58:26 +00:00
Code Issues Releases Wiki Activity

Pass through parameterised handlers section

Browse Source
This commit is contained in:
Daniel Hillerström
2020-10-27 13:26:30 +00:00
parent c047b061c7
commit de8158d6ec
1 changed files with 4 additions and 8 deletions
Download Patch File Download Diff File Expand all files Collapse all files

12
thesis.tex
View File

@@ -4378,12 +4378,8 @@ approximate the body of the resumption up to administrative reduction.
\section{Parameterised handlers} \section{Parameterised handlers}
\label{sec:unary-parameterised-handlers} \label{sec:unary-parameterised-handlers}
In Section~\ref{sec:state} we informally presented parameterised Parameterised handlers are a useful idiom for handling stateful
handlers as a useful idiom for handling stateful computations. We now computations.
consider parameterised handlers as a primitive in $\HCalc$, and show
how to extend the CPS and abstract machine implementations to support
them. We also show that parameterised handlers can always be simulated
by deep handlers.
\subsection{Syntax and static semantics} \subsection{Syntax and static semantics}
% %
@@ -4427,7 +4423,7 @@ the parameter $q$.
{{\bl {{\bl
C = A \eff \{(\ell_i : A_i \to B_i)_i; R\} \\ C = A \eff \{(\ell_i : A_i \to B_i)_i; R\} \\
D = B \eff \{(\ell_i : P)_i; R\} \\ D = B \eff \{(\ell_i : P)_i; R\} \\
H = \{\Return\;x \mapsto M\} \uplus \{ \ell_i\;p_i\;r_i \mapsto N_i \}_i H = \{\Return\;x \mapsto M\} \uplus \{ \OpCase{\ell_i}{p_i}{r_i} \mapsto N_i \}_i
\el}\\\\ \el}\\\\
\typ{\Delta;\Gamma, q : A', x : A}{M : D}\\\\ \typ{\Delta;\Gamma, q : A', x : A}{M : D}\\\\
[\typ{\Delta;\Gamma,q : A', p_i : A_i, r_i : B_i \to D}{N_i : D}]_i [\typ{\Delta;\Gamma,q : A', p_i : A_i, r_i : B_i \to D}{N_i : D}]_i
@@ -4459,7 +4455,7 @@ $\semlab{Op^\param}$.
&\ParamHandle \; \EC[\Do \; \ell \; V] \; \With \; (q.~H)(W)\\ &\ParamHandle \; \EC[\Do \; \ell \; V] \; \With \; (q.~H)(W)\\
\reducesto& \reducesto&
N[V/p,W/q,\lambda \Record{y;q'}.\Handle \; \EC[\Return \; y] \; \With \; (q.~H)(q')/r]\\ N[V/p,W/q,\lambda \Record{y;q'}.\Handle \; \EC[\Return \; y] \; \With \; (q.~H)(q')/r]\\
& \text{ where } \ell \notin BL(\EC) \text{ and } \hell = \{ \ell \; p \; r \mapsto N \} & \text{ where } \ell \notin BL(\EC) \text{ and } \hell = \{ \OpCase{\ell}{p}{r} \mapsto N \}
\ea \ea
\] \]
% %