main.tex

%%----------------------------------------------------------------------------------------
%	PACKAGES AND OTHER DOCUMENT CONFIGURATIONS
%----------------------------------------------------------------------------------------

\documentclass[
		twoside,openright,titlepage,numbers=noenddot,headinclude,%1headlines,
                footinclude=true,cleardoublepage=empty,
                BCOR=10mm,paper=a4,fontsize=10pt, % Binding correction, paper type and font size
                ngerman,american, % Languages
                ]{scrreprt}

% Includes the file which contains all the document configurations and packages - make sure to edit this file
\input{classicthesis-config}
\usepackage{semantic}
\usepackage{paralist}
\usepackage{etoolbox}
\usepackage{stmaryrd}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{enumitem}

\newcounter{mythmcounter}
\newcounter{mydefcounter}
\newcounter{myexpcounter}
\newtheorem{example}[myexpcounter]{Example}
\newtheorem{remark}[mythmcounter]{Remark}
\newtheorem{definition}[mydefcounter]{Definition}
\newtheorem{theorem}[mythmcounter]{Theorem}
\newtheorem{lemma}[mythmcounter]{Lemma}
\newtheorem{proposition}[mythmcounter]{Proposition}
\newtheorem*{lemma*}{Lemma}

% Formatting for source code & types
\definecolor{cmtclr}{rgb}{0.0,0.6,0.0}
\definecolor{kvdclr}{rgb}{0.0,0.0,0.6}
\definecolor{numclr}{rgb}{0.0,0.4,0.0}
\definecolor{strclr}{rgb}{0.4,0.3,0.0}
\definecolor{prepclr}{rgb}{0.6,0.0,0.2}

