wip

coq/_CoqProject

@@ -2,7 +2,6 @@
 terms.v
 equiv.v
 subst.v
-subtype.v
 typing.v
 smallstep.v
 bbencode.v

coq/equiv.v

@@ -30,43 +30,18 @@
  * satisfies all properties required of an equivalence relation.
  *)
 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).
-Inductive type_conv_alpha : type_term -> type_term -> Prop :=
-  | TEq_Alpha : forall x y t,
-  (type_univ x t) -->α (type_univ y (type_subst x (type_var y) t))
-where "S '-->α' T" := (type_conv_alpha S T).
-
-(** Alpha conversion is symmetric *)
-
-Lemma type_alpha_symm :
-  forall σ τ,
-  (σ -->α τ) -> (τ -->α σ).
-Proof.
- (* TODO *)
-Admitted.
-
-
 (** Define all rewrite steps $\label{coq:type-dist}$ *)
 
 Reserved Notation "S '-->distribute-ladder' T" (at level 40).
 Inductive type_distribute_ladder : type_term -> type_term -> Prop :=
-  | L_DistributeOverSpec1 : forall x x' y,
+  | L_DistributeOverApp : forall x y y',
-    (type_spec (type_ladder x x') y)
-    -->distribute-ladder
-    (type_ladder (type_spec x y) (type_spec x' y))
-
-  | L_DistributeOverSpec2 : forall x y y',
     (type_spec x (type_ladder y y'))
     -->distribute-ladder
     (type_ladder (type_spec x y) (type_spec x y'))
@@ -81,28 +56,13 @@ Inductive type_distribute_ladder : type_term -> type_term -> Prop :=
     -->distribute-ladder
     (type_ladder (type_fun x y) (type_fun x y'))
 
-  | L_DistributeOverMorph1 : forall x x' y,
-    (type_morph (type_ladder x x') y)
-    -->distribute-ladder
-    (type_ladder (type_morph x y) (type_morph x' y))
-
-  | L_DistributeOverMorph2 : forall x y y',
-    (type_morph x (type_ladder y y'))
-    -->distribute-ladder
-    (type_ladder (type_morph x y) (type_morph x y'))
-
 where "S '-->distribute-ladder' T" := (type_distribute_ladder S T).
 
 
 
 Reserved Notation "S '-->condense-ladder' T" (at level 40).
 Inductive type_condense_ladder : type_term -> type_term -> Prop :=
-  | L_CondenseOverSpec1 : forall x x' y,
+  | L_CondenseOverApp : forall x y y',
-    (type_ladder (type_spec x y) (type_spec x' y))
-    -->condense-ladder
-    (type_spec (type_ladder x x') y)
-
-  | L_CondenseOverSpec2 : forall x y y',
     (type_ladder (type_spec x y) (type_spec x y'))
     -->condense-ladder
     (type_spec x (type_ladder y y'))
@@ -117,16 +77,6 @@ Inductive type_condense_ladder : type_term -> type_term -> Prop :=
     -->condense-ladder
     (type_fun x (type_ladder y y'))
 
-  | L_CondenseOverMorph1 : forall x x' y,
-    (type_ladder (type_morph x y) (type_morph x' y))
-    -->condense-ladder
-    (type_morph (type_ladder x x') y)
-
-  | L_CondenseOverMorph2 : forall x y y',
-    (type_ladder (type_morph x y) (type_morph x y'))
-    -->condense-ladder
-    (type_morph x (type_ladder y y'))
-
 where "S '-->condense-ladder' T" := (type_condense_ladder S T).
 
 
@@ -140,12 +90,9 @@ Lemma distribute_inverse :
 Proof.
   intros.
   destruct H.
-  apply L_CondenseOverSpec1.
+  apply L_CondenseOverApp.
-  apply L_CondenseOverSpec2.
   apply L_CondenseOverFun1.
   apply L_CondenseOverFun2.
-  apply L_CondenseOverMorph1.
-  apply L_CondenseOverMorph2.
 Qed.
 
 (** Inversion Lemma:
@@ -158,12 +105,9 @@ Lemma condense_inverse :
 Proof.
   intros.
   destruct H.
-  apply L_DistributeOverSpec1.
+  apply L_DistributeOverApp.
-  apply L_DistributeOverSpec2.
   apply L_DistributeOverFun1.
   apply L_DistributeOverFun2.
-  apply L_DistributeOverMorph1.
-  apply L_DistributeOverMorph2.
 Qed.
 
 
@@ -171,23 +115,19 @@ Qed.
 
 Reserved Notation " S '===' T " (at level 40).
 Inductive type_eq : type_term -> type_term -> Prop :=
-  | TEq_Refl : forall x,
+  | L_Refl : forall x,
     x === x
 
-  | TEq_Trans : forall x y z,
+  | L_Trans : forall x y z,
     x === y ->
     y === z ->
     x === z
 
-  | TEq_Rename : forall x y,
+  | L_Distribute : forall x y,
-    x -->α y ->
-    x === y
-
-  | TEq_Distribute : forall x y,
     x -->distribute-ladder y ->
     x === y
 
-  | TEq_Condense : forall x y,
+  | L_Condense : forall x y,
     x -->condense-ladder y ->
     x === y
 
@@ -203,23 +143,24 @@ Proof.
   intros.
   induction H.
   
-  apply TEq_Refl.
+  1:{
+    apply L_Refl.
+  }
 
-  apply TEq_Trans with (y:=y).
+  2:{
+    apply L_Condense.
+    apply distribute_inverse.
+    apply H.
+  }
+  2:{
+    apply L_Distribute.
+    apply condense_inverse.
+    apply H.
+  }
+
+  apply L_Trans with (y:=y).
   apply IHtype_eq2.
   apply IHtype_eq1.
-
-  apply type_alpha_symm in H.
-  apply TEq_Rename.
-  apply H.
-
-  apply TEq_Condense.
-  apply distribute_inverse.
-  apply H.
-
-  apply TEq_Distribute.
-  apply condense_inverse.
-  apply H.
 Qed.
 
 (** "flat" types do not contain ladders $\label{coq:type-flat}$ *)
@@ -296,26 +237,25 @@ Proof.
   destruct t.
 
   exists type_unit.
-  split. apply TEq_Refl.
+  split. apply L_Refl.
   apply LNF.
   admit.
   
   exists (type_id s).
-  split. apply TEq_Refl.
+  split. apply L_Refl.
   apply LNF.
   admit.
   admit.
   
   exists (type_num n).
-  split. apply TEq_Refl.
+  split. apply L_Refl.
   apply LNF.
   admit.
   
   admit.
   
   exists (type_univ s t).
-  split.
+  split. apply L_Refl.
-  apply TEq_Refl.
   apply LNF.
   
 Admitted.
@@ -362,8 +302,8 @@ Example example_type_eq :
     (type_ladder (type_spec (type_id "Seq") (type_id "Char"))
                (type_spec (type_id "Seq") (type_id "Byte"))).
 Proof.
-  apply TEq_Distribute.
+  apply L_Distribute.
-  apply L_DistributeOverSpec2.
+  apply L_DistributeOverApp.
 Qed.
 
 

coq/smallstep.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' ->

coq/subtype.v

@@ -1,96 +0,0 @@
-(*
- * This module defines the subtype relationship
- *
- * We distinguish between *representational* subtypes,
- * where any high-level type is a subtype of its underlying
- * representation type and *convertible* subtypes that
- * are compatible at high level, but have a different representation
- * that requires a conversion.
- *)
-
-From Coq Require Import Strings.String.
-Require Import terms.
-Require Import equiv.
-Include Terms.
-Include Equiv.
-
-Module Subtype.
-
-(** Subtyping *)
-
-Reserved Notation "s ':<=' t" (at level 50).
-Reserved Notation "s '~<=' t" (at level 50).
-
-(* Representational Subtype *)
-Inductive is_repr_subtype : type_term -> type_term -> Prop :=
-	| TSubRepr_Refl : forall t t', (t === t') -> (t :<= t')
-	| TSubRepr_Trans : forall x y z, (x :<= y) -> (y :<= z) -> (x :<= z)
-	| TSubRepr_Ladder : forall x' x y, (x :<= y) -> ((type_ladder x' x) :<= y)
-where "s ':<=' t" := (is_repr_subtype s t).
-
-(* Convertible Subtype *)
-Inductive is_conv_subtype : type_term -> type_term -> Prop :=
-	| TSubConv_Refl : forall t t', (t === t') -> (t ~<= t')
-	| TSubConv_Trans : forall x y z, (x ~<= y) -> (y ~<= z) -> (x ~<= z)
-	| TSubConv_Ladder : forall x' x y, (x ~<= y) -> ((type_ladder x' x) ~<= y)
-	| TSubConv_Morph : forall x y y', (type_ladder x y) ~<= (type_ladder x y')
-where "s '~<=' t" := (is_conv_subtype s t).
-
-
-(* Every Representational Subtype is a Convertible Subtype *)
-
-Lemma syn_sub_is_sem_sub : forall x y, (x :<= y) -> (x ~<= y).
-Proof.
-	intros.
-	induction H.
-	apply TSubConv_Refl.
-	apply H.
-	apply TSubConv_Trans with (x:=x) (y:=y) (z:=z).
-	apply IHis_repr_subtype1.
-	apply IHis_repr_subtype2.
-	apply TSubConv_Ladder.
-	apply IHis_repr_subtype.
-Qed.
-
-
-
-
-(* EXAMPLES *)
-
-Open Scope ladder_type_scope.
-Open Scope ladder_expr_scope.
-
-Example sub0 :
-  [   < $"Seq"$ < $"Digit"$ $"10"$ > >
-    ~ < $"Seq"$ $"Char"$ > ]
-:<=
-  [   < $"Seq"$ $"Char"$ > ]
-.
-Proof.
-  apply TSubRepr_Ladder.
-  apply TSubRepr_Refl.
-	apply TEq_Refl.
-Qed.
-
-
-Example sub1 :
-    [ < $"Seq"$ < $"Digit"$ $"10"$ > ~ $"Char"$ > ]
-:<= [ < $"Seq"$ $"Char"$ > ]
-.
-Proof.
-  set [ < $"Seq"$ < $"Digit"$ $"10"$ > > ~ < $"Seq"$ $"Char"$ > ].
-	set [ < $"Seq"$ < $"Digit"$ $"10"$ > ~ $"Char"$ > ].
-	set [ < $"Seq"$ $"Char"$ > ].
-	set (t0 === t).
-	set (t :<= t0).
-	set (t :<= t1).
-	apply TSubRepr_Trans with t.
-	apply TSubRepr_Refl.
-	apply TEq_Distribute.
-	apply L_DistributeOverSpec2.
-	apply TSubRepr_Ladder.
-	apply TSubRepr_Refl.
-	apply TEq_Refl.
-Qed.
-
-End Subtype.

coq/typing.v

@@ -4,11 +4,66 @@
 From Coq Require Import Strings.String.
 Require Import terms.
 Require Import subst.
+Require Import equiv.
 Include Terms.
 Include Subst.
+Include Equiv.
 
 Module Typing.
 
+
+(** Subtyping *)
+
+Reserved Notation "s ':<=' t" (at level 50).
+Reserved Notation "s '~=~' t" (at level 50).
+
+Inductive is_syntactic_subtype : type_term -> type_term -> Prop :=
+  | S_Refl : forall t t', (t === t') -> (t :<= t')
+  | S_Trans : forall x y z, (x :<= y) -> (y :<= z) -> (x :<= z)
+  | S_SynRepr : forall x' x y, (x :<= y) -> ((type_ladder x' x) :<= y)
+where "s ':<=' t" := (is_syntactic_subtype s t).
+
+Inductive is_semantic_subtype : type_term -> type_term -> Prop :=
+  | S_Synt : forall x y,
+    (x :<= y) -> (x ~=~ y)
+
+  | S_SemRepr : forall x y y',
+    (type_ladder x y) ~=~ (type_ladder x y')
+where "s '~=~' t" := (is_semantic_subtype s t).
+
+
+Open Scope ladder_type_scope.
+
+Example sub0 :
+  [   < $"Seq"$ < $"Digit"$ $"10"$ > >
+    ~ < $"Seq"$ $"Char"$ > ]
+  :<=
+  [   < $"Seq"$ $"Char"$ > ]
+.
+Proof.
+apply S_SynRepr.
+apply S_Refl.
+apply L_Refl.
+Qed.
+
+Example sub1 :
+  [ < $"Seq"$ < $"Digit"$ $"10"$ > ~ $"Char"$ > ]
+  :<= [ < $"Seq"$ $"Char"$ > ]
+.
+Proof.
+  set [ < $"Seq"$ < $"Digit"$ $"10"$ > > ~ < $"Seq"$ $"Char"$ > ].
+  set [ < $"Seq"$ < $"Digit"$ $"10"$ > ~ $"Char"$ > ].
+  set [ < $"Seq"$ $"Char"$ > ].
+  set (t0 === t).
+  set (t :<= t0).
+  set (t :<= t2).
+  apply S_Trans with t1.
+  apply S_Refl.
+Qed.
+
+
+(** Typing Derivation *)
+
 Inductive context : Type :=
   | ctx_assign : string -> type_term -> context -> context
   | ctx_empty : context
@@ -17,7 +72,8 @@ Inductive context : Type :=
 Inductive context_contains : context -> string -> type_term -> Prop :=
   | C_take : forall (x:string) (X:type_term) (Γ:context),
     (context_contains (ctx_assign x X Γ) x X)
-  | C_shuffle : forall x X y Y Γ,
+
+  | C_shuffle : forall x X y Y (Γ:context),
     (context_contains Γ x X) ->
     (context_contains (ctx_assign y Y Γ) x X).
 
@@ -27,7 +83,7 @@ Reserved Notation "Gamma '|-' x '\compatible' X"  (at level 101, x at next level
 Inductive expr_type : context -> expr_term -> type_term -> Prop :=
   | T_Var : forall Γ x τ,
     (context_contains Γ x τ) ->
-    (Γ |- (expr_var x) \is τ)
+    (Γ |- x \is τ)
 
   | T_Let : forall Γ s (σ:type_term) t τ x,
     (Γ |- s \is σ) ->
@@ -55,6 +111,7 @@ Inductive expr_type : context -> expr_term -> type_term -> Prop :=
 where "Γ '|-' x '\is' τ" := (expr_type Γ x τ).
 
 
+
 Inductive expr_type_compatible : context -> expr_term -> type_term -> Prop :=
 
   | T_Compatible : forall Γ x τ,

paper/main.tex

@@ -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}.
+This work explores the idea of \emph{representational polymorphism}
-Using ladder-types, multi-layered embeddings of higher-level data-types into lower-level data-types can be described by a type-level structure.
+to treat the coexistence of multiple equivalent representational forms for a single abstract concept.
-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.
+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})\)