diff --git a/PragmataPro.ttf b/PragmataPro.ttf new file mode 120000 index 0000000..52ab274 --- /dev/null +++ b/PragmataPro.ttf @@ -0,0 +1 @@ +/home/michael/.local/share/fonts/PragmataPro_Mono_R_liga_0829.ttf \ No newline at end of file diff --git a/csci8980-project.agda-lib b/agda-project.agda-lib similarity index 63% rename from csci8980-project.agda-lib rename to agda-project.agda-lib index e7d169e..7b46da2 100644 --- a/csci8980-project.agda-lib +++ b/agda-project.agda-lib @@ -1,3 +1,3 @@ -name: csci8980-project +name: agda-project depend: standard-library include: ./src diff --git a/main.tex b/main.tex index f4fd755..47f7439 100644 --- a/main.tex +++ b/main.tex @@ -1,93 +1,190 @@ -\documentclass{beamer} +\documentclass[xcolor={dvipsnames}]{beamer} \usepackage[utf8]{inputenc} +\usepackage{relsize} +\usepackage{amsmath} \usepackage{agda} \usepackage{caption} \usepackage{catchfilebetweentags} \usepackage{cite} +\usepackage{fancyvrb} +\usepackage{fontspec} +\usepackage{hyperref} \usepackage{newunicodechar} +\usepackage{setspace} \usepackage{url} -% \usetheme{CambridgeUS} +\usetheme{Berlin} \usecolortheme{lily} \setbeamercovered{transparent} +\newfontfamily\PragmataPro[Extension=.ttf,NFSSFamily=PragmataPro]{PragmataPro} + \usepackage{tikz} \usetikzlibrary{positioning} +\setstretch{1.25} +\fvset{fontfamily=PragmataPro} + +\AtBeginSection[] { + \begin{frame} + \frametitle{\insertsectionhead} + \tableofcontents[currentsection] + \end{frame} +} + \titlegraphic{ \centering \vspace{-1cm} \includegraphics[width=.2\textwidth,height=.35\textheight]{cesk.png} } -\title{First class continuations with CEK machines in Agda} +\title{First class continuations with CEK in Agda} \author{Michael Zhang} \date{} \begin{document} -% \frame{\titlepage} -\begin{frame}[t]\vspace{1cm} +\begin{frame} \maketitle \end{frame} -\section{Primer on CESK} +\section{Background} \begin{frame} \frametitle{What is a CESK machine?} - \begin{itemize}[<+->] + \begin{itemize} \item Abstract machine for interpreters, introduced by Matthias Felleisen. \item Stands for $C$ontrol, $E$nvironment, $S$tore, $K$ontinuation. - \item Based on Matt Might's blog post on CESK machines \cite{might-cesk}. + \item Based on Matt Might's blog post on CESK machines. \end{itemize} \end{frame} \begin{frame} - \frametitle{What are each of the components?} + \frametitle{What do C, E, S, and K mean?} - \begin{itemize}[<+->] + \begin{itemize} \item $C$ontrol is your current term. \item $E$nvironment is a list of addresses. \item $S$tore is a mapping of addresses to values. \item $K$ont is what gets evaluated next. \end{itemize} + + \vspace{.5cm} + + Example on next slide. \end{frame} \begin{frame} - \frametitle{What are continuations?} + \begin{exampleblock}{Example} + \begin{equation*} \begin{split} + \{ C = (\lambda .\:`0 + 2) \cdot 4, E = [], K = [halt] \} \\ + \{ C = (\lambda .\:`0 + 2), E = [4], K = [\lambda .\:`0 \cdot 4, halt] \} \\ + \end{split} \end{equation*} + \end{exampleblock} \end{frame} \begin{frame} - \begin{tikzpicture}[ - roundnode/.style={circle, draw=green!60, fill=green!5, very thick, minimum size=7mm}, - squarednode/.style={rectangle, draw=red!60, fill=red!5, very thick, minimum size=5mm}, - ] - \node[draw, align=left, squarednode](ceskState){ - C = $\lambda x . (\lambda y . x + y)$ \\ - $E$ = [] \\ - $\kappa$ = halt - }; - \node[squarednode](ceskState2)[right=of ceskState]{CEK}; + \frametitle{Why continuations?} - %lines - \draw[->] (ceskState.east) -- (ceskState2.west); - \end{tikzpicture} + \begin{itemize} + \item Useful for implementing other language constructs + \begin{itemize} + \item call/cc + \item Exceptions + \item Mutation + \item Recursion + \end{itemize} + \end{itemize} + + \begin{exampleblock}{Example} + $\color{Plum}4 + \color{black}(\texttt{call/cc} \color{Orange}(\lambda k .\:k\:2)\color{black}) \Rightarrow + \color{Orange}(\lambda k.\:k\:2)\color{black} (\lambda n.\:\color{Plum}4 + \color{black}n) \Rightarrow + 6$ + \end{exampleblock} \end{frame} -\section{Implementation} - \begin{frame} - \frametitle{Hellosu} + \frametitle{A-Normal Form} - \include{./gentex/Project/Cesk.tex} + \begin{itemize} + \item Separates atomic expressions from state-mutating ones + \item Atomic expressions evaluate to values + \item This approach cleans up the implementation a bit + \end{itemize} +\end{frame} + +\section{Agda Implementation} + +\begin{frame}[fragile] + \frametitle{Keeping track of types} + + \begin{Verbatim}[fontsize=\relsize{-3}] + data Aexp (Tω : Type) Context : Type → Set + data Exp (Tω : Type) Context : Type → Set + + data Aexp Tω Γ where + value : ∀ {A} → Value Tω A → Aexp Tω Γ A + zero : Aexp Tω Γ `ℕ + suc : Aexp Tω Γ `ℕ → Aexp Tω Γ `ℕ + `_ : ∀ {A} → Γ ∋ A → Aexp Tω Γ A + ƛ : ∀ {A B : Type} → Exp Tω (Γ , A) B → Aexp Tω Γ (A ⇒ B) + + data Exp Tω Γ where + atomic : ∀ {A} → Aexp Tω Γ A → Exp Tω Γ A + case : ∀ {A} → Aexp Tω Γ `ℕ → Exp Tω Γ A → Aexp Tω Γ (`ℕ ⇒ A) → Exp Tω Γ A + _·_ : ∀ {A B} → Aexp Tω Γ (A ⇒ B) → Aexp Tω Γ A → Exp Tω Γ B + abort : ∀ {A} → Aexp Tω Γ ⊥ → Exp Tω Γ A + _∘_ : ∀ {A} → Aexp Tω Γ K[ A ⇒ ⊥ ] → Aexp Tω Γ A → Exp Tω Γ ⊥ + call/cc : ∀ {A} → Aexp Tω Γ (K[ A ⇒ ⊥ ] ⇒ Tω) → Exp Tω Γ A + \end{Verbatim} +\end{frame} + +\begin{frame}[fragile] + \frametitle{Progress and Preservation} + + \begin{itemize} + \item We get preservation for free. + \item Closed step function gives us progress. + \end{itemize} + + \vspace{.5cm} + + \begin{Verbatim}[fontsize=\relsize{-2}] + data StepResult (A : Type) : Set where + part : State A → StepResult A + done : Value A A → StepResult A + step : ∀ {Tω : Type} → State Tω → StepResult Tω + \end{Verbatim} +\end{frame} + +\begin{frame}[fragile] + \frametitle{Evaluation} + + \begin{Verbatim}[fontsize=\relsize{-2}] + data EvalResult : Set where + complete : ∀ {A} → StepResult A → EvalResult + exhausted : ∀ {A} → State A → EvalResult + + eval′ : ∀ {A} → ℕ → State A → EvalResult + eval′ 0 s = exhausted s + eval′ (suc n) s with step s + ... | part x = eval′ n x + ... | done x = complete $ done x + + eval : ∀ {A} → ℕ → Exp A ∅ A → EvalResult + eval n e = eval′ n (inject e) + \end{Verbatim} \end{frame} \section{Conclusion} \begin{frame} - \frametitle{Resources} - \bibliography{res}{} - \bibliographystyle{plain} + \frametitle{Links} + + \begin{itemize} + \item Source code of this project \url{https://git.sr.ht/~mzhang/agda-project} + \item Matt Might's blog \url{https://matt.might.net/articles/cesk-machines} + \end{itemize} \end{frame} \end{document} diff --git a/res.bib b/res.bib deleted file mode 100644 index 051a316..0000000 --- a/res.bib +++ /dev/null @@ -1,21 +0,0 @@ -@phdthesis{ - felleisen-cesk, - author = "Matthias Felleisen", - howpublished = {\url{https://www2.ccs.neu.edu/racket/pubs/dissertation-felleisen.pdf}}, -} - -@misc{ - might-cesk, - author = "Matt Might", - title = "Writing an interpreter, CESK-style", - howpublished = {\url{https://matt.might.net/articles/cesk-machines}}, -} - -@misc{ - source-code, - author = "Michael Zhang", - title = "First class continuations with CEK machines in Agda", - howpublished = {\url{https://git.sr.ht/~mzhang/csci8980-f21-project}}, -} - -@comment vim: set sw=2 : diff --git a/src/Project/Definitions.agda b/src/Project/Definitions.agda index cb1aad3..8ae34cb 100644 --- a/src/Project/Definitions.agda +++ b/src/Project/Definitions.agda @@ -48,7 +48,7 @@ data Aexp Tω Γ where -- Functions `_ : ∀ {A} → Γ ∋ A → Aexp Tω Γ A - ƛ : ∀ {B} {A : Type} → Exp Tω (Γ , A) B → Aexp Tω Γ (A ⇒ B) + ƛ : ∀ {A B : Type} → Exp Tω (Γ , A) B → Aexp Tω Γ (A ⇒ B) data Exp Tω Γ where abort : ∀ {A} → Aexp Tω Γ ⊥ → Exp Tω Γ A