From 592b2f4fdf77992feff99255bed7e9288cdc74e8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Thu, 5 Dec 2019 14:45:55 +0000 Subject: [PATCH] Calculi macros. --- macros.tex | 76 +++++++++++++++++++++++++++++++++++++++++++++++ thesis.tex | 86 +++++++++++++++++++++++++++++++----------------------- 2 files changed, 126 insertions(+), 36 deletions(-) create mode 100644 macros.tex diff --git a/macros.tex b/macros.tex new file mode 100644 index 0000000..df32e12 --- /dev/null +++ b/macros.tex @@ -0,0 +1,76 @@ +%% +%% Calculi names. +%% +\newcommand{\Links}{Links\xspace} +\newcommand{\BCalc}{\ensuremath{\lambda_{\mathsf{b}}}} +\newcommand{\BCalcRec}{\ensuremath{\lambda_{\mathsf{b}+\mathsf{rec}}}} + +%% +%% Calculi terms and types type-setting. +%% +\newcommand{\slab}[1]{\textrm{#1}} +\newcommand{\semlab}[1]{\text{\scshape{S-#1}}} +\newcommand{\tylab}[1]{\text{\scshape{T-#1}}} +\newcommand{\mlab}[1]{\text{\scshape{M-#1}}} +\newcommand{\siglab}[1]{\text{\scshape{Sig-#1}}} +\newcommand{\klab}[1]{#1} +\newcommand{\revto}{\ensuremath{\leftarrow}} + +\newcommand{\dec}[1]{\mathsf{#1}} +\newcommand{\keyw}[1]{\mathbf{#1}} +\newcommand{\Handle}{\keyw{handle}} +\newcommand{\ShallowHandle}{\ensuremath{\keyw{handle}^\dagger}} +\newcommand{\With}{\keyw{with}} +\newcommand{\Let}{\keyw{let}} +\newcommand{\Rec}{\keyw{rec}} +\newcommand{\In}{\keyw{in}} +\newcommand{\Do}{\keyw{do}} +\newcommand{\Return}{\keyw{return}} +\newcommand{\Val}{\keyw{val}} +\newcommand{\Case}{\keyw{case}} +\newcommand{\If}{\keyw{if}} +\newcommand{\Then}{\keyw{then}} +\newcommand{\Else}{\keyw{else}} +\newcommand{\Absurd}{\keyw{absurd}} +\newcommand{\Record}[1]{\ensuremath{\langle #1 \rangle}} +\newcommand{\Unit}{\Record{}} +\newcommand{\Inl}{\keyw{inl}} +\newcommand{\Inr}{\keyw{inr}} +\newcommand{\Thunk}{\lambda \Unit.} + +\newcommand{\Pre}[1]{\mathsf{Pre}(#1)} +\newcommand{\Abs}{\mathsf{Abs}} +\newcommand{\Presence}{\mathsf{Presence}} +\newcommand{\Row}{\mathsf{Row}} +\newcommand{\Type}{\mathsf{Type}} +\newcommand{\Ground}{\mathsf{ground}} + +\newcommand{\Comp}{\mathsf{Comp}} +\newcommand{\Effect}{\mathsf{Effect}} +\newcommand{\Handler}{\mathsf{Handler}} + +\newcommand{\One}{1} +\newcommand{\Int}{\mathsf{Int}} +\newcommand{\Bool}{\mathsf{Bool}} +\newcommand{\List}{\mathsf{List}} +\newcommand{\Nat}{\mathsf{Nat}} +\newcommand{\Choose}{\dec{Choose}} +\newcommand{\Count}{\dec{count}} +\newcommand{\GenericSearch}{\dec{genericSearch}} +\newcommand{\Predicate}{\dec{Predicate}} +\newcommand{\Point}{\dec{Point}} +\newcommand{\Branch}{\dec{Branch}} +\newcommand{\Get}{\dec{Get}} +\newcommand{\Put}{\dec{Put}} +\newcommand{\Zero}{\dec{Zero}} +\newcommand{\Fail}{\dec{Fail}} + +\newcommand{\True}{\mathsf{true}} +\newcommand{\False}{\mathsf{false}} + +%% Handler projections. +\newcommand{\hret}{H^{\mathrm{val}}} +\newcommand{\hval}{\hret} +\newcommand{\hops}{H^{\mathrm{ops}}} +%\newcommand{\hex}{H^{\mathrm{ex}}} +\newcommand{\hell}{H^{\ell}} diff --git a/thesis.tex b/thesis.tex index 514f8af..e74f750 100644 --- a/thesis.tex +++ b/thesis.tex @@ -1,5 +1,5 @@ %% 12pt font size, PhD thesis, LFCS, print twosided, new chapters on right page -\documentclass[11pt,phd,lfcs,twoside,openright,logo,leftchapter,normalheadings]{infthesis} +\documentclass[12pt,phd,lfcs,twoside,openright,logo,leftchapter,normalheadings]{infthesis} \shieldtype{0} %% Packages @@ -29,6 +29,7 @@ shrink=10]{microtype} \usepackage{enumerate} % Customise enumerate-environments \usepackage{xcolor} % Colours +\usepackage{xspace} % Smart spacing in commands. \usepackage{tikz} \usetikzlibrary{fit,calc,trees,positioning,arrows,chains,shapes.geometric,% decorations.pathreplacing,decorations.pathmorphing,shapes,% @@ -46,6 +47,11 @@ \textquotedblleft={ ,150}, % left quotation mark, space from right \textquotedblright={150, }} % right quotation mark, space from left +%% +%% Load macros. +%% +\include{macros} + %% Information about the title, etc. % \title{Higher-Order Theories of Handlers for Algebraic Effects} % \title{Handlers for Algebraic Effects: Applications, Compilation, and Expressiveness} @@ -159,89 +165,97 @@ Explain conventions\dots \part{Background} \label{p:background} -\chapter{The State of Effectful Programming} +\chapter{The state of effectful programming} \label{ch:related-work} -\section{Type and Effect Systems} -\section{Monadic Programming} +\section{Type and effect systems} +\section{Monadic programming} \chapter{Continuations} \label{ch:continuations} -\section{Zoo of Control Operators} +\section{Zoo of control operators} Describe how effect handlers fit amongst shift/reset, prompt/control, callcc, J, catchcont, etc. -\section{Implementation Strategies} +\section{Implementation strategies} \part{Design} -\chapter{A ML-like Base Language} -\section{Syntax and Static Semantics} -\section{Type Inference} -\section{Dynamic Semantics} +\chapter{A ML-flavoured programming language} +\label{ch:base-language} + +In this chapter we introduce a core calculus, \BCalc, which we shall +later use as the basis for exploration of design considerations for +effect handlers. This calculus distils the functional core of the +\Links programming language~\cite{CooperLWY06}, which is a +ML-flavoured language for multi-tier web-programming. + +\section{Syntax and static semantics} +\section{Type inference} +\section{Dynamic semantics} -\chapter{Unary Handlers} +\chapter{Unary handlers} \label{ch:deep-handlers} -\section{Deep Handlers} -\subsection{Syntax and Static Semantics} +\section{Deep handlers} +\subsection{Syntax and static semantics} \subsection{Effect inference} -\subsection{Dynamic Semantics} +\subsection{Dynamic semantics} -\section{Parameterised Handlers} +\section{Parameterised handlers} -\section{Shallow Handlers} +\section{Shallow handlers} \label{ch:shallow-handlers} -\subsection{Syntax and Static Semantics} -\subsection{Dynamic Semantics} +\subsection{Syntax and static semantics} +\subsection{Dynamic semantics} -\chapter{N-ary Handlers} +\chapter{N-ary handlers} \label{ch:multi-handlers} % \section{Syntax and Static Semantics} % \section{Dynamic Semantics} -\section{Unifying Deep and Shallow Handlers} +\section{Unifying deep and shallow handlers} \part{Implementation} -\chapter{Continuation Passing Styles} -\chapter{Abstract Machine Semantics} +\chapter{Continuation passing styles} +\chapter{Abstract machine semantics} \part{Expressiveness} -\chapter{Computability, Complexity, and Expressivness} +\chapter{Computability, complexity, and expressivness} \label{ch:expressiveness} -\section{Notions of Expressiveness} +\section{Notions of expressiveness} Felleisen's macro-expressiveness, Longley's type-respecting expressiveness, Kammar's typability-preserving expressiveness. -\section{Interdefinability of Deep and Shallow Handlers} -\section{Encoding Parameterised Handlers} +\section{Interdefinability of deep and shallow Handlers} +\section{Encoding parameterised handlers} -\chapter{The Asymptotic Power of Control} +\chapter{The asymptotic power of control} \label{ch:handlers-efficiency} Describe the methodology\dots -\section{Generic Search} +\section{Generic search} \section{Calculi} \subsection{Base calculus} \subsection{Handler calculus} -\section{A Practical Model of Computation} +\section{A practical model of computation} \subsection{Syntax} \subsection{Semantics} \subsection{Realisability} -\section{Points, Predicates, and their Models} -\section{Efficient Generic Search with Effect Handlers} +\section{Points, predicates, and their models} +\section{Efficient generic search with effect handlers} \subsection{Space complexity} -\section{Best-case Complexity of Generic Search without Control} +\section{Best-case complexity of generic search without control} \subsection{No shortcuts} \subsection{No sharing} -\chapter{Robustness of the Asymptotic Power of Control} -\section{Mutable State} -\section{Exception Handling} -\section{Effect System} +\chapter{Robustness of the asymptotic power of control} +\section{Mutable state} +\section{Exception handling} +\section{Effect system} \part{Conclusions}