\newcommand{\sep}[0]{\; | \;}
\newcommand{\kvd}[1]{\textnormal{\textcolor{kvdclr}{\ttfamily #1}}}
\newcommand{\num}[1]{\textcolor{numclr}{#1}}
\newcommand{\str}[1]{\textnormal{\textcolor{strclr}{\ttfamily "#1"}}}
\newcommand{\strf}[1]{\textnormal{\textcolor{strclr}{\ttfamily #1}}}
\newcommand{\prepk}[1]{\textnormal{\textcolor{prepclr}{\ttfamily #1}}}
\newcommand{\prepi}[1]{\textnormal{\textcolor{prepclr}{\ttfamily #1}}}
\newcommand{\ident}[1]{\textnormal{\ttfamily #1}}
\newcommand{\cmt}[1]{\textit{\ttfamily\textcolor{cmtclr}{#1}}}

\newcommand{\ctyp}[2]{C^{#1}#2}
\newcommand{\mtyp}[2]{M^{#1}#2}
\newcommand{\subst}[3]{#1[#2 \leftarrow #3]}

% Typing rule and typing statement (single line)
\newcommand{\tyrule}[3]{ \inference[\footnotesize{(\emph{#1})}~~]{#2}{#3} }
\newcommand{\tyruler}[3]{ \inference{#2}{#3}~~\footnotesize{(\emph{#1})} }

% Coeffect algebra
\definecolor{aclr}{rgb}{0.6,0.3,0.0}
\newcommand{\aclrd}[1]{\textcolor{aclr}{#1}}

% Coeffect algebra
\definecolor{cclr}{rgb}{0.0,0.5,0.0}
\newcommand{\cclrd}[1]{\textcolor{cclr}{#1}}

% Red color
\definecolor{rclr}{rgb}{0.75,0.0,0.0}
\newcommand{\rclrd}[1]{\textcolor{rclr}{#1}}

\newcommand{\czero}{ \textcolor{cclr}{ \mathtt{ign} } }
\newcommand{\cunit}{ \textcolor{cclr}{ \mathtt{use} } }
\newcommand{\cseq}{ \textcolor{cclr}{ \circledast }}
\newcommand{\cpar}{ \textcolor{cclr}{\oplus} }
\newcommand{\czip}{ \textcolor{cclr}{\wedge} } % only used by flat coeffects
\newcommand{\cleq}{ \textcolor{cclr}{\leq} }
\newcommand{\cgeq}{ \textcolor{cclr}{\geq} }

\newcommand{\vtimes}{ \mathbin{+\mkern-10mu+} }

\newcommand{\atimes}{ \textcolor{aclr}{\mathbin{+\mkern-10mu+}} }
\newcommand{\aseq}{ \textcolor{aclr}{\circledast}} % Should be the same as \cseq
\newcommand{\aparstr}{ \textcolor{aclr}{\oplus}} % Should be the same as \cseq

% Unified

\newcommand{\SH}{ {\textcolor{sclr}{S}} }
\newcommand{\SP}{ {\textcolor{sclr}{P}} }
\newcommand{\SHP}{ {\textcolor{sclr}{S\triangleright P}} }
\newcommand{\sempty}{ {\textcolor{sclr}{ \hat{0}}} }
\newcommand{\sunit}{ {\textcolor{sclr}{\hat{1}}} }
\newcommand{\stimes}{ {\textcolor{sclr}{\diamond}} }
\newcommand{\sflat}{\star}

\newcommand{\azero}{ \textcolor{aclr}{\bot} }
\newcommand{\aunit}{ \alift{\cunit} }
\newcommand{\aweak}{ \alift{\czero} }

\newcommand{\azip}{ \textcolor{aclr}{ \mathbin{\rotatebox[origin=c]{180}{$\perp$}\mkern-10mu\rotatebox[origin=c]{180}{$\perp$}} } }
\newcommand{\apar}{ \textcolor{aclr}{ \mathbin{\perp\mkern-10mu\perp} } }


\newcommand{\xtimes}{\hat{\times}}

\newcommand{\ctx}{\textit{ctx}}


% Ordinary context where colouring is done by hand
\newcommand{\coctx}[2]{ #1 \,\text{\scriptsize @}\, {{\text{$#2$}}}  }

% Simple coeffect systems in the introduction
\newcommand{\cons}{\hspace{-0.15em}\times\hspace{-0.25em}} %\sctxclrd{+\hspace{-0.55em}+}}

\newcommand{\alift}[1]{ \textcolor{aclr}{\langle} #1 \textcolor{aclr}{\rangle}}

\definecolor{sclr}{rgb}{0.2,0,0.8}
\newcommand{\sclrd}[1]{ \textcolor{sclr}{#1} }

\newcommand{\C}{ {\textcolor{cclr}{\mathcal{C}}} }
\newcommand{\M}{ {\textcolor{cclr}{\mathcal{M}}} }

\newcommand{\alen}[1]{{\aclrd{\textit{len}(}#1\aclrd{)}}}
\newcommand{\slen}[1]{{\sclrd{\textit{len}(}#1\sclrd{)}}}
\newcommand{\xlen}[1]{{\textit{len}(#1)}}

\newcommand{\reduce}{\longrightarrow}


\newcommand{\restr}[2]{#1|_{#2}}
\newcommand{\narrow}[1]{\hspace{-0.5em} #1 \hspace{-0.65em}~}


\definecolor{todoclr}{rgb}{0.8,0,0.5}
\newcommand{\todo}[1]{\textcolor{todoclr}{ \begin{quotation} \noindent\textbf{TODO:} #1 \end{quotation} }}

\newcommand{\sem}[1]{\llbracket #1 \rrbracket}
\newcommand{\catc}{\mathcal{C}}
\newcommand{\idf}[1]{ {\textnormal{\ttfamily id}}_{#1} }

\urlstyle{tt}

\newcommand{\figcaption}[1]{
  \vspace{0.5em}
  \noindent\makebox[\linewidth]{\rule{\textwidth}{0.5pt}}
  \vspace{-2em}
  \caption{#1}
}

% For definining semantics of things over a typing derivation
\newcommand{\semdef}[2]{
\begin{array}{rcl}
  ~ & ~ & ~ \\ \cline{1-1}\cline{3-3}
  \sem{#1} & = & #2 \\
\end{array}
}
\newcommand{\semdeff}[4]{
\begin{array}{rcl}
  \sem{#1} & = & #3 \\ \cline{1-1}\cline{3-3}
  \sem{#2} & = & #4 \\
\end{array}
}
\newcommand{\mdeff}[4]{
\begin{array}{rcl}
  #1 & = & #3 \\ \cline{1-1}\cline{3-3}
  #2 & = & #4 \\
\end{array}
}
\newcommand{\emdeff}[4]{
\begin{array}{rcl}
  \sem{#1} & = & #3 \\ \cline{1-1}\cline{3-3}
  #2 & = & #4 \\
\end{array}
}
\newcommand{\semdefff}[6]{
\begin{array}{rcl}
  \sem{#1} & = & #4 \\
  \sem{#2} & = & #5 \\ \cline{1-1}\cline{3-3}
  \sem{#3} & = & #6 \\
\end{array}
}
\newcommand{\emdefff}[6]{
\begin{array}{rcl}
  \sem{#1} & = & #4 \\
  \sem{#2} & = & #5 \\ \cline{1-1}\cline{3-3}
  #3 & = & #6 \\
\end{array}
}

% Half line spacing around align
\newcommand{\zerodisplayskips}{%
  \setlength{\abovedisplayskip}{0.5em}
  \setlength{\belowdisplayskip}{0.5em}
  \setlength{\abovedisplayshortskip}{0.5em}
  \setlength{\belowdisplayshortskip}{0.5em}}
\appto{\normalsize}{\zerodisplayskips}
\appto{\small}{\zerodisplayskips}
\appto{\footnotesize}{\zerodisplayskips}

% half line spacing around compactitem
\setlength{\pltopsep}{0.5em}
\setlength{\plitemsep}{0.3em}


\begin{document}
\setcounter{page}{3}

\frenchspacing % Reduces space after periods to make text more compact

\raggedbottom % Makes all pages the height of the text on that page

\selectlanguage{american} % Select your default language - e.g. american or ngerman

%\renewcommand*{\bibname}{new name} % Uncomment to change the name of the bibliography
%\setbibpreamble{} % Uncomment to include a preamble to the bibliography - some text before the reference list starts

%\pagenumbering{roman} % Roman page numbering prior to the start of the thesis content (i, ii, iii, etc)

\pagestyle{plain} % Suppress headers for the pre-content pages

%----------------------------------------------------------------------------------------
%	PRE-CONTENT THESIS PAGES
%----------------------------------------------------------------------------------------

%\include{text/Titlepage} % Main title page

%\cleardoublepage\include{text/Declaration} % Publications from the thesis page

\cleardoublepage\include{text/Abstract} % Abstract page

\cleardoublepage\include{text/Acknowledgements} % Publications from the thesis page

\pagestyle{scrheadings} % Show chapter titles as headings

\cleardoublepage\include{text/Contents} % Contents, list of figures/tables/listings and acronyms

%\pagenumbering{arabic} % Arabic page numbering for thesis content (1, 2, 3, etc)
%\setcounter{page}{90} % Uncomment to manually start the page counter at an arbitrary value (for example if you wish to count the pre-content pages in the page count)

\cleardoublepage % Avoids problems with pdfbookmark

% ==================================================================================================

\ctparttext{  The computing ecosystem is becoming increasingly heterogeneous and rich. Modern
  programs need to run on a variety of devices that are all different, but provide unique rich
  capabilities. For example, an application running on a phone can access the GPS sensor, while
  a service running in the cloud can access GPU computing resources. Both diversity and richness
  can only be expected to increase with trends such as the internet of things.

  In this thesis, we argue that creating programming languages that allow the programmer to
  better work with the environment or \emph{context} in which applications execute is the next
  big challenge for programming language designers.

  We start with a detailed discussion of the motivation for the thesis and an overview of our
  methodology (Chapter~\ref{ch:intro}). Next, we discuss previous programming language research that
  leads to the work presented in this thesis (Chapter~\ref{ch:pathways}) and we examine a number
  of practical context-aware systems in detail (Chapter~\ref{ch:applications}), identifying two
  kinds of context that we later capture by \emph{flat} and \emph{structural coeffects}.
}
\part{Context-aware programming}
\label{part:context-aware}

\include{text/Chapter01}
\include{text/Chapter02}
\include{text/Chapter03}

% ==================================================================================================

\ctparttext{In this part, we capture the similarities between the concrete context-aware languages
  presented in the previous chapter. We also develop the key novel technical contributions of
  the thesis. We define a \emph{flat coeffect type system} (Chapter~\ref{ch:flat}) that is
  parameterized by a \emph{coeffect algebra} and a mechanism for choosing unique typing derivation.
  We instantiate a coeffect type system with a concrete coeffect algebra and procedure for choosing
  unique typing derivation for three languages to capture dataflow, implicit parameters and liveness.

  The type system is complemented with a translational semantics for coeffect-based context-aware
  programming languages (Chapter~\ref{ch:semantics}). The semantics is inspired by a categorical
  model based on \emph{indexed comonads} and it translates a source context-aware program into a
  target program in a simple functional language with comonadically-inspired primitives. We give a
  concrete definition of the primitives for dataflow, implicit parameters and liveness and
  present a syntactic safety proof for these three languages.

  The following page provides a detailed overview of the content of Chapters~\ref{ch:flat} and
  Chapters~\ref{ch:semantics}, highlighting the split between general definitions and properties
  (about the coeffect calculus) and concrete definitions and properties (about concrete
  context-awre language). Chapter~\ref{ch:structural} mirrors the same development for
  \emph{structural coeffect systems}.
}
\part{Coeffect calculi}
\label{part:coeffect-calculi}

% --------------------------------------------------------------------------------------------------

\begin{center}
\begin{tabular}{ | l | l | l |}
\hline
\multicolumn{3}{ | c | }{\spacedlowsmallcaps{Chapter 4}} \\ \hline \hline
\hspace{7.1em} & \textsc{Coeffect calculus} \hspace{2.5em} & \textsc{Language-specific} \hspace{6.9em} \\ \hline
\textsc{Syntax}
  & \hspace{-0.5em}\begin{tabular}{l} Coeffect $\lambda$-calculus \\[-0.3em] (Section~\ref{sec:flat-calculus}) \end{tabular}
  & \hspace{-0.5em}\begin{tabular}{l} Extensions such as \\[-0.3em] \ident{?param} and \kvd{prev} \\[-0.3em] (Section~\ref{sec:flat-calculus-examples})  \end{tabular} \\ \hline
\textsc{Type system}
  & \hspace{-0.5em}\begin{tabular}{l} Abstract coeffect \\[-0.3em] algebra (Section~\ref{sec:flat-calculus-algebra})  \end{tabular}
  & \hspace{-0.5em}\begin{tabular}{l} Concrete instances \\[-0.3em] of the coeffect algebra \\[-0.3em] (Section~\ref{sec:flat-calculus-examples})  \end{tabular} \\
\hline
  & \hspace{-0.5em}\begin{tabular}{l} Coeffect type system \\[-0.3em] parameterized by \\[-0.3em] the coeffect algebra \\[-0.3em] (Section~\ref{sec:flat-calculus-types})  \end{tabular}
  & \hspace{-0.5em}\begin{tabular}{l} Typing for language- \\[-0.3em] specific extensions \\[-0.3em] (Section~\ref{sec:flat-calculus-examples})  \end{tabular} \\
\hline
  &
  & \hspace{-0.5em}\begin{tabular}{l} Procedure for determining \\[-0.3em] a unique typing derivation \\[-0.3em]  (Section~\ref{sec:flat-unique})  \end{tabular} \\ \hline
\textsc{Properties}
  & \hspace{-0.5em}\begin{tabular}{l} Syntactic properties \\[-0.3em] of coeffect $\lambda$-calculus \\[-0.3em] (Section~\ref{sec:flat-syntax})  \end{tabular}
  & \hspace{-0.5em}\begin{tabular}{l} Uniqueness of the above \\[-0.3em]  (Section~\ref{sec:flat-unique})  \end{tabular} \\ \hline
\end{tabular}
\end{center}

~

\begin{center}
\begin{tabular}{ | l | l | l |}
\hline
\multicolumn{3}{ | c | }{\spacedlowsmallcaps{Chapter 5}} \\ \hline \hline
& \textsc{Coeffect calculus} & \textsc{Language-specific} \\ \hline
\textsc{Categorical}
  & \hspace{-0.5em}\begin{tabular}{l} Indexed comonads \\[-0.3em] (Section~\ref{sec:semantics-flat-idx}) \end{tabular}
  & \hspace{-0.5em}\begin{tabular}{l} Examples including indexed \\[-0.3em] product, list and maybe \\[-0.3em] comonads (Section~\ref{sec:semantics-flat-monoidal}) \end{tabular} \\
\hline
  & \hspace{-0.5em}\begin{tabular}{l} Categorical semantics \\[-0.4em] of coeffect $\lambda$-calculus \\[-0.3em] (Section~\ref{sec:semantics-flat-calculus}) \end{tabular}
  & \\ \hline
\textsc{Translational}
  & \hspace{-0.5em}\begin{tabular}{l} Functional target \\[-0.3em] language (Section~\ref{sec:semantics-translation-target}) \end{tabular}
  &  \\
\hline
  & \hspace{-0.5em}\begin{tabular}{l} Translation from coeffect \\[-0.3em] $\lambda$-calculus to target \\[-0.3em]  language (Section~\ref{sec:semantics-translation-transl}) \end{tabular}
  & \hspace{-0.5em}\begin{tabular}{l} Translation for language-\\[-0.3em] specific extensions (\kvd{prev}, \ident{?p}) \\[-0.3em] (Sections~\ref{sec:semantics-proofs-df} and \ref{sec:semantics-proofs-impl}) \end{tabular} \\ \hline
\textsc{Operational}
  & \hspace{-0.5em}\begin{tabular}{l} Abstract comonadically- \\[-0.3em] inspired primitives \\[-0.3em] (Section~\ref{sec:semantics-translation-transl}) \end{tabular}
  & \hspace{-0.5em}\begin{tabular}{l} Concrete reduction rules for \\[-0.3em] comonadically-inspired primitives \\[-0.3em] (Sections~\ref{sec:semantics-proofs-df} and \ref{sec:semantics-proofs-impl}) \end{tabular} \\
\hline
  &
  & \hspace{-0.5em}\begin{tabular}{l} Reduction rules for language-\\[-0.3em] specific extensions (\kvd{prev}, \ident{?p}) \\[-0.3em] (Sections~\ref{sec:semantics-proofs-df} and \ref{sec:semantics-proofs-impl}) \end{tabular} \\
\hline
  & \hspace{-0.5em}\begin{tabular}{l} Sketch of generalized \\[-0.3em] syntactic soundness \\[-0.3em] (Section~\ref{sec:semantics-generalising}) \end{tabular}
  & \hspace{-0.5em}\begin{tabular}{l} Syntactic soundness \\[-0.3em] (Sections~\ref{sec:semantics-proofs-df} and \ref{sec:semantics-proofs-impl}) \end{tabular} \\ \hline
\end{tabular}
\end{center}

% --------------------------------------------------------------------------------------------------

\include{text/Chapter04}
\include{text/Chapter05}
\include{text/Chapter06}

% ==================================================================================================

\ctparttext{ In the first part of the thesis, we argued for the importance of \emph{context} in
  programming languages. As programs execute in increasingly diverse and rich environments,
  languages need to understand and check how programs use such context. In the second part, we
  developed theoretical foundations (type system and semantics) for context-aware programming
  languages. What remains to be done if context-aware programming languages are to become
  ``the next big thing''?

  In this part, we explore practical aspects of implementing context-aware programming languages
  based on coeffects and related future work. We discuss a prototype implementation (Chapter~\ref{ch:impl}),
  which links together all parts of the theory discussed in the previous part. Building a
  production-ready programming language is outside the scope of the thesis, so we instead focus
  on conveying the concept of coeffects to broader audience and make the implementation available
  as a web-based interactive essay (Section~\ref{sec:impl-essay}) at: \url{http://tomasp.net/coeffects}.

  In Chapter~\ref{ch:further}, we outline unification of flat and structural
  coeffects (Section~\ref{sec:further-unified}), which may be more suited for embedding in practical
  languages and we discuss alternative approaches for using coeffects in programming languages
  (Section~\ref{sec:further-meta}).
}

\part{Towards practical coeffects}
\label{part:context-aware}

\include{text/Chapter07}
\include{text/Chapter08}
\include{text/Chapter09}

% ==================================================================================================

\cleardoublepage
\include{Bibliography}

% --------------------------------------------------------------------------------------------------

\appendix
\include{text/AppendixA}
\include{text/AppendixB}

\end{document}