From ec1a2ab4a49a1d68593dce1d764885b292de84fd Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Wed, 24 Jul 2024 11:23:51 +0200 Subject: [PATCH] add initial main.tex --- paper/main.tex | 697 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 697 insertions(+) create mode 100644 paper/main.tex diff --git a/paper/main.tex b/paper/main.tex new file mode 100644 index 0000000..8362e44 --- /dev/null +++ b/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{} \( \in \typenonterm{\emptyset}\)\\ +"sequence of characters" +\item \typeterminal{ \(\sim\) Char>} \( \in \typenonterm{\emptyset}\)\\ +"sequence of decimal digits, where each digit is represented as character" +\item \typeterminal{ \(\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{ \(\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 . \(\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\) \(\sim\) \(\sim\) Char>\\ + \(\rightarrow_{morph}\)\\ + \(\mathbb{N} \sim\) \(\sim\) \(\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\) \(\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{ }\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{ }\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} +