coq/context.v

@@ -1,5 +1,8 @@
 From Coq Require Import Strings.String.
 Require Import terms.
+Include Terms.
+
+Module Context.
 
 
 Inductive context : Type :=
@@ -13,3 +16,6 @@ Inductive context_contains : context -> string -> type_term -> Prop :=
   | C_shuffle : forall x X y Y Γ,
     (context_contains Γ x X) ->
     (context_contains (ctx_assign y Y Γ) x X).
+
+
+End Context.

coq/equiv.v

@@ -34,6 +34,12 @@ Require Import terms.
 Require Import subst.
 From Coq Require Import Strings.String.
 
+Include Terms.
+Include Subst.
+
+Module Equiv.
+
+
 (** Alpha conversion in types *)
 
 Reserved Notation "S '--->α' T" (at level 40).
@@ -401,3 +407,6 @@ Proof.
   apply TEq_Distribute.
   apply L_DistributeOverSpec2.
 Qed.
+
+
+End Equiv.

coq/morph.v

@@ -5,6 +5,14 @@ Require Import equiv.
 Require Import subtype.
 Require Import context.
 
+Include Terms.
+Include Subst.
+Include Equiv.
+Include Subtype.
+Include Context.
+
+Module Morph.
+
 (* Given a context, there is a morphism path from τ to τ' *)
 Reserved Notation "Γ '|-' σ '~>' τ" (at level 101, σ at next level, τ at next level).
 
@@ -89,3 +97,6 @@ Proof.
   apply C_shuffle.
   apply C_take.
 Qed.
+
+
+End Morph.

coq/smallstep.v

@@ -1,9 +1,14 @@
 From Coq Require Import Strings.String.
 Require Import terms.
 Require Import subst.
-Require Import subtype.
 Require Import typing.
 
+Include Terms.
+Include Subst.
+Include Typing.
+
+Module Smallstep.
+
 Reserved Notation " s '-->α' t " (at level 40).
 Reserved Notation " s '-->β' t " (at level 40).
 
@@ -135,3 +140,5 @@ Proof.
 
   apply Multi_Refl.
 Qed.
+
+End Smallstep.

coq/soundness.v

@@ -3,11 +3,19 @@ Require Import terms.
 Require Import subst.
 Require Import equiv.
 Require Import subtype.
-Require Import context.
-Require Import morph.
 Require Import smallstep.
 Require Import typing.
 
+Include Terms.
+Include Subst.
+Include Equiv.
+Include Subtype.
+Include Smallstep.
+Include Typing.
+
+
+Module Soundness.
+
 
 Lemma typing_weakening : forall Γ e τ x σ,
   (Γ |- e \is τ) ->
@@ -406,3 +414,5 @@ Proof.
   admit.
 Admitted.
 
+End Soundness.
+

coq/subst.v

@@ -1,6 +1,10 @@
  From Coq Require Import Strings.String.
 Require Import terms.
 
+Include Terms.
+
+Module Subst.
+
 (* Type Variable "x" is a free variable in type *)
 Inductive type_var_free (x:string) : type_term -> Prop :=
   | TFree_Var :
@@ -124,3 +128,5 @@ Fixpoint expr_specialize (v:string) (n:type_term) (e0:expr_term) :=
   | expr_descend t e => expr_descend (type_subst v n t) (expr_specialize v n e)
   | e => e
   end.
+
+End Subst.

coq/subtype.v

@@ -11,6 +11,10 @@
 From Coq Require Import Strings.String.
 Require Import terms.
 Require Import equiv.
+Include Terms.
+Include Equiv.
+
+Module Subtype.
 
 (** Subtyping *)
 
@@ -92,3 +96,5 @@ Proof.
 	apply TSubRepr_Refl.
 	apply TEq_Refl.
 Qed.
+
+End Subtype.

coq/terms.v

@@ -4,6 +4,7 @@
  *)
 
 From Coq Require Import Strings.String.
+Module Terms.
 
 (* types *)
 Inductive type_term : Type :=
@@ -65,8 +66,6 @@ Declare Custom Entry ladder_expr.
 
 Notation "[< t >]" := t
   (t custom ladder_type at level 80) : ladder_type_scope.
-Notation "t" := t
-  (in custom ladder_type at level 0, t ident) : ladder_type_scope.
 Notation "'∀' x ',' t" := (type_univ x t)
   (t custom ladder_type at level 80, in custom ladder_type at level 80, x constr).
 Notation "'<' σ τ '>'" := (type_spec σ τ)
@@ -86,8 +85,6 @@ Notation "'%' x '%'" := (type_var x%string)
 
 Notation "[{ e }]" := e
   (e custom ladder_expr at level 80) : ladder_expr_scope.
