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

Remove static semantics paragraphs from escape and catch.

Browse Source
This commit is contained in:
Daniel Hillerström
2020-12-01 23:23:50 +00:00
parent ab36a78a50
commit bebb40ce9f
1 changed files with 34 additions and 29 deletions
Download Patch File Download Diff File Expand all files Collapse all files

63
thesis.tex
View File

@@ -817,28 +817,34 @@ available for use within $N$. \citeauthor{Reynolds98a} recognised the
power of this idiom and noted that it could be used to implement power of this idiom and noted that it could be used to implement
coroutines and backtracking~\cite{Reynolds98a}. coroutines and backtracking~\cite{Reynolds98a}.
% %
In our simply-typed setting it is not possible for the continuation to \citeauthor{Reynolds98a} did not develop the static semantics for
propagate outside its binding $\Escape$-expression as it would require $\Escape$, however, it is worth noting that this idiom require
the addition of either recursive types or some other escape hatch like recursive types to type check. Even in a language without recursive
types, the continuation may propagate outside its binding
$\Escape$-expression if the language provides an escape hatch such as
mutable reference cells. mutable reference cells.
% % In our simply-typed setting it is not possible for the continuation to
% propagate outside its binding $\Escape$-expression as it would require
% the addition of either recursive types or some other escape hatch like
% mutable reference cells.
% %
The typing of $\Escape$ and $\Continue$ reflects that the captured % The typing of $\Escape$ and $\Continue$ reflects that the captured
continuation is abortive. % continuation is abortive.
% % %
\begin{mathpar} % \begin{mathpar}
\inferrule* % \inferrule*
{\typ{\Gamma,k : \Cont\,\Record{A;\Zero}}{M : A}} % {\typ{\Gamma,k : \Cont\,\Record{A;\Zero}}{M : A}}
{\typ{\Gamma}{\Escape\;k\;\In\;M : A}} % {\typ{\Gamma}{\Escape\;k\;\In\;M : A}}
% \inferrule* % % \inferrule*
% {\typ{\Gamma}{V : A} \\ \typ{\Gamma}{W : \Cont\,\Record{A;\Zero}}} % % {\typ{\Gamma}{V : A} \\ \typ{\Gamma}{W : \Cont\,\Record{A;\Zero}}}
% {\typ{\Gamma}{\Continue~W~V : \Zero}} % % {\typ{\Gamma}{\Continue~W~V : \Zero}}
\end{mathpar} % \end{mathpar}
% % %
The return type of the continuation object can be taken as a telltale % The return type of the continuation object can be taken as a telltale
sign that an invocation of this object never returns, since there are % sign that an invocation of this object never returns, since there are
no inhabitants of the empty type. % no inhabitants of the empty type.
% %
An invocation of the continuation discards the invocation context and An invocation of the continuation discards the invocation context and
plugs the argument into the captured context. plugs the argument into the captured context.
@@ -869,18 +875,17 @@ with access to the current continuation. Thus it is same as
M,N ::= \cdots \mid \Catch~k.M M,N ::= \cdots \mid \Catch~k.M
\] \]
% %
Although, their syntax differ, their static and dynamic semantics are Although, their syntax differ, their dynamic semantics are the same.
the same.
% %
\begin{mathpar} % \begin{mathpar}
\inferrule* % \inferrule*
{\typ{\Gamma,k : \Cont\,\Record{A;\Zero}}{M : A}} % {\typ{\Gamma,k : \Cont\,\Record{A;\Zero}}{M : A}}
{\typ{\Gamma}{\Catch~k.M : A}} % {\typ{\Gamma}{\Catch~k.M : A}}
% \inferrule* % % \inferrule*
% {\typ{\Gamma}{V : A} \\ \typ{\Gamma}{W : \Cont\,\Record{A;B}}} % % {\typ{\Gamma}{V : A} \\ \typ{\Gamma}{W : \Cont\,\Record{A;B}}}
% {\typ{\Gamma}{\Continue~W~V : B}} % % {\typ{\Gamma}{\Continue~W~V : B}}
\end{mathpar} % \end{mathpar}
% %
\begin{reductions} \begin{reductions}
\slab{Capture} & \EC[\Catch~k.M] &\reducesto& \EC[M[\qq{\cont_{\EC}}/k]]\\ \slab{Capture} & \EC[\Catch~k.M] &\reducesto& \EC[M[\qq{\cont_{\EC}}/k]]\\