add initial main.tex

paper/main.tex

@@ -0,0 +1,697 @@
+\documentclass[10pt, nonacm]{acmart}
+
+\usepackage[utf8]{inputenc}
+\usepackage{formal-grammar}
+\usepackage[dvipsnames]{xcolor}
+\usepackage{mathpartir}
+
+
+\newcommand{\metavariable}[1]{\textcolor{teal}{#1}}
+\newcommand{\typeterminal}[1]{\textcolor{brown}{#1}}
+\newcommand{\exprterminal}[1]{\textcolor{Sepia}{#1}}
+
+\newcommand{\seltype}[0]{ {\textsc{\footnotesize{Typ}}} }
+\newcommand{\selexpr}[0]{ {\textsc{\footnotesize{Exp}}} }
+\newcommand{\selval}[0]{ {\textsc{\footnotesize{Val}}} }
+
+\newcommand{\exprvars}[0]{ V }
+\newcommand{\typevars}[0]{ \Upsilon }
+\newcommand{\typenames}[0]{ \Sigma }
+
+\newcommand{\typenonterm}[1]{ \nonterm{ T_\seltype \footnotesize{\textsf{$(\typenames, #1)$}}}}
+\newcommand{\exprnonterm}[2]{ \nonterm{ T_\selexpr \footnotesize{\textsf{$(\typenames, #1, #2)$}}}}
+\newcommand{\valnonterm}[2]{ \nonterm{ T_\selval \footnotesize{\textsf{$(\typenames, #1, #2)$}}}}
+
+
+\newcommand{\todo}[1]{ {\textcolor{red}{\textbf{TODO:} #1}} }
+
+\title{A functional core calculus with ladder-types}
+\author{Michael Sippel}
+\email{michael.sippel@mailbox.tu-dresden.de}
+
+\makeatletter
+\let\@authorsaddresses\@empty
+\makeatother
+\begin{document}
+
+
+\begin{abstract}
+This paper presents a minimal core calculus extending the \(\lambda\)-calculus by a polymorphic type-system similar to SystemF, but in addition it introduces a new type-constructor called the \emph{ladder-type}.
+Using ladder-types, multi-layered embeddings of higher-level data-types into lower-level data-types can be described by a type-level structure.
+By facilitating automatic transformations between semantically compatible datatypes, ladder-typing opens up a new paradigm of abstraction.
+We formally define the syntax \& semantics of this calculus and prove its \emph{type soundness}.
+Further we show how the Boehm-Berarducci encoding can be used to implement algebraic datatypes on the basis of the introduced core calculus.
+\end{abstract}
+
+\maketitle
+\tableofcontents
+
+
+%\newpage
+\section{Core Calculus}
+\subsection{Syntax}
+
+The calculus is made up of a \emph{type-level} language, and an \emph{expression-level} language. The formal grammar for both is given in \ref{gr:core}.
+In addition to \emph{function types} \(\tau_1 \rightarrow \tau_2\), \emph{universal types} \(\forall\alpha.\tau\) and type specialization \(<\tau_1 \tau_2>\),
+which are already known from SystemF,
+types can be of the form \(\tau_1 \sim \tau_2\) to denote a \emph{ladder type} to formalizes the notion of a type \(\tau_1\) being represented in terms of type \(\tau_2\).
+Similar to SystemF, expressions can be \emph{variables}, \emph{type-abstractions}, \emph{}
+
+\begin{figure}[h]
+\label{gr:core}
+
+\begin{grammar}
+\firstcase{ T_\seltype \textsf{$(\typenames, \typevars)$} }{
+	\metavariable{\sigma}
+}{Type Literal \quad \textsf{where $ \metavariable{\sigma} \in \typenames $}}
+
+\otherform{
+   \metavariable{\alpha}
+}{Type Variable \quad \textsf{where $ \metavariable{\alpha} \in \typevars $}}
+
+\otherform{
+	$$\typeterminal{\forall}$$ \metavariable{\alpha} \typeterminal{.} \quad \typenonterm{\typevars \cup \{\metavariable{\alpha}\}}
+}{Universal Type}
+
+\otherform{
+	\typeterminal{<} \typenonterm{\typevars} \quad \typenonterm{\typevars} \typeterminal{>}
+}{Specialization}
+
+\otherform{
+	\typenonterm{\typevars}
+	\quad $$\typeterminal{\rightarrow}$$ \quad
+	\typenonterm{\typevars}
+}{Function Type}
+
+\otherform{
+	\typenonterm{\typevars}
+	\quad $$\typeterminal{\rightarrow_{morph}}$$ \quad
+	\typenonterm{\typevars}
+}{Morphism Type}
+
+\otherform{
+	\typenonterm{\typevars}
+	\quad $$\typeterminal{\sim}$$ \quad
+	\typenonterm{\typevars}
+}{Ladder Type}
+
+\otherform{
+	$$\typeterminal{(}$$ \quad
+	\typenonterm{\typevars}
+    \quad $$\typeterminal{)}$$
+}{Parenthesis}
+
+
+
+
+$$\\$$
+
+
+
+\firstcase{ T_\selexpr \textsc{$(\typenames, \typevars, \exprvars)$} }
+	{ \metavariable{x}
+} {Variable \quad \textsf{where $\metavariable{x} \in \exprvars$} }
+
+\otherform{
+	$$ \exprterminal{\Lambda} \metavariable{\alpha}
+	\quad \exprterminal{\mapsto} \quad $$
+	\exprnonterm{\typevars \cup \{\metavariable{\alpha}\}}{\exprvars}
+}{Type Abstraction}
+
+\otherform{
+	$$ \exprterminal{\lambda} \metavariable{x} $$
+	\exprterminal{:} \typenonterm{\typevars}
+    \quad $$\exprterminal{\mapsto}$$ \quad
+	\exprnonterm{\typevars}{\exprvars \cup \{\metavariable{x}\}}
+}{Value Abstraction}
+
+\otherform{
+	$$ \exprterminal{\lambda} \metavariable{x} $$
+	\exprterminal{:} \typenonterm{\typevars}
+    \quad $$\exprterminal{\mapsto_{morph}}$$ \quad
+	\exprnonterm{\typevars}{\exprvars \cup \{\metavariable{x}\}}
+}{Value Morphism}
+
+\otherform{
+	\exprterminal{let} \quad \metavariable{x} \quad \exprterminal{=} \quad 
+	\exprnonterm{\typevars}{\exprvars}
+	\quad \exprterminal{in} \quad
+	\exprnonterm{\typevars}{\exprvars \cup \{\metavariable{x}\}}
+}{Variable Binding}
+
+\otherform{
+    \exprnonterm{\typevars}{\exprvars}
+	\quad
+    \typenonterm{\typevars}
+}{Type Application}
+
+\otherform{
+    \exprnonterm{\typevars}{\exprvars}
+	\quad
+    \exprnonterm{\typevars}{\exprvars}
+}{Value Application}
+
+\otherform{
+    \exprnonterm{\typevars}{\exprvars}
+	\quad
+	\exprterminal{as}
+	\quad
+    \typenonterm{\typevars}
+}{Type Cast}
+
+\otherform{
+	\exprterminal{(} \quad
+    \exprnonterm{\typevars}{\exprvars}
+	\quad \exprterminal{)}
+}{Parenthesis}
+
+
+$$\\$$
+
+\firstcase{ T_\textsc{Val} \textsc{$(\typenames, \typevars, \exprvars)$} }{
+    \exprterminal{\epsilon}
+}{Empty Value}
+
+\otherform{
+    \metavariable{x} \quad \valnonterm{\typevars}{\exprvars}
+}{Value Conactenation}
+
+%\otherform{
+%	\exprterminal{\Lambda} \metavariable{\alpha} \quad
+%	\exprterminal{\mapsto} \quad
+%	\valnonterm{ \typevars \cup \{ \metavariable{\alpha} \} }
+%}{Type-Function Value}
+
+\otherform{
+	\exprterminal{\lambda} \metavariable{x} \quad
+	\exprterminal{:} \quad
+	\typenonterm{\emptyset} \quad
+	\exprterminal{\mapsto} \quad
+	\exprnonterm{\typevars}{\{\metavariable{x}\}}
+}{Function Value}
+
+\otherform{
+	\valnonterm{ \typevars } \quad
+	\exprterminal{as} \quad
+	\typenonterm{ \typevars }
+}{Value}
+
+\end{grammar}
+
+
+
+\caption{Syntax of the core calculus with colors for \metavariable{metavariables}, \typeterminal{type-level terminal symbols}, \exprterminal{expression-level terminal symbols}
+where $\typenames, \typevars, \exprvars$ are mutually disjoint, countable sets of symbols to denote atomic type identifiers (\(\typenames\)), free typevariables (\(\typevars\)), and free expression variables (\(\exprvars\)).
+$$\\$$}
+
+\end{figure}
+
+\begin{example}
+\label{ex:terms}
+Let \(\Sigma = \{ \text{Digit}, \text{Char}, \text{Seq}, \text{UTF-8}, \mathbb{N}, PosInt \} \cup \{ 0, 1, 2, ... \}\).
+The following terms are valid types over \(\Sigma\):
+
+\begin{enumerate}
+\item \typeterminal{<Seq Char>} \( \in \typenonterm{\emptyset}\)\\
+"sequence of characters"
+\item \typeterminal{<Seq <Digit 10> \(\sim\) Char>} \( \in \typenonterm{\emptyset}\)\\
+"sequence of decimal digits, where each digit is represented as character"
+\item \typeterminal{<Seq Item> \(\rightarrow \mathbb{N} \rightarrow\) Item} \( \in \typenonterm{\{Item\}}\)\\
+"function that maps a sequence of items and a natural number to an item"\\
+Note: this type contains the free variable \typeterminal{Item}
+\item \typeterminal{<Seq Char> \(\sim\) UTF-8 \(\rightarrow \mathbb{N} \rightarrow\) Char } \( \in \typenonterm{\emptyset}\)\\
+"function that takes a sequence of chars, represented as UTF-8 string, and a natural number to return a character"
+\item \typeterminal{\(\forall\) Radix . <Seq <Digit Radix> \(\sim\) Char>} \(\in \typenonterm{\emptyset} \)\\
+"given the parameter \typeterminal{Radix}, a sequence of digits where each digit is represented as character"\\
+Note: this type-term is \emph{ground} (i.e. \(\typevars = \emptyset\)), since \typeterminal{Radix} is bound by \(\typeterminal{\forall}\)
+\item \typeterminal{
+	\(\forall\) SrcRadix.\\
+	\(\forall\) DstRadix.\\
+	\(\mathbb{N} \sim\) <PosInt SrcRadix> \(\sim\) <Seq <Digit SrcRadix> \(\sim\) Char>\\
+	\(\rightarrow_{morph}\)\\
+	\(\mathbb{N} \sim\) <PosInt DstRadix> \(\sim\) <Seq <Digit DstRadix> \(\sim\) Char>\\
+} \(\in \typenonterm{\emptyset} \)\\
+"morphism function that maps the \typeterminal{PosInt} representation of \(\typeterminal{\mathbb{N}}\) with radix \typeterminal{SrcRadix} to the \typeterminal{PosInt} representation of radix \typeterminal{DstRadix}"
+\end{enumerate}
+\end{example}
+
+
+\begin{definition}[Substitution in Types]
+Given a type-variable assignment \(\psi_t = \{ \metavariable{\alpha_1} \mapsto \metavariable{\tau_1}, \quad \metavariable{\alpha_2} \mapsto \metavariable{\tau_2}, \quad \dots \}\),
+the thereby induced, lexically scoped substitution \(\overline{\psi_t}\) replaces all \emph{free} occurences of the variables \(\metavariable{\alpha_i}\) in a type-term \(\metavariable{\xi} \in \typenonterm{\{\metavariable{\alpha_1}, \quad \metavariable{\alpha_2}, \quad \dots\}}\) recursively with the type-term given by \(\psi_t(\metavariable{\alpha_i})\).
+Lexical scoping is implemented by simply not substituting any bound occourences of variables \(\metavariable{\alpha_i}\). This allows to skip \(\alpha\)-conversion as done in classical \(\lambda\)-calculus.
+
+\[\overline{\psi_t} \metavariable{\xi} = \begin{cases}
+\metavariable{\xi} \quad \text{if } \metavariable{\xi} \in \typenames\\
+\metavariable{\xi} \quad \text{if }  \metavariable{\xi} \in \{\metavariable{\alpha_1}, \metavariable{\alpha_2}, \dots\} \text{ and } \metavariable{\xi} \notin \text{Dom}(\psi_t)\\
+\metavariable{\tau} \quad \text{if }  \metavariable{\xi} \in \{\metavariable{\alpha_1}, \metavariable{\alpha_2}, \dots\} \text{ and } (\metavariable{\xi} \mapsto \metavariable{\tau}) \in \psi_t\\
+\typeterminal{\forall} \metavariable{\alpha} \typeterminal{.} \overline{\psi_t}\metavariable{\xi'} \quad \text{if } \metavariable{\xi} \text{ is of the form } \typeterminal{\forall}  \metavariable{\alpha} \typeterminal{.} \metavariable{\xi'} \text{ and } \metavariable{\alpha} \notin \text{Dom}(\psi_t)\\
+\typeterminal{\forall} \metavariable{\alpha} \typeterminal{.} \overline{\psi_t \setminus \{\metavariable{\alpha} \mapsto \metavariable{\tau}\}}\metavariable{\xi'} \quad \text{if } \metavariable{\xi} \text{ is of the form } \typeterminal{\forall}  \metavariable{\alpha} \typeterminal{.} \metavariable{\xi'} \text{ and } \{\metavariable{\alpha} \mapsto \metavariable{\tau}\} \in \psi_t\\
+\typeterminal{<} (\overline{\psi_t} \metavariable{\xi_1}) \quad (\overline{\psi_t} \metavariable{\xi_2}) \typeterminal{>} \quad \text{if } \metavariable{\xi} \text{ is of the form } \typeterminal{<} \metavariable{\xi_1} \quad \metavariable{\xi_2} \typeterminal{>}\\
+(\overline{\psi_t} \metavariable{\xi_1}) \typeterminal{\rightarrow} (\overline{\psi_t} \metavariable{\xi_2}) \quad \text{if } \metavariable{\xi} \text{ is of the form } \metavariable{\xi_1} \typeterminal{\rightarrow} \metavariable{\xi_2}\\
+(\overline{\psi_t} \metavariable{\xi_1}) \typeterminal{\rightarrow_{morph}} (\overline{\psi_t} \metavariable{\xi_2}) \quad \text{if } \metavariable{\xi} \text{ is of the form } \metavariable{\xi_1} \typeterminal{\rightarrow_{morph}} \metavariable{\xi_2}\\
+(\overline{\psi_t} \metavariable{\xi_1}) \typeterminal{\sim} (\overline{\psi_t} \metavariable{\xi_2}) \quad \text{if } \metavariable{\xi} \text{ is of the form } \metavariable{\xi_1} \typeterminal{\sim} \metavariable{\xi_2}\\
+\end{cases}\]
+
+\[\overline{\psi_t} \metavariable{e} = \begin{cases}
+\metavariable{e} \quad \text{ if } \metavariable{e} \text{ is a variable}
+\exprterminal{\Lambda \metavariable{\alpha} \mapsto} \overline{\psi_t}\metavariable{e'}  \quad \text{ if \metavariable{e} is of the form } \exprterminal{\Lambda \metavariable{\alpha} \mapsto \metavariable{e'}}\\
+\exprterminal{\lambda \metavariable{x} : }\overline{\psi_t}\metavariable{\tau} \exprterminal{\mapsto} \overline{\psi_t}\metavariable{e'}  \quad \text{ if \metavariable{e} is of the form } \exprterminal{\lambda \metavariable{x} : \metavariable{\tau} \mapsto \metavariable{e'}}\\
+\exprterminal{\lambda \metavariable{x} : }\overline{\psi_t}\metavariable{\tau} \exprterminal{\mapsto_\text{morph}} \overline{\psi_t}\metavariable{e'}  \quad \text{ if \metavariable{e} is of the form } \exprterminal{\lambda \metavariable{x} : \metavariable{\tau} \mapsto_\text{morph} \metavariable{e'}}\\
+\end{cases}\]
+
+
+\end{definition}
+
+
+
+
+
+\begin{definition}[Substitution in Expressions]
+\todo{complete}
+Given an expression-variable assignment \(\psi_e = \{ \metavariable{x_1} \mapsto \metavariable{t_1}, \quad \metavariable{x_2} \mapsto \metavariable{t_2}, \quad \dots \}\),
+the thereby induced, lexically scoped substitution \(\overline{\psi_e}\) replaces all \emph{free} occurences of the expression variables \(\metavariable{x_i}\)
+in an expression \(
+	e \in
+	\exprnonterm
+	{\typevars}
+	{\{\metavariable{x_1}, \quad \metavariable{x_2}, \quad \dots\}}
+\). Lexical scoping is implemented by simply not substituting any bound occourences of variables \(\metavariable{\alpha_i}\). This allows to skip \(\alpha\)-conversion as done in classical \(\lambda\)-calculus.
+
+\[\overline{\psi} \metavariable{e} = \begin{cases}
+\metavariable{e} \quad \text{if } \metavariable{\xi} \in \typenames\\
+\metavariable{\tau} \quad \text{if } (\metavariable{\xi} \mapsto \metavariable{\tau}) \in \psi\\
+\typeterminal{\forall} \metavariable{\alpha} \typeterminal{.} \overline{\psi}\metavariable{\xi'} \quad \text{if } \metavariable{\xi} \text{ is of the form } \typeterminal{\forall}  \metavariable{\alpha} \typeterminal{.} \metavariable{\xi'} \text{ and } \metavariable{\alpha} \notin \text{Dom}(\psi)\\
+\typeterminal{\forall} \metavariable{\alpha} \typeterminal{.} \metavariable{\xi'} \quad \text{if } \metavariable{\xi} \text{ is of the form } \typeterminal{\forall}  \metavariable{\alpha} \typeterminal{.} \metavariable{\xi'} \text{ and } \metavariable{\alpha} \in \text{Dom}(\psi)\\
+\typeterminal{<} (\overline{\psi} \metavariable{\xi_1}) \quad (\overline{\psi} \metavariable{\xi_2}) \typeterminal{>} \quad \text{if } \metavariable{\xi} \text{ is of the form } \typeterminal{<} \metavariable{\xi_1} \quad \metavariable{\xi_2} \typeterminal{>}\\
+(\overline{\psi} \metavariable{\xi_1}) \typeterminal{\rightarrow} (\overline{\psi} \metavariable{\xi_2}) \quad \text{if } \metavariable{\xi} \text{ is of the form } \metavariable{\xi_1} \typeterminal{\rightarrow} \metavariable{\xi_2}\\
+(\overline{\psi} \metavariable{\xi_1}) \typeterminal{\rightarrow_{morph}} (\overline{\psi} \metavariable{\xi_2}) \quad \text{if } \metavariable{\xi} \text{ is of the form } \metavariable{\xi_1} \typeterminal{\rightarrow_{morph}} \metavariable{\xi_2}\\
+(\overline{\psi} \metavariable{\xi_1}) \typeterminal{\sim} (\overline{\psi} \metavariable{\xi_2}) \quad \text{if } \metavariable{\xi} \text{ is of the form } \metavariable{\xi_1} \typeterminal{\sim} \metavariable{\xi_2}\\
+\end{cases}\]
+
+\end{definition}
+
+\subsection{Typing}
+\subsubsection{Equivalence of Type Terms}
+
+\begin{definition}[Distributivity]
+\todo{}
+\end{definition}
+
+\begin{definition}[Equivalence Relation]
+\todo{}
+\end{definition}
+
+\subsubsection{Normal Forms}
+
+\begin{definition}[Ladder Normal Form]
+\todo{}
+\end{definition}
+
+\subsubsection{Subtyping}
+
+\begin{definition}[Syntactic Subtyping]
+\todo{}
+\end{definition}
+
+\begin{definition}[Semantic Subtyping]
+\todo{}
+\end{definition}
+
+\subsubsection{Inference of Expression Types}
+
+The type-context \(\Gamma = \{ \metavariable{x_1} : \metavariable{\tau_1} , \quad \metavariable{x_2} : \metavariable{\tau_2} , \quad \ldots \}\) is a finite mapping from variables \(\metavariable{x_i} \in \exprvars\) to ground types \(\metavariable{\tau_i} \in \typenonterm{\emptyset}\).
+Using the inference rules given in \ref{def:typerules}, further typing-judgements
+of the form
+\begin{itemize}
+\item \(\metavariable{e} : \metavariable{\tau} \quad\) read as "expression \(\metavariable{e}\) is of type \(\metavariable{\tau}\)" and
+\item \(\metavariable{e} :\approx \metavariable{\tau} \quad\) read as "expression \(\metavariable{e}\) is compatible with type \(\metavariable{\tau}\)"
+\end{itemize}
+can be derived from the context \(\Gamma\) where \(\metavariable{e} \in \exprnonterm{\emptyset}{\exprvars}\) and \(\metavariable{\tau} \in \typenonterm{\emptyset}\)
+
+\begin{definition}[Syntactic Well-Typedness]
+An expression \(\metavariable{e} \in \exprnonterm{\emptyset}{\emptyset}\) is \textbf{syntactically well-typed} if there exists a type \(\metavariable{\tau} \in \typenonterm{\emptyset}\),
+such that \( \emptyset \vdash \metavariable{e} : \metavariable{\tau} \) by \ref{def:typerules}.
+\end{definition}
+
+\begin{definition}[Semantic Well-Typedness]
+An expression \(\metavariable{e} \in \exprnonterm{\emptyset}{\emptyset}\) is \textbf{semantically well-typed} if there exists a type \(\metavariable{\tau} \in \typenonterm{\emptyset}\),
+such that \( \emptyset \vdash \metavariable{e} :\approx \metavariable{\tau} \) by \ref{def:typerules}.
+\end{definition}
+
+\begin{definition}[Inference Rules for the Typing Relation.]
+  \label{def:typerules}
+
+As usual, each rule is composed of premises (above the horizontal line) and a conclusion (below the line):
+\begin{mathpar}
+
+	\inferrule[T-Variable]{
+		\metavariable{x} \in \exprvars\\
+		\metavariable{\tau} \in \typenonterm{\emptyset}\\
+		\metavariable{x}:\metavariable{\tau} \in \Gamma\\
+	}{
+		\Gamma \vdash \metavariable{x}:\metavariable{\tau}
+	}\and
+
+
+	\inferrule[T-LetBinding]{
+		\Gamma \vdash \metavariable{e} : \metavariable{\sigma} \\
+		\Gamma , \metavariable{x}:\metavariable{\sigma} \vdash \metavariable{t} : \metavariable{\tau}
+	}{
+		\Gamma \vdash (\exprterminal{\text{let }}\metavariable{x}\exprterminal{\text{ = }}\metavariable{e}\exprterminal{\text{ in }} \metavariable{t}) : \metavariable{\tau}
+	}
+
+
+	\inferrule[T-TypeAbs]{
+		\metavariable{\tau} \in \typenonterm{\typevars \cup \{\metavariable{\alpha}\}} \\
+		\metavariable{e} \in \exprnonterm{\typevars \cup \{ \metavariable{\alpha} \}}{\exprvars} \\
+		\Gamma \vdash \metavariable{e} : \metavariable{\tau} \\
+	}{
+        \Gamma \vdash (\exprterminal{\Lambda} \metavariable{\alpha} \exprterminal{\mapsto} \metavariable{e}) : \typeterminal{\forall}\metavariable{\alpha}\typeterminal{.}\metavariable{\tau}
+	}
+
+	\inferrule[T-TypeApp]{
+		\Gamma \vdash \metavariable{e} : \metavariable{\tau} \\
+		\metavariable{\tau} \in \typenonterm{\typevars \cup \metavariable{\alpha}} \\
+		\metavariable{\sigma} \in \typenonterm{\typevars}
+	}{
+		\Gamma \vdash ( \metavariable{e} \quad \metavariable{\sigma} ) : \{\metavariable{\alpha} \mapsto \metavariable{\sigma}\} \metavariable{\tau}
+	}
+
+
+	\inferrule[T-ValueAbs]{
+		\metavariable{\sigma}, \metavariable{\tau} \in \typenonterm{\typevars} \\
+		\metavariable{e} \in \exprnonterm{\typevars}{\exprvars \cup \{ \metavariable{x} \} } \\
+		\Gamma \vdash \metavariable{e} : \metavariable{\tau} \\
+	}{
+        \Gamma \vdash (\exprterminal{\lambda} \metavariable{x} \exprterminal{:} \metavariable{\sigma} \exprterminal{\mapsto} \metavariable{e}) : \metavariable{\sigma}\typeterminal{\rightarrow}\metavariable{\tau}
+	}
+
+	\inferrule[T-ValueApp]{
+		\Gamma \vdash \metavariable{f} : \metavariable{\sigma} \typeterminal{\rightarrow} \metavariable{\tau} \\
+		\Gamma \vdash \metavariable{a} : \metavariable{\sigma} \\
+	}{
+		\Gamma \vdash (\metavariable{f} \quad \metavariable{a}) : \metavariable{\tau}
+	}\and
+
+
+	\inferrule[T-Compatible]{
+		\Gamma \vdash \metavariable{e} : \metavariable{\tau}
+	}{
+		\Gamma \vdash \metavariable{e} :\approx \metavariable{\tau}
+	}\and
+	
+	\inferrule[T-MorphAbs]{
+		\metavariable{\sigma}, \metavariable{\tau} \in \typenonterm{\typevars} \\
+		\metavariable{e} \in \exprnonterm{\typevars}{\exprvars \cup \{ \metavariable{x} \} } \\
+		\Gamma \vdash \metavariable{e} : \metavariable{\tau} \\
+	}{
+        \Gamma \vdash (\exprterminal{\lambda} \metavariable{x} \exprterminal{:} \metavariable{\tau} \exprterminal{\mapsto_{morph}} \metavariable{e}) : \metavariable{\sigma}\typeterminal{\rightarrow_{morph}}\metavariable{\tau}
+	}\and
+
+	\inferrule[T-MorphApp]{
+		\Gamma \vdash \metavariable{e} : \metavariable{\tau}\\
+		\exists \metavariable{h} . \Gamma \vdash \metavariable{h} : \metavariable{\tau} \typeterminal{\rightarrow_{morph}} \metavariable{\tau'}\\
+		\metavariable{\tau} \precsim \metavariable{\tau'}
+	}{
+		\Gamma \vdash \metavariable{e} :\approx \metavariable{\tau'}
+	}\and
+
+	\inferrule[T-Ascension]{
+		\Gamma \vdash \metavariable{e} : \metavariable{\tau} \\
+		\metavariable{\tau'} \leq \metavariable{\tau}
+	}{
+		\Gamma \vdash (\metavariable{e} \exprterminal{\text{ as }} \metavariable{\tau'}) : \metavariable{\tau'}
+	}\and
+
+	\inferrule[T-Descension]{
+		\Gamma \vdash \metavariable{e} : \metavariable{\tau}\\
+		\metavariable{\tau} \leq \metavariable{\tau'}
+	}{
+		\Gamma \vdash \metavariable{e} : \metavariable{\tau'}
+	}\and
+
+\end{mathpar}
+\end{definition}
+
+
+\subsection{Evaluation Semantics}
+
+Evaluation of an expression \(\metavariable{e} \in \exprnonterm{\emptyset}{\emptyset}\) is defined by exhaustive application of the rewrite rules \(\rightarrow_\beta\) and \(\rightarrow_\delta\),
+which are given in \ref{def:evalrules}.
+
+\begin{definition}[Inference Rules for Evaluation]
+\label{def:evalrules}
+
+\begin{mathpar}
+
+	\inferrule[E-App1]{
+		\metavariable{e_1} \rightarrow_\beta \metavariable{e_1'}
+	}{
+		\metavariable{e_1} \metavariable{e_2}
+		\rightarrow_\beta
+		\metavariable{e_1'} \metavariable{e_2}
+	}\and
+
+	\inferrule[E-App2]{
+		\metavariable{e_2} \rightarrow_\beta \metavariable{e_2'}
+	}{
+		\metavariable{e_1} \metavariable{e_2}
+		\rightarrow_\beta
+		\metavariable{e_1} \metavariable{e_2'}
+	}
+
+	\inferrule[E-TypApp]{
+		\metavariable{\tau} \in \typenonterm{\emptyset}\\
+		\metavariable{e} \rightarrow_\beta \metavariable{e'}
+	}{
+		\metavariable{e}
+		\metavariable{\tau}
+		\rightarrow_\beta
+		\metavariable{e'}
+		\metavariable{\tau}
+	}
+
+	\newline
+
+	\inferrule[E-TypAppLam]{
+	}{
+		\exprterminal{(\Lambda} \metavariable{\alpha}
+		\exprterminal{\mapsto} \metavariable{e}
+		\exprterminal{)}
+		\metavariable{\tau}
+		\rightarrow_\beta
+		\{ \metavariable{\alpha} \mapsto \metavariable{\tau} \} \metavariable{e}
+	}\and
+
+	\inferrule[E-AppLam]{
+	}{
+		\exprterminal{(\lambda} \metavariable{x}
+		\exprterminal{:} \metavariable{\sigma}
+		\exprterminal{\mapsto} \metavariable{e}
+		\exprterminal{)}
+		\metavariable{a}
+		\rightarrow_\beta
+		\{ \metavariable{x} \mapsto \metavariable{a} \} \metavariable{e}
+	}\and
+
+	\inferrule[E-AppLet]{
+	}{
+		\exprterminal{\text{let }}\metavariable{x}
+		\exprterminal{\text{ = }}\metavariable{a}
+		\exprterminal{\text{ in }}\metavariable{e}
+		\rightarrow_\beta
+		\{ \metavariable{x} \mapsto \metavariable{a} \} \metavariable{e}
+	}
+
+
+	\inferrule[E-ImplicitCast]{
+		\Gamma \vdash \metavariable{f} : \metavariable{\sigma} \typeterminal{\rightarrow} \metavariable{\tau} \\
+		\Gamma \vdash \metavariable{h} : \metavariable{\sigma'} \typeterminal{\rightarrow_{morph}} \metavariable{\sigma} \\
+		\Gamma \vdash \metavariable{a} : \metavariable{\sigma'}
+	}{
+		\exprterminal{(} \metavariable{f} \quad \metavariable{a} \exprterminal{)}
+		\rightarrow_\delta
+		\exprterminal{(} \metavariable{f} \quad \exprterminal{(} \metavariable{h} \quad \metavariable{a} \exprterminal{))}
+	}
+
+\end{mathpar}
+\end{definition}
+
+
+\begin{lemma}[\(\beta\)-reduction preserves \(\delta\)-normalform]
+Assume \metavariable{e} is in \(\delta\)-normalform and \(\metavariable{e} \rightarrow \metavariable{e'}\). Then \(\metavariable{e'}\) is in \(\delta\)-normalform as well.
+\begin{proof}
+\todo{}
+\end{proof}
+\end{lemma}
+
+\subsection{Proof of Syntactic Type Soundness}
+
+\begin{lemma}[Progress]
+\label{lemma:progress}
+
+If \(\emptyset \vdash \metavariable{e} : \metavariable{\tau}\), then either \(\metavariable{e}\) is a value or there exists some \(\metavariable{e'}\) such that \(\metavariable{e} \rightarrow_{eval} \metavariable{e'}\)
+
+\begin{proof}
+\todo{}
+\end{proof}
+
+\end{lemma}
+
+
+\begin{lemma}[Preservation]
+\label{lemma:preservation}
+
+\begin{proof}
+\todo{}
+\end{proof}
+
+\end{lemma}
+
+
+
+
+\begin{theorem}[Type Soundness]
+If \(\emptyset \vdash \metavariable{e}:\metavariable{\tau}\), then it never occurs that \(\metavariable{e} \rightarrow_{eval}^{*} \metavariable{e'}\) where \metavariable{e'} is in normal form but not a value.
+
+\begin{proof}
+Follows from \ref{lemma:progress} and \ref{lemma:preservation}.
+\end{proof}
+\end{theorem}
+
+
+\section{Boehm-Berarducci Encoding}
+
+
+\newcommand{\typvar}[1]{\textcolor{Emerald}{#1}}
+\newcommand{\expvar}[1]{\textcolor{MidnightBlue}{#1}}
+
+
+\subsection{Booleans}
+
+\begin{definition}
+Let \(\Sigma = \{ \text{Bool}, \text{BB-Bool} \}\).
+
+\begin{itemize}
+\item let {\textcolor{magenta}{bb-true}} = \exprterminal{\((\Lambda\typvar{\alpha}\mapsto\lambda\expvar{t}:\typvar{\alpha}\mapsto\lambda\expvar{f}:\typvar{\alpha}\mapsto\expvar{t})\) as} \typeterminal{Bool \(\sim\) BB-Bool}
+\item let {\textcolor{magenta}{bb-false}} = \exprterminal{\((\Lambda\typvar{\alpha}\mapsto\lambda\expvar{t}:\typvar{\alpha}\mapsto\lambda\expvar{f}:\typvar{\alpha}\mapsto\expvar{f})\) as} \typeterminal{Bool \(\sim\) BB-Bool}
+\end{itemize}
+
+\end{definition}
+
+\begin{lemma}
+{\textcolor{magenta}{bb-true}} and {\textcolor{magenta}{bb-false}} are \emph{values}.
+
+\begin{proof}
+\todo{}
+\end{proof}
+\end{lemma}
+
+\subsection{Conditionals}
+
+\begin{itemize}
+\item let {\textcolor{magenta}{bb-if}} = \exprterminal{
+	\(\Lambda\typvar{\alpha}\)\\
+	\(\mapsto\lambda\) \expvar{cond} : \typeterminal{ Bool \(\sim\) BB-Bool \(\sim \forall\typvar{\beta}.(\typvar{\beta}\rightarrow\typvar{\beta}\rightarrow\typvar{\beta})\)}\\
+	\(\mapsto\lambda\) \expvar{then} : \(\typvar{\alpha}\)\\
+	\(\mapsto\lambda\) \expvar{else} : \(\typvar{\alpha}\)\\
+	\(\mapsto\) \expvar{cond} \typvar{\(\alpha\)} \expvar{then} \expvar{else}
+}
+\end{itemize}
+
+\subsection{Natural Numbers}
+\begin{definition}
+
+Let \(\Sigma = \{ \mathbb{N}, \text{BB-Nat}\}\).
+
+\begin{itemize}
+\item let {\textcolor{magenta}{bb-zero}} = \(\exprterminal{( \Lambda \typvar{\alpha} \mapsto \lambda \expvar{s} : \typeterminal{\typvar{\alpha} \rightarrow \typvar{\alpha}} \mapsto \lambda \expvar{z} : \typvar{\alpha} \mapsto \expvar{z} ) \text{ as } }\)
+\typeterminal{\(\mathbb{N} \sim \text{BB-Nat} \sim \forall \typvar{\alpha} . (\typvar{\alpha} \rightarrow \typvar{\alpha}) \rightarrow \typvar{\alpha} \rightarrow \typvar{\alpha} \)}
+
+
+\item let {\textcolor{magenta}{bb-one}} = \(\exprterminal{(\Lambda \typvar{\alpha} \mapsto \lambda \expvar{s} : \typeterminal{\typvar{\alpha} \rightarrow \typvar{\alpha}} \mapsto \lambda \expvar{z} : \typvar{\alpha} \mapsto \expvar{s} \expvar{z} ) \text{ as }}\)
+\typeterminal{\(\mathbb{N} \sim \text{BB-Nat} \sim \forall \typvar{\alpha} . (\typvar{\alpha} \rightarrow \typvar{\alpha}) \rightarrow \typvar{\alpha} \rightarrow \typvar{\alpha} \)}
+
+
+\item let {\textcolor{magenta}{bb-two}} = \(\exprterminal{(\Lambda \typvar{\alpha} \mapsto \lambda \expvar{s} : \typeterminal{\typvar{\alpha} \rightarrow \typvar{\alpha}} \mapsto \lambda \expvar{z} : \typvar{\alpha} \mapsto \expvar{s} (\expvar{s} \expvar{z}) ) \text{ as }}\)
+\typeterminal{\(\mathbb{N} \sim \text{BB-Nat} \sim \forall \typvar{\alpha} . (\typvar{\alpha} \rightarrow \typvar{\alpha}) \rightarrow \typvar{\alpha} \rightarrow \typvar{\alpha} \)}
+
+\end{itemize}
+
+\end{definition}
+
+
+\begin{definition}
+The successor function is given by:
+
+let {\textcolor{magenta}{bb-succ}} =
+\newline\(\exprterminal{\quad \lambda \expvar{n} :
+\typeterminal{ \mathbb{N}
+\sim \text{BB-Nat}
+\sim \forall \typvar{\alpha} . ((\typvar{\alpha} \rightarrow \typvar{\alpha}) \rightarrow \typvar{\alpha} \rightarrow \typvar{\alpha})}\\
+}\)
+\newline
+\( \exprterminal{\quad \quad \mapsto ( \Lambda \typvar{\alpha} \mapsto \lambda \expvar{s} : \typeterminal{(\typvar{\alpha} \rightarrow \typvar{\alpha})} \mapsto \lambda \expvar{z} : \typvar{\alpha} }\)
+\( \exprterminal{\mapsto \expvar{s} ( \expvar{n} \typvar{\alpha} \expvar{s} \expvar{z} )) \text{ as } }\)
+\typeterminal{
+\(\mathbb{N} \sim \text{BB-Nat} \sim \forall \typvar{\alpha} . (\typvar{\alpha} \rightarrow \typvar{\alpha}) \rightarrow \typvar{\alpha} \rightarrow \typvar{\alpha}\)
+}
+\end{definition}
+
+\begin{example}
+\(\emptyset \vdash ( \textcolor{magenta}{\text{bb-succ} \quad \text{bb-one}} ) : \typeterminal{ \mathbb{N} \sim \text{BB-Nat} \sim \forall \typvar{\alpha} . (\typvar{\alpha} \rightarrow \typvar{\alpha}) \rightarrow \typvar{\alpha} \rightarrow \typvar{\alpha}) } \)
+\end{example}
+
+\begin{example}
+\textcolor{magenta}{bb-succ bb-one} \(\rightarrow_\beta^{*}\) \textcolor{magenta}{bb-two}.
+\end{example}
+
+\begin{example}
+\exprterminal{(}\textcolor{magenta}{bb-succ bb-false}\exprterminal{)} is stuck. \(\nexists\metavariable{v} . \) \exprterminal{(}\textcolor{magenta}{bb-succ bb-false}\exprterminal{)} \( \rightarrow_\text{eval} \metavariable{v}\) where \(\metavariable{v}\) is a \emph{value}.
+\end{example}
+
+\begin{example}
+\exprterminal{(}\textcolor{magenta}{bb-succ bb-false}\exprterminal{)} is \emph{not} well-typed. \(\nexists\metavariable{\tau} . \emptyset \vdash \) \textcolor{magenta}{bb-succ bb-false} : \(\metavariable{\tau}\).
+\end{example}
+
+\subsection{Pairs}
+
+\begin{definition}
+pairs
+
+\begin{itemize}
+\item let {\textcolor{magenta}{bb-pair}} = \(\exprterminal{\Lambda \typvar{\alpha} \mapsto \Lambda \typvar{\beta} \mapsto \lambda \expvar{a}:\typvar{\alpha} \mapsto \lambda \expvar{b} : \typvar{\beta}}\)\\
+\(\exprterminal{
+	\mapsto (\Lambda\typvar{\gamma} \mapsto \lambda \expvar{s} : \typeterminal{\typvar{\alpha} \rightarrow \typvar{\beta} \rightarrow \typvar{\gamma}} \mapsto \expvar{s} \expvar{a} \expvar{b})}\)
+	\exprterminal{ as } \typeterminal{\((\typvar{\alpha}\times\typvar{\beta})\) \(\sim\) <BB-Pair \(\typvar{\alpha}\text{ }\typvar{\beta}\)> \(\sim\) \(\forall \typvar{\gamma} . ((\typvar{\alpha} \rightarrow \typvar{\beta} \rightarrow \typvar{\gamma}) \rightarrow \typvar{\gamma})\) }\\
+
+\item let {\textcolor{magenta}{bb-pair-first}} = \(\exprterminal{
+	\Lambda \typvar{\alpha} \mapsto \Lambda \typvar{\beta}\\
+	\mapsto \lambda \expvar{p} : \typeterminal{
+		(\typvar{\alpha}\times\typvar{\beta}) \sim\text{ <BB-Pair \(\typvar{\alpha}\text{ }\typvar{\beta}\)> }\sim \forall \typvar{\gamma} . ((\typvar{\alpha} \rightarrow \typvar{\beta} \rightarrow \typvar{\gamma}) \rightarrow \typvar{\gamma} )
+	}}\)\\
+	\(\exprterminal{
+	\mapsto \expvar{p} \typvar{\alpha} (\lambda \expvar{a}:\typvar{\alpha} \mapsto \lambda \expvar{b}:\typvar{\beta} \mapsto \expvar{a})
+}\)\\
+
+\item let {\textcolor{magenta}{bb-pair-second}} = \(\exprterminal{
+	\Lambda \typvar{\alpha} \mapsto \Lambda \typvar{\beta}
+	\mapsto \lambda \expvar{p} : \typeterminal{
+		(\typvar{\alpha}\times\typvar{\beta}) \sim\text{<BB-Pair \(\typvar{\alpha}\text{ }\typvar{\beta}\)> }\sim \forall \typvar{\gamma} . ((\typvar{\alpha} \rightarrow \typvar{\beta} \rightarrow \typvar{\gamma}) \rightarrow \typvar{\gamma} )
+	}}\)\\
+	\(\exprterminal{
+	\mapsto \expvar{p} \typvar{\beta} (\lambda \expvar{a}:\typvar{\alpha} \mapsto \lambda \expvar{b}:\typvar{\beta} \mapsto \expvar{b})
+}\)\\
+
+\end{itemize}
+\end{definition}
+
+\subsection{Lists}
+
+
+\subsection{Algebraic Datatypes}
+\todo{}
+
+\end{document}
+