From 36f20350037e60ae5e64638fdaf2396bd37de98b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Thu, 22 Oct 2020 17:03:08 +0100 Subject: [PATCH] Control operator references --- macros.tex | 2 + thesis.bib | 135 ++++++++++++++++++++++++++++++++++++++++++++++++++++- thesis.tex | 32 +++++++++++-- 3 files changed, 164 insertions(+), 5 deletions(-) diff --git a/macros.tex b/macros.tex index a19a17a..8b91c0f 100644 --- a/macros.tex +++ b/macros.tex @@ -9,6 +9,8 @@ %% Some useful maths abbreviations %% \newcommand{\N}{\ensuremath{\mathbb{N}}} +\newcommand{\B}{\ensuremath{\mathbb{B}}} +\newcommand{\BB}[1]{\ensuremath{\mathbf{#1}}} %% %% Partiality diff --git a/thesis.bib b/thesis.bib index 11ceaff..e8e6f2e 100644 --- a/thesis.bib +++ b/thesis.bib @@ -1171,7 +1171,7 @@ year = {1994} } -# Control operators +# Landin's J operator @article{Landin65, author = {Peter J. Landin}, title = {Correspondence between {ALGOL} 60 and Church's Lambda-notation: part @@ -1204,6 +1204,138 @@ year = {1998} } +@article{DanvyM08, + author = {Olivier Danvy and + Kevin Millikin}, + title = {A Rational Deconstruction of Landin's {SECD} Machine with the {J} + Operator}, + journal = {Log. Methods Comput. Sci.}, + volume = {4}, + number = {4}, + year = {2008} +} + +# Cupto +@inproceedings{GunterRR95, + author = {Carl A. Gunter and + Didier R{\'{e}}my and + Jon G. Riecke}, + title = {A Generalization of Exceptions and Control in ML-like Languages}, + booktitle = {{FPCA}}, + pages = {12--23}, + publisher = {{ACM}}, + year = {1995} +} + +# Prompts +@inproceedings{Felleisen88, + author = {Matthias Felleisen}, + title = {The Theory and Practice of First-Class Prompts}, + booktitle = {{POPL}}, + pages = {180--190}, + publisher = {{ACM} Press}, + year = {1988} +} + +# Escape +@article{Reynolds98a, + author = {John C. Reynolds}, + title = {Definitional Interpreters for Higher-Order Programming Languages}, + journal = {High. Order Symb. Comput.}, + volume = {11}, + number = {4}, + pages = {363--397}, + year = {1998} +} + +# Amb +@incollection{McCarthy63, + author = {John McCarthy}, + title = {A Basis for a Mathematical Theory of Computation}, + editor = {P. Braffort and D. Hirschberg}, + series = {Studies in Logic and the Foundations of Mathematics}, + publisher = {Elsevier}, + volume = {35}, + pages = {33--70}, + year = {1963}, + booktitle = {Computer Programming and Formal Systems}, + OPTissn = "0049-237X", + OPTdoi = "https://doi.org/10.1016/S0049-237X(08)72018-4" +} + +# Simula (coroutines) +@inproceedings{DahlMN68, + author = {Ole-Johan Dahl and Bj\o{}rn Myhrhaug and Kristen Nygaard}, + title = {Some Features of the SIMULA 67 Language}, + year = {1968}, + publisher = {Winter Simulation Conference}, + booktitle = {Proceedings of the Second Conference on Applications of Simulations}, + pages = {29--31}, + numpages = {3}, + location = {New York, New York, USA} +} + +@book{DahlDH72, + editor = {Ole-Johan Dahl and Edgar W. Dijkstra and C. A. R. Hoare}, + title = {Structured Programming}, + year = {1972}, + isbn = {0122005503}, + publisher = {Academic Press Ltd.}, + address = {GBR} +} + +# Second-hand reference for the inventor of coroutines +@book{Knuth97, + author = {Donald E. Knuth}, + title = {The Art of Computer Programming, Volume 1 (3rd Ed.): Fundamental Algorithms}, + year = {1997}, + isbn = {0201896834}, + publisher = {Addison Wesley Longman Publishing Co., Inc.}, + address = {USA} +} + +# Second-hand reference for call/cc +@article{Abelson91, + author = {Abelson, H. + and Dybvig, R. K. + and Haynes, C. T. + and Rozas, G. J. + and Adams, N. I. + and Friedman, D. P. + and Kohlbecker, E. + and Steele, G. L. + and Bartley, D. H. + and Halstead, R. + and Oxley, D. + and Sussman, G. J. + and Brooks, G. + and Hanson, C. + and Pitman, K. M. + and Wand, M. + and Clinger, William + and Rees, Jonathan}, + title = {Revised4 Report on the Algorithmic Language Scheme}, + year = {1991}, + publisher = {Association for Computing Machinery}, + address = {New York, NY, USA}, + volume = {IV}, + number = {3}, + issn = {1045-3563}, + journal = {SIGPLAN Lisp Pointers}, + month = jul, + pages = {1–-55} +} + +# Common Lisp (resumable exceptions) +@book{Steele90, + author = {Guy L. Steele}, + title = {Common {LISP}: The Language (2nd Ed.)}, + year = {1990}, + isbn = {1555580416}, + publisher = {Digital Press}, + address = {USA} +} + # System F @phdthesis{Girard72, author = {J. Y. Girard}, @@ -1312,6 +1444,7 @@ year = {2008} } +# Catchcont @misc{LongleyW08, author = {John Longley and Nicholas Wolverson}, title = {Eriskay: a programming language based on game semantics}, diff --git a/thesis.tex b/thesis.tex index a623954..73b9fac 100644 --- a/thesis.tex +++ b/thesis.tex @@ -412,7 +412,7 @@ We use these properties to define partial and total functions. % A total function is also simply called a `function'. Throughout this dissertation the terms (partial) mapping and (partial) function are -used interchangeably. +synonymous. % For a function $f : A \to B$ (or partial function $f : A \pto B$) we @@ -467,7 +467,14 @@ respectively. \section{Universal algebra} \label{sec:universal-algebra} -\begin{definition}[Algebra]\label{def:algebra} +Universal algebra studies \emph{algebraic theories}. + +\begin{definition}[Operations] + +\end{definition} + +\begin{definition}[Algebraic theory]\label{def:algebra} + \end{definition} \section{Algebraic effects and their handlers} @@ -492,14 +499,31 @@ handlers. Moggi's work gives a precise characterisation of what's \emph{not} an effect} -\chapter{Continuations} +\chapter{Control operators} \label{ch:continuations} +Undelimited control: Landin's J~\cite{Landin98}, Reynolds' +escape~\cite{Reynolds98a}, Scheme75's catch~\cite{SussmanS75}, callcc +is a procedural variation of catch. It was invented in +1982~\cite{Abelson91}. + +Delimited control: Common Lisp resumable exceptions (condition +system)~\cite{Steele90}, prompt/control~\cite{Felleisen88}, +shift/reset~\cite{DanvyF90}, catchcont~\cite{LongleyW08}, effect +handlers~\cite{PlotkinP09}. + +Backtracking: Amb~\cite{McCarthy63}. + +Coroutines~\cite{DahlDH72} as introduced by Simula +67~\cite{DahlMN68}. The notion of coroutines was coined by Melvin +Conway, who used coroutines as a code idiom in assembly +programs~\cite{Knuth97}. + \section{Zoo of control operators} Describe how effect handlers fit amongst shift/reset, prompt/control, callcc, J, catchcont, etc. -\section{Implementation strategies} +\section{Ad-hoc implementation strategies} \part{Design}