Compare commits

..

3 commits

10 changed files with 92 additions and 75 deletions

View file

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

View file

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

View file

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

View file

@ -1,14 +1,9 @@
From Coq Require Import Strings.String. From Coq Require Import Strings.String.
Require Import terms. Require Import terms.
Require Import subst. Require Import subst.
Require Import subtype.
Require Import typing. 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).
Reserved Notation " s '-->β' t " (at level 40). Reserved Notation " s '-->β' t " (at level 40).
@ -140,5 +135,3 @@ Proof.
apply Multi_Refl. apply Multi_Refl.
Qed. Qed.
End Smallstep.

View file

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

View file

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

View file

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

View file

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

View file

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

View file

@ -53,11 +53,35 @@
\begin{abstract} \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} \end{abstract}
\maketitle \maketitle
@ -65,6 +89,62 @@ Further we show how the Boehm-Berarducci encoding can be used to implement algeb
%\newpage %\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} \section{Core Calculus}
\subsection{Syntax} \subsection{Syntax}