dhil/phd-dissertation
1
0
Fork 0
mirror of https://github.com/dhil/phd-dissertation synced 2026-03-12 18:48:25 +00:00
Code Issues Releases Wiki Activity

Fix Ref macro

Browse Source
This commit is contained in:
Daniel Hillerström
2021-05-18 08:04:20 +01:00
parent 52b12535ae
commit 8ecfadb94e
2 changed files with 15 additions and 14 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
macros.tex
View File

@@ -77,6 +77,7 @@
\newcommand{\Inl}{\keyw{inl}} \newcommand{\Inl}{\keyw{inl}}
\newcommand{\Inr}{\keyw{inr}} \newcommand{\Inr}{\keyw{inr}}
\newcommand{\Thunk}{\lambda \Unit.} \newcommand{\Thunk}{\lambda \Unit.}
\newcommand{\PCFRef}{\keyw{ref}}
\newcommand{\Pre}[1]{\mathsf{Pre}(#1)} \newcommand{\Pre}[1]{\mathsf{Pre}(#1)}
\newcommand{\Abs}{\mathsf{Abs}} \newcommand{\Abs}{\mathsf{Abs}}

28
thesis.tex
View File

@@ -1163,20 +1163,20 @@ handlers.
% %
\dhil{Definition of (typed) programming language, conservative extension, macro-expressiveness~\cite{Felleisen90,Felleisen91}} \dhil{Definition of (typed) programming language, conservative extension, macro-expressiveness~\cite{Felleisen90,Felleisen91}}
\chapter{State of effectful programming} % \chapter{State of effectful programming}
\label{ch:related-work} % \label{ch:related-work}
% \section{Type and effect systems} % % \section{Type and effect systems}
% \section{Monadic programming} % % \section{Monadic programming}
\section{Golden age of impurity} % \section{Golden age of impurity}
\section{Monadic enlightenment} % \section{Monadic enlightenment}
\dhil{Moggi's seminal work applies the notion of monads to effectful % \dhil{Moggi's seminal work applies the notion of monads to effectful
programming by modelling effects as monads. More importantly, % programming by modelling effects as monads. More importantly,
Moggi's work gives a precise characterisation of what's \emph{not} % Moggi's work gives a precise characterisation of what's \emph{not}
an effect} % an effect}
\section{Direct-style revolution} % \section{Direct-style revolution}
\subsection{Monadic reflection: best of both worlds} % \subsection{Monadic reflection: best of both worlds}
\chapter{Continuations} \chapter{Continuations}
\label{ch:continuations} \label{ch:continuations}
@@ -15868,11 +15868,11 @@ be modified.
We have in mind an extension $\BCalcS$ of $\BCalc$ with ML-style We have in mind an extension $\BCalcS$ of $\BCalc$ with ML-style
reference cells: we extend our grammar for types with a reference type reference cells: we extend our grammar for types with a reference type
($\Ref~A$), and that for computation terms with forms for creating ($\PCFRef~A$), and that for computation terms with forms for creating
references ($\keyw{letref}\; x = V\; \In\; N$), dereferencing ($!x$), references ($\keyw{letref}\; x = V\; \In\; N$), dereferencing ($!x$),
and destructive update ($x := V$), with the familiar typing rules. We and destructive update ($x := V$), with the familiar typing rules. We
also add a new kind of value, namely \emph{locations} $l^A$, of type also add a new kind of value, namely \emph{locations} $l^A$, of type
$\Ref~A$. We adopt a basic Scott-Strachey~\citeyearpar{ScottS71} model $\PCFRef~A$. We adopt a basic Scott-Strachey~\citeyearpar{ScottS71} model
of store: a location is a natural number decorated with a type, and of store: a location is a natural number decorated with a type, and
the execution of a stateful program allocates locations in the order the execution of a stateful program allocates locations in the order
$0,1,2,\ldots$, assigning types to them as it does so. A \emph{store} $0,1,2,\ldots$, assigning types to them as it does so. A \emph{store}