From 7c3942a5647a940949b5ebdf421b8149a8058a77 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Mon, 24 May 2021 11:49:38 +0100 Subject: [PATCH] WIP --- thesis.bib | 25 ++++++++++++++++++++++- thesis.tex | 59 ++++++++++++++++++++++++++++++++++++++---------------- 2 files changed, 66 insertions(+), 18 deletions(-) diff --git a/thesis.bib b/thesis.bib index 7245e98..a402b3a 100644 --- a/thesis.bib +++ b/thesis.bib @@ -741,6 +741,19 @@ year = {2012} } +# "Proto handlers" +@inproceedings{CartwrightF94, + author = {Robert Cartwright and + Matthias Felleisen}, + title = {Extensible Denotational Language Specifications}, + booktitle = {{TACS}}, + series = {Lecture Notes in Computer Science}, + volume = {789}, + pages = {244--272}, + publisher = {Springer}, + year = {1994} +} + # Applicative idioms @article{McBrideP08, author = {Conor McBride and @@ -3531,4 +3544,14 @@ number = {2}, pages = {98--107}, year = {1989} -} \ No newline at end of file +} + +# Curry-Howard correspondence +@incollection{Howard80, + author = {William A. Howard}, + title = {The Formulae-as-Types Notion of Construction}, + booktitle = {To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism}, + publisher = {Academic Press}, + editor = {Haskell Curry and Hindley B. and Seldin J. Roger and P. Jonathan}, + year = 1980 +} diff --git a/thesis.tex b/thesis.tex index 759d5c7..d742af4 100644 --- a/thesis.tex +++ b/thesis.tex @@ -371,15 +371,31 @@ \chapter{Introduction} \label{ch:introduction} % -Functional programmers tend to view functions as impenetrable black +Functional programmers tend to view programs as impenetrable opaque boxes, whose outputs are determined entirely by their -inputs~\cite{Hughes89}. This is a compelling view which admits a -canonical mathematical model of +inputs~\cite{Hughes89,Howard80}. This is a compelling view which +admits a canonical mathematical model of computation~\cite{Church32,Church41}. % Alas, this view does not capture the reality of practical programs, -which must interact with their environment (i.e. operating system) to -facilitate file I/O\dots +which perform operations to interact with their ambient environment to +for example signal graceful or erroneous termination, manipulate the +file system, fork a new thread, and so forth, all of which may have an +observable effect on the program state. Interactions with the +environment are mediated by some local authority (e.g. operating +system), which confers the meaning of operations~\cite{CartwrightF94}. +% +This suggests a view of programs as translucent boxes, which convey +their internal use of operations used to compute their outputs. + +This view underpins the \emph{effectful programming paradigm} in which +computational effects constitute an integral part of programs. In +effectful programming a computational effect is understood as a +collection of operations, e.g. exceptions are an effect with a single +operation \emph{raise}, mutable state is an effect with two operations +\emph{get} and \emph{put}, concurrency is an effect with two +operations \emph{fork} and \emph{yield}, etc~\cite{Moggi91,PlotkinP01}. + % Alas, this view does not capture the reality of practical programs, which % may use a variety of observable computational effects such as % exceptions, state, concurrency, interactive input/output, and so @@ -405,18 +421,27 @@ Functional programming offers two distinct, but related, approaches to effectful programming, which \citet{Filinski96} succinctly characterises as \emph{effects as data} and \emph{effects as behaviour}. The former uses monads to encapsulate -effects~\cite{Moggi91,Wadler92} which is compelling because it extends -the black box view to effectful functions, though, at the expense of a -change of programming style~\cite{JonesW93}. The latter retains the -usual direct style of programming by way of \emph{first-class - control}, which is a powerful facility that can simulate any -effect~\cite{Filinski94,Filinski96}. First-class control enables the -programmer to manipulate and reify the control state as a first-class -data object known as a continuation~\cite{FriedmanHK84}. First-class -control has the ability pry open function boundaries, which fractures -the black box view of computation. This ability can significantly -improve the computational expressiveness and efficiency of programming -languages~\cite{LongleyN15,HillerstromLL20}. +effects~\cite{Moggi91,Wadler92} which is compelling because it +recovers some of benefits of the opaque box view for effectful +programs, though, at the expense of a change of programming +style~\cite{JonesW93}. The latter retains the usual direct style of +programming by way of \emph{first-class control}, which is a powerful +facility that can simulate any computational +effect~\cite{Filinski94,Filinski96}. + +\citeauthor{PlotkinP09}'s \emph{effect handlers} are a recent +innovation\dots + +% First-class control enables the programmer to reify and manipulate the +% control state as a first-class data object known as a +% continuation~\cite{FriedmanHK84}. + + +% +% Programmers with continuations at their disposal have the ability to +% pry open function boundaries, which shatters the opaque box view. This +% ability can significantly improve the computational expressiveness and +% efficiency of programming languages~\cite{LongleyN15,HillerstromLL20}. effect handlers, a recent innovation,