wip
This commit is contained in:
parent
61f1234fcc
commit
b0035e711a
4 changed files with 57 additions and 8 deletions
|
@ -5,5 +5,5 @@ subst.v
|
|||
subtype.v
|
||||
typing.v
|
||||
smallstep.v
|
||||
soundness.v
|
||||
bbencode.v
|
||||
|
||||
|
|
|
@ -9,10 +9,22 @@ Include Typing.
|
|||
|
||||
Module Smallstep.
|
||||
|
||||
Reserved Notation " s '-->α' t " (at level 40).
|
||||
Reserved Notation " s '-->β' t " (at level 40).
|
||||
Reserved Notation " s '-->δ' t " (at level 40).
|
||||
Reserved Notation " s '-->eval' t " (at level 40).
|
||||
|
||||
Inductive alpha_step : expr_term -> expr_term -> Prop :=
|
||||
| E_Rename : forall x x' e,
|
||||
(expr_tm_abs x e) -->α (expr_tm_abs x' (expr_subst x (type_var x')))
|
||||
where "s '-->α' t" := (alpha_step s t).
|
||||
|
||||
|
||||
Example a1 : polymorphic_identity1 -->α polymorphic_identity2.
|
||||
Proof.
|
||||
Qed.
|
||||
|
||||
|
||||
Inductive beta_step : expr_term -> expr_term -> Prop :=
|
||||
| E_App1 : forall e1 e1' e2,
|
||||
e1 -->β e1' ->
|
||||
|
|
1
coq/soundness.v
Normal file
1
coq/soundness.v
Normal file
|
@ -0,0 +1 @@
|
|||
|
|
@ -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})\)
|
||||
|
|
Loading…
Reference in a new issue