\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{}
\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\)).
"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.
\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}\)
\). 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.
\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):
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]
Assume \metavariable{e} is in \(\delta\)-normalform and \(\metavariable{e}\rightarrow_\beta\metavariable{e'}\). Then \(\metavariable{e'}\) is in \(\delta\)-normalform as well.
Assume \(\emptyset\vdash\metavariable{e} :\approx\metavariable{\tau}\) and \(\metavariable{e}\rightarrow_{\delta}^*\metavariable{e'}\) such that \(\metavariable{e'}\) is in \(\delta\)-normalform.
Then \(\emptyset\vdash\metavariable{e'} : \metavariable{\tau}\)
Assume the expression \(\metavariable{e}\) is \textbf{syntactically well-typed}, i.e. \(\emptyset\vdash\metavariable{e} : \metavariable{\tau}\) for some type \(\metavariable{\tau}\). Then forall \(\metavariable{e'}\) with \(\metavariable{e}\rightarrow_{\beta}\metavariable{e'}\) it holds that \(\emptyset\vdash\metavariable{e'} : \metavariable{\tau}\) as well.
Assume the expression \(\metavariable{e}\) is well typed, i.e. \(\emptyset\vdash\metavariable{e} : \metavariable{\tau}\) for some type \(\metavariable{\tau}\). Then forall \(\metavariable{e'}\) with \(\metavariable{e}\rightarrow_{eval}\metavariable{e'}\) it holds that \(\emptyset\vdash\metavariable{e'} : \metavariable{\tau}\) as well.
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'}\)
If \(\emptyset\vdash\metavariable{e}:\approx\metavariable{\tau}\), then it never occurs that \(\metavariable{e}\rightarrow_{eval}^{*}\metavariable{e'}\) where \metavariable{e'} is in normal form but not a value.
\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}.