-Notation "e" := e
-  (in custom ladder_expr at level 0, e ident) : ladder_expr_scope.
 Notation "'%' x '%'" := (expr_var x%string)
   (in custom ladder_expr at level 0, x constr) : ladder_expr_scope.
 Notation "'Λ' t '↦' e" := (expr_ty_abs t e)
@@ -121,3 +118,5 @@ Compute polymorphic_identity1.
 
 Close Scope ladder_type_scope.
 Close Scope ladder_expr_scope.
+
+End Terms.

coq/typing.v

@@ -9,6 +9,15 @@ Require Import subtype.
 Require Import context.
 Require Import morph.
 
+Include Terms.
+Include Subst.
+Include Equiv.
+Include Subtype.
+Include Context.
+Include Morph.
+
+Module Typing.
+
 (** Typing Derivation *)
 
 Reserved Notation "Gamma '|-' x '\is' X"  (at level 101, x at next level, X at level 0).

paper/main.tex

@@ -53,35 +53,11 @@
 
 
 \begin{abstract}
- This work introduces \emph{representational polymorphism} as a form of
+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}.
- coercive subtyping, which differentiates between various concrete
+Using ladder-types, multi-layered embeddings of higher-level data-types into lower-level data-types can be described by a type-level structure.
- representations w.r.t. an abstract concept using an explicit type
+By facilitating automatic transformations between semantically compatible datatypes, ladder-typing opens up a new paradigm of abstraction.
- structure. This structure captures the 'represented-as' relation of
+We formally define the syntax \& semantics of this calculus and prove its \emph{type soundness}.
- multi-level data embeddings.  Motivated by the need to manage data
+Further we show how the Boehm-Berarducci encoding can be used to implement algebraic datatypes on the basis of the introduced core calculus.
- transformations —whether for hardware interfacing, IPC/RPC
- communication, or performance optimizations— our type system aims to
- reduce bugs and enhance code clarity by enabling implicit coercions
- between semantically equivalent representations, while retaining
- coherence and soundness.
-
- We extend the polymorphic λ-calculus (System F) with a new type
- constructor, termed \emph{ladder-type} to encode a subtype relation based on
- syntactical embedding, which inversely also helps to disambiguate
- multiple interpretations of the same presentation type. To facilitate
- implicit coercions between semantically equivalent yet presentationally
- different types, we introduce morphisms —functions that transform one
- representation to another of the same abstract type. Morphisms can be
- inductively combined to form complex morphism-paths allowing
- transitivity, list-mappings and lifting of presentation subtypes
- without loss of coherence.  This enables programmers to treat various
- representational forms interchangeably as abstract objects, with
- required transformations managed by the compiler during a separate
- translation step based on expression typing, while still being able to
- locally control specific representations.
-
- We formalize our extended calculus in Coq and demonstrate that our
- translation function preserves typing, with progress and preservation
- theorems remaining valid.
 \end{abstract}
 
 \maketitle
@@ -89,62 +65,6 @@
 
 
 %\newpage
-\section{Introduction}
-The issue of transformation between varying data encodings is all-pervasive in software development.
-Altough programming languages in principle try provide a 'realm of consistent abstraction',
-many parts of the code that interface with the outside world are still riddled with data transformation routines.
-
-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, efficiency or
-for the sake of interfacing with hardware, other libraries / processes, the user.
-Further, differing complexity-profiles of certain representations might even have the potential to complement
-each other and coexist in a single application.
-Often however, such specialized 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.
-
-\paragraph{Interfacing}
-\todo{serilization / marshalling}
-
-\paragraph{How to get fast code ?}
- -> algorithmic optimization
-   -> see which methods are used most frequently
-   -> switch structures to reduce complexity there
-   -> identify special cases
-   -> remove indirection
-
- -> optimize implementation detail:
- -- bottleneck? memory!
- ---- plenty of Main memory,
-	  but FAST memory is scarce
-	--> improve cache efficiency: make compact representations
-	   * Balance De-/Encode Overhead
-	         vs. Load-Overhead
-
-       * Synchronize locality in access order and memory layout.
-       -> elements accessed in succession shall be close in memory.
-	        (e.g. AoS vs SoA)
-
-     ..while..
-     - accounting for machine specific cache-sizes
-     - accounting for SIMD instructions
-     - interfacing with kernels running on accelerator devices
-
-\paragraph{Elegant Abstractions}
-\todo{difference to traditional coercions (static cast)}
-\todo{relation with inheritance based subtyping:  bottom-up vs top-down inheritance vs ladder-types}
-\todo{relation to traits/type-classes}
-\todo{relation to coercive subtyping}
-
-\paragraph{Related Work}
-\todo{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}