work on abstract & intro

coq/context.v

@@ -1,8 +1,5 @@
 From Coq Require Import Strings.String.
 Require Import terms.
-Include Terms.
-
-Module Context.
 
 
 Inductive context : Type :=
@@ -16,6 +13,3 @@ 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,12 +34,6 @@ 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).
@@ -407,6 +401,3 @@ Proof.
   apply TEq_Distribute.
   apply L_DistributeOverSpec2.
 Qed.
-
-
-End Equiv.

coq/morph.v

@@ -5,14 +5,6 @@ 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).
 
@@ -97,6 +89,3 @@ Proof.
   apply C_shuffle.
   apply C_take.
 Qed.
-
-
-End Morph.

coq/smallstep.v

@@ -1,14 +1,9 @@
 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).
 
@@ -140,5 +135,3 @@ Proof.
 
   apply Multi_Refl.
 Qed.
-
-End Smallstep.

coq/soundness.v

@@ -3,19 +3,11 @@ 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 τ) ->
@@ -414,5 +406,3 @@ Proof.
   admit.
 Admitted.
 
-End Soundness.
-

coq/subst.v

@@ -1,10 +1,6 @@
  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 :
@@ -128,5 +124,3 @@ 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,10 +11,6 @@
 From Coq Require Import Strings.String.
 Require Import terms.
 Require Import equiv.
-Include Terms.
-Include Equiv.
-
-Module Subtype.
 
 (** Subtyping *)
 
@@ -96,5 +92,3 @@ Proof.
 	apply TSubRepr_Refl.
 	apply TEq_Refl.
 Qed.
-
-End Subtype.

coq/terms.v

@@ -4,7 +4,6 @@
  *)
 
 From Coq Require Import Strings.String.
-Module Terms.
 
 (* types *)
 Inductive type_term : Type :=
@@ -66,6 +65,8 @@ 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 σ τ)
@@ -85,6 +86,8 @@ 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)
@@ -118,5 +121,3 @@ Compute polymorphic_identity1.
 
 Close Scope ladder_type_scope.
 Close Scope ladder_expr_scope.
-
-End Terms.

coq/typing.v

@@ -9,15 +9,6 @@ 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,11 +53,35 @@
 
 
 \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}.
+ This work introduces \emph{representational polymorphism} as a form of
-Using ladder-types, multi-layered embeddings of higher-level data-types into lower-level data-types can be described by a type-level structure.
+ coercive subtyping, which differentiates between various concrete
-By facilitating automatic transformations between semantically compatible datatypes, ladder-typing opens up a new paradigm of abstraction.
+ representations w.r.t. an abstract concept using an explicit type
-We formally define the syntax \& semantics of this calculus and prove its \emph{type soundness}.
+ structure. This structure captures the 'represented-as' relation of
-Further we show how the Boehm-Berarducci encoding can be used to implement algebraic datatypes on the basis of the introduced core calculus.
+ multi-level data embeddings.  Motivated by the need to manage data
+ 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
@@ -65,6 +89,62 @@ Further we show how the Boehm-Berarducci encoding can be used to implement algeb
 
 
 %\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}