From 740413ed1b86c5954f46da5f2a3f9cae13a83267 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Thu, 12 Aug 2021 22:37:01 +0100 Subject: [PATCH] Viva slides --- slides/Makefile | 32 +++++++++ slides/viva.bib | 82 +++++++++++++++++++++++ slides/viva.tex | 173 ++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 287 insertions(+) create mode 100644 slides/Makefile create mode 100644 slides/viva.bib create mode 100644 slides/viva.tex diff --git a/slides/Makefile b/slides/Makefile new file mode 100644 index 0000000..a36651e --- /dev/null +++ b/slides/Makefile @@ -0,0 +1,32 @@ +TEXC=pdflatex +CFLAGS=-interaction=nonstopmode -halt-on-error -file-line-error +BIBC=bibtex +PAPER=viva +BIBLIO=$(PAPER) +LATEST_COMMIT=$(shell git log --format="%h" -n 1) + +all: $(PAPER).pdf +draft: $(PAPER).pdf-draft + +$(PAPER).aux: $(PAPER).tex + $(TEXC) $(CFLAGS) $(PAPER) + +$(BIBLIO).bbl: $(PAPER).aux $(BIBLIO).bib + $(BIBC) $(PAPER) + +$(PAPER).pdf: $(PAPER).aux $(BIBLIO).bbl + $(TEXC) $(CFLAGS) $(PAPER) + $(TEXC) $(CFLAGS) $(PAPER) + +$(PAPER).pdf-draft: CFLAGS:=$(CFLAGS) "\def\DRAFT{$(LATEST_COMMIT)}\input{$(PAPER)}" +$(PAPER).pdf-draft: all + mv $(PAPER).pdf $(PAPER)-draft.pdf + tar cf thesis-draft.tar.gz $(PAPER)-draft.pdf + +clean: + rm -f *.log *.aux *.toc *.out + rm -f *.bbl *.blg *.fls *.xml + rm -f *.nav *.snm + rm -f *.fdb_latexmk *.vtc *.cut + rm -f $(PAPER).pdf camera-ready.pdf submission.pdf + rm -f *.o *.cmx *.cmo diff --git a/slides/viva.bib b/slides/viva.bib new file mode 100644 index 0000000..cd18854 --- /dev/null +++ b/slides/viva.bib @@ -0,0 +1,82 @@ +@inproceedings{HillerstromL16, + author = {Daniel Hillerstr{\"{o}}m and + Sam Lindley}, + title = {Liberating effects with rows and handlers}, + booktitle = {TyDe@ICFP}, + pages = {15--27}, + publisher = {{ACM}}, + year = {2016} +} + +@inproceedings{HillerstromLAS17, + author = {Daniel Hillerstr{\"{o}}m and + Sam Lindley and + Robert Atkey and + {KC} Sivaramakrishnan}, + title = {Continuation Passing Style for Effect Handlers}, + booktitle = {{FSCD}}, + series = {LIPIcs}, + volume = {84}, + pages = {18:1--18:19}, + OPTpublisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik}, + year = {2017} +} + +@inproceedings{HillerstromL18, + author = {Daniel Hillerstr{\"{o}}m and + Sam Lindley}, + title = {Shallow Effect Handlers}, + booktitle = {{APLAS}}, + OPTseries = {Lecture Notes in Computer Science}, + series = {{LNCS}}, + volume = {11275}, + pages = {415--435}, + publisher = {Springer}, + year = {2018} +} + +@article{HillerstromLA20, + author = {Daniel Hillerstr{\"{o}}m and + Sam Lindley and + Robert Atkey}, + title = {Effect handlers via generalised continuations}, + journal = {J. Funct. Program.}, + volume = {30}, + pages = {e5}, + year = {2020} +} + +@article{HillerstromLL20, + author = {Daniel Hillerstr{\"{o}}m and + Sam Lindley and + John Longley}, + title = {Effects for Efficiency: Asymptotic Speedup with First-Class Control}, + journal = {Proc. {ACM} Program. Lang.}, + volume = {4}, + number = {{ICFP}}, + pages = {100:1--100:29}, + year = {2020} +} + +# Unix +@article{RitchieT74, + author = {Dennis Ritchie and + Ken Thompson}, + title = {The {UNIX} Time-Sharing System}, + journal = {Commun. {ACM}}, + volume = {17}, + number = {7}, + pages = {365--375}, + year = {1974} +} + +# CEK & C +@InProceedings{FelleisenF86, + title={Control Operators, the {SECD}-machine, and the $\lambda$-Calculus}, + author={Felleisen, Matthias and Friedman, Daniel P.}, + year=1987, + booktitle = {Formal Description of Programming Concepts III}, + OPTbooktitle = {The Proceedings of the Conference on Formal Description of Programming Concepts III, Ebberup, Denmark}, + pages = {193--217}, + OPTpublisher={North Holland} +} \ No newline at end of file diff --git a/slides/viva.tex b/slides/viva.tex new file mode 100644 index 0000000..39faca4 --- /dev/null +++ b/slides/viva.tex @@ -0,0 +1,173 @@ +\documentclass[169,10pt,compress,dvipsnames]{beamer} +%% +%% Slides layout +%% +\beamertemplatenavigationsymbolsempty % hides navigation buttons +\usetheme{Madrid} % standard Madrid theme +\setbeamertemplate{footline}{} % renders the footer empty +% +\setbeamertemplate{bibliography item}{ % this is a hack to prevent Madrid theme + biblatex + \hspace{-0.4cm}\lower3pt\hbox{ % from causing bibliography entries to run over + \pgfuseimage{beamericonarticle} % the slide margins +}} + +%% +%% Packages +%% +\usepackage[utf8]{inputenc} % enable UTF-8 compatible typing +\usepackage{hyperref} % interactive PDF +\usepackage[sort&compress,square,numbers]{natbib} % Bibliography +\usepackage{amsmath,amssymb,mathtools} % maths typesetting +\usepackage{../pkgs/mathpartir} % Inference rules +\usepackage{../pkgs/mathwidth} % renders character sequences nicely in math mode +\usepackage{stmaryrd} % semantic brackets +\usepackage{xspace} % proper spacing for macros in text + +\usepackage[T1]{fontenc} % 8-bit font encoding + % native support for accented characters. +\usepackage[scaled=0.85]{beramono} % smoother typewriter font +\newcommand*{\Scale}[2][4]{\scalebox{#1}{\ensuremath{#2}}}% + +\input{../macros.tex} + +%% +%% Meta information +%% +\author{Daniel Hillerström} +\title{Foundations for Programming and Implementing Effect Handlers} +\institute{The University of Edinburgh, Scotland UK} +\subtitle{PhD viva} +\date{August 13, 2021} + +%% +%% Slides +%% +\begin{document} + +% +% Title slide +% +\begin{frame} + \maketitle +\end{frame} + +% Dissertation overview +\begin{frame} + \frametitle{My dissertation at glance} +\end{frame} + +\begin{frame} + \frametitle{Calculi for deep, shallow, and parameterised handlers} + + The calculi capture key aspects of the implementation of effect + handlers in Links. + + \begin{itemize} + \item $\HCalc$ ordinary deep handlers (fold). + \item $\SCalc$ shallow handlers (case-split). + \item $\HPCalc$ parameterised deep handlers (fold+state). + \end{itemize} + + The actual implementation is the union of the three calculi. +\end{frame} + +% UNIX +\begin{frame} + \frametitle{Effect handlers as composable operating systems} + + An interpretation of \citeauthor{RitchieT74}'s + UNIX~\cite{RitchieT74} in terms of effect handlers.\\[2em] + + \[ + \bl + \!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\textbf{Basic idea} + \ba[m]{@{\qquad}r@{~}c@{~}l} + \text{\emph{system call}} &\approx& \text{\emph{operation invocation}}\\ + \text{\emph{system call implementation}} &\approx& \text{\emph{operation interpretation}} + \ea + \el + \]\hfill\\[2em] + + \textbf{Key point} Legacy code is modularly retrofitted with functionality. +\end{frame} + +% CPS translation +\begin{frame} + \frametitle{CPS transforms for effect handlers} + + A higher-order CPS transform for effect handlers with generalised + continuations.\\[1em] + + \textbf{Generalised continuation} Structured representation of + delimited continuations.\\[0.5em] + + \[ + \Scale[1.8]{\kappa = \overline{(\sigma, (\hret,\hops))}} + \]\\[1em] + + \textbf{Key point} Separate the \emph{doing} layer ($\sigma$) from the \emph{being} layer ($H$). +\end{frame} + +% Abstract machine +\begin{frame} + \frametitle{Abstract machine semantics for effect handlers} + + Plugging generalised continuations into \citeauthor{FelleisenF86}'s + CEK machine~\cite{FelleisenF86} yields a runtime for effect + handlers.\\[2em] + + \[ + \Scale[2]{\cek{C \mid E \mid K = \overline{((H,E), \sigma)}}} + \] + +\end{frame} + +% Interdefinability of handlers +\begin{frame} + \frametitle{Interdefinability of effect handlers} + + Deep, shallow, and parameterised handlers are interdefinable + w.r.t. to typability-preserving macro-expressiveness. + + \begin{itemize} + \item Deep as shallow, $\mathcal{D}\llbracket - \rrbracket$, image is lightweight. + \item Shallow as deep, $\mathcal{S}\llbracket - \rrbracket$, image is computationally expensive. + \item Parameterised as deep, $\mathcal{P}\llbracket - \rrbracket$, + image uses explicit state-passing. + \end{itemize} +\end{frame} + +% Asymptotic speed up with first-class control +\begin{frame} + \frametitle{Asymptotic speed up with effect handlers} + + Effect handlers can make some programs faster! + + \[ + \Count_n : ((\Nat_n \to \Bool) \to \Bool) \to \Nat + \]\\[1em] + % + Using type-respecting expressiveness + \begin{itemize} + \item There \textbf{exists} an implementation of $\Count_n \in \HPCF$ with + effect handlers such that the runtime for every $n$-standard predicate $P$ is + $\Count_n~P = \BigO(2^n)$. + \item Forall implementations of $\Count_n \in \BPCF$ the runtime for every $n$-standard predicate $P$ is $\Count_n~P = \Omega(n2^n)$ + \end{itemize} +\end{frame} + +% Background +\begin{frame} + \frametitle{Continuations literature review} +\end{frame} + +% +% References +% +\begin{frame}%[allowframebreaks] + \frametitle{References} + \nocite{*} + \bibliographystyle{plainnat} + \bibliography{\jobname} +\end{frame} +\end{document} \ No newline at end of file