|
|
|
@ -6,7 +6,7 @@
|
|
|
|
|
\usepackage{mathpartir}
|
|
|
|
|
\usepackage{hyperref}
|
|
|
|
|
\usepackage{url}
|
|
|
|
|
|
|
|
|
|
\usepackage{stmaryrd}
|
|
|
|
|
\usepackage{minted}
|
|
|
|
|
\usemintedstyle{tango}
|
|
|
|
|
|
|
|
|
@ -52,11 +52,25 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
\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.
|
|
|
|
|
This work explores the idea of \emph{representational polymorphism}
|
|
|
|
|
to treat the coexistence of multiple equivalent representational forms for a single abstract concept.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
interchangeability
|
|
|
|
|
%Our goal is a type system to support the seamless integration of
|
|
|
|
|
%which may arise by consequence of external interfaces or internal optimization.
|
|
|
|
|
|
|
|
|
|
For the study of its formalism, we extend the \emph{polymorphic lambda-calculus} by a new type-constructor,
|
|
|
|
|
called the \emph{ladder-type} in order to encode a \emph{represented-as} relationship into our type-terms.
|
|
|
|
|
Based on this extended type-structure, we first define a subtyping relation to capture
|
|
|
|
|
a notion of structural embedding of higher-level types into lower-level types
|
|
|
|
|
which is then relaxed into \emph{semantic subtyping},
|
|
|
|
|
where for a certain expected type, an equivalent representation implementing the same abstract type
|
|
|
|
|
is accepted as well. In that case, a coercion is inserted implicitly to transform the underlying datastructure
|
|
|
|
|
while keeping all semantical properties of the type intact.
|
|
|
|
|
We specify our typing-rules accordingly, give an algorithm that manifests all implicit coercions in a program
|
|
|
|
|
and prove its \emph{soundness}.
|
|
|
|
|
|
|
|
|
|
\end{abstract}
|
|
|
|
|
|
|
|
|
|
\maketitle
|
|
|
|
@ -64,6 +78,29 @@ Further we show how the Boehm-Berarducci encoding can be used to implement algeb
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
%\newpage
|
|
|
|
|
\section{Introduction}
|
|
|
|
|
While certain representational forms might be fixed already at the boundaries of an application,
|
|
|
|
|
internally, some other representations might be desired for reasons of simplicity and efficiency.
|
|
|
|
|
Further, differing complexity-profiles of certain representations might even have the potential to complement
|
|
|
|
|
each other and coexist in a single application.
|
|
|
|
|
Often however, implementations become heavily dependent on concrete data formats
|
|
|
|
|
and require technical knowledge of the low-level data structures.
|
|
|
|
|
Making use of multiple such representations additionally requires careful transformation of data.
|
|
|
|
|
|
|
|
|
|
\todo{serialization}
|
|
|
|
|
\todo{memory layout optimizations}
|
|
|
|
|
\todo{difference to traditional coercions (static cast)}
|
|
|
|
|
\todo{relation with inheritance based subtyping: bottom-up vs top-down inheritance vs ladder-types}
|
|
|
|
|
|
|
|
|
|
\todo{related work: type specific languages}
|
|
|
|
|
|
|
|
|
|
In order to facilitate programming at "high-level", we introduce a type-system that is able to disambiguate
|
|
|
|
|
this multiplicity of representations and facilitate implicit coercions between them.
|
|
|
|
|
We claim this to aid in (1) forgetting details about representational details during program composition
|
|
|
|
|
and (2) keeping the system flexible enough to introduce representational optimizations at a later stage without
|
|
|
|
|
compromising semantic correctness.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
\section{Core Calculus}
|
|
|
|
|
\subsection{Syntax}
|
|
|
|
|
|
|
|
|
@ -301,7 +338,6 @@ Coq definition is at \hyperref[coq:subst-type]{subst.v:\ref{coq:subst-type}}.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
\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 substitution \(\overline{\psi_e}\) replaces all \emph{free} occurences of the expression variables \(\metavariable{x_i}\)
|
|
|
|
|
in an expression \(e \in \nonterm{E} \) with the \(\psi_e(\metavariable{x_i})\)
|
|
|
|
|