coq: add subtype relations

coq/_CoqProject

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

coq/equiv.v

@@ -30,18 +30,43 @@
  * 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_DistributeOverApp : forall x y y',
+  | L_DistributeOverSpec1 : forall x x' 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'))
@@ -56,13 +81,28 @@ 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_CondenseOverApp : forall x y y',
+  | L_CondenseOverSpec1 : forall x x' 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'))
@@ -77,6 +117,16 @@ 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).
 
 
@@ -90,9 +140,12 @@ Lemma distribute_inverse :
 Proof.
   intros.
   destruct H.
-  apply L_CondenseOverApp.
+  apply L_CondenseOverSpec1.
+  apply L_CondenseOverSpec2.
   apply L_CondenseOverFun1.
   apply L_CondenseOverFun2.
+  apply L_CondenseOverMorph1.
+  apply L_CondenseOverMorph2.
 Qed.
 
 (** Inversion Lemma:
@@ -105,9 +158,12 @@ Lemma condense_inverse :
 Proof.
   intros.
   destruct H.
-  apply L_DistributeOverApp.
+  apply L_DistributeOverSpec1.
+  apply L_DistributeOverSpec2.
   apply L_DistributeOverFun1.
   apply L_DistributeOverFun2.
+  apply L_DistributeOverMorph1.
+  apply L_DistributeOverMorph2.
 Qed.
 
 
@@ -115,19 +171,23 @@ Qed.
 
 Reserved Notation " S '===' T " (at level 40).
 Inductive type_eq : type_term -> type_term -> Prop :=
-  | L_Refl : forall x,
+  | TEq_Refl : forall x,
     x === x
 
-  | L_Trans : forall x y z,
+  | TEq_Trans : forall x y z,
     x === y ->
     y === z ->
     x === z
 
-  | L_Distribute : forall x y,
+  | TEq_Rename : forall x y,
+    x -->α y ->
+    x === y
+
+  | TEq_Distribute : forall x y,
     x -->distribute-ladder y ->
     x === y
 
-  | L_Condense : forall x y,
+  | TEq_Condense : forall x y,
     x -->condense-ladder y ->
     x === y
 
@@ -143,24 +203,23 @@ Proof.
   intros.
   induction H.
   
-  1:{
+  apply TEq_Refl.
-    apply L_Refl.
-  }
 
-  2:{
+  apply TEq_Trans with (y:=y).
-    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}$ *)
@@ -237,25 +296,26 @@ Proof.
   destruct t.
 
   exists type_unit.
-  split. apply L_Refl.
+  split. apply TEq_Refl.
   apply LNF.
   admit.
   
   exists (type_id s).
-  split. apply L_Refl.
+  split. apply TEq_Refl.
   apply LNF.
   admit.
   admit.
   
   exists (type_num n).
-  split. apply L_Refl.
+  split. apply TEq_Refl.
   apply LNF.
   admit.
   
   admit.
   
   exists (type_univ s t).
-  split. apply L_Refl.
+  split.
+  apply TEq_Refl.
   apply LNF.
   
 Admitted.
@@ -302,8 +362,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 L_Distribute.
+  apply TEq_Distribute.
-  apply L_DistributeOverApp.
+  apply L_DistributeOverSpec2.
 Qed.
 
 

coq/smallstep.v

@@ -9,22 +9,10 @@ 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

@@ -0,0 +1,96 @@
+(*
+ * 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,66 +4,11 @@
 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
@@ -72,8 +17,7 @@ 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).
 
@@ -83,7 +27,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 τ) ->
-    (Γ |- x \is τ)
+    (Γ |- (expr_var x) \is τ)
 
   | T_Let : forall Γ s (σ:type_term) t τ x,
     (Γ |- s \is σ) ->
@@ -111,7 +55,6 @@ 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,25 +52,11 @@
 
 
 \begin{abstract}
-This work explores the idea of \emph{representational polymorphism}
+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}.
-to treat the coexistence of multiple equivalent representational forms for a single abstract concept.
+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}.
-interchangeability
+Further we show how the Boehm-Berarducci encoding can be used to implement algebraic datatypes on the basis of the introduced core calculus.
-%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
@@ -78,29 +64,6 @@ and prove its \emph{soundness}.
 
 
 %\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}
 
@@ -338,6 +301,7 @@ 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})\)