wip

coq/_CoqProject

@@ -5,5 +5,5 @@ subst.v
 subtype.v
 typing.v
 smallstep.v
+soundness.v
 bbencode.v
-

coq/bbencode.v

@@ -1,5 +1,4 @@
 From Coq Require Import Strings.String.
-
 Require Import terms.
 Require Import subst.
 Require Import smallstep.
@@ -8,37 +7,35 @@ Include Terms.
 Include Subst.
 Include Smallstep.
 
-Open Scope ladder_type_scope.
-Open Scope ladder_expr_scope.
 
 (*  let bb_zero = Λα ↦ λs: α->α ↦ λz: α ↦ z
  *                ∀α.(α->α)->α->α
 *)
 Definition bb_zero : expr_term :=
   (expr_ty_abs "α"
-    (expr_abs "s" (type_fun (type_var "α") (type_var "α"))
+    (expr_tm_abs "s" (type_fun (type_var "α") (type_var "α"))
-      (expr_abs "z" (type_var "α")
+      (expr_tm_abs "z" (type_var "α")
         (expr_var "z")))).
 
 (*  let bb_one = Λα ↦ λs: α->α ↦ λz: α ↦ s z
 *)
 Definition bb_one : expr_term :=
   (expr_ty_abs "α"
-    (expr_abs "s" (type_fun (type_var "α") (type_var "α"))
+    (expr_tm_abs "s" (type_fun (type_var "α") (type_var "α"))
-      (expr_abs "z" (type_var "α")
+      (expr_tm_abs "z" (type_var "α")
-        (expr_app (expr_var "s") (expr_var "z"))))).
+        (expr_tm_app (expr_var "s") (expr_var "z"))))).
 
 (*  let bb_two = Λα ↦ λs: α->α ↦ λz: α ↦ s (s z)
 *)
 Definition bb_two : expr_term :=
   (expr_ty_abs "α"
-    (expr_abs "s" (type_fun (type_var "α") (type_var "α"))
+    (expr_tm_abs "s" (type_fun (type_var "α") (type_var "α"))
-      (expr_abs "z" (type_var "α")
+      (expr_tm_abs "z" (type_var "α")
-        (expr_app (expr_var "s") (expr_app (expr_var "s") (expr_var "z")))))).
+        (expr_tm_app (expr_var "s") (expr_tm_app (expr_var "s") (expr_var "z")))))).
 
 
 Definition bb_succ : expr_term :=
-  (expr_abs "n" (type_ladder (type_id "ℕ")
+  (expr_tm_abs "n" (type_ladder (type_id "ℕ")
                     (type_ladder (type_id "BBNat")
                      (type_univ "α"
                       (type_fun (type_fun (type_var "α") (type_var "α"))
@@ -46,10 +43,10 @@ Definition bb_succ : expr_term :=
 
        (expr_ascend (type_ladder (type_id "ℕ") (type_id "BBNat"))
           (expr_ty_abs "α"
-            (expr_abs "s" (type_fun (type_var "α") (type_var "α"))
+            (expr_tm_abs "s" (type_fun (type_var "α") (type_var "α"))
-              (expr_abs "z" (type_var "α")
+              (expr_tm_abs "z" (type_var "α")
-                (expr_app (expr_var "s")
+                (expr_tm_app (expr_var "s")
-                  (expr_app (expr_app
+                  (expr_tm_app (expr_tm_app
                       (expr_ty_app (expr_var "n") (type_var "α"))
                       (expr_var "s"))
                     (expr_var "z")))))))).
@@ -61,25 +58,25 @@ Definition e1 : expr_term :=
                             (type_fun (type_fun (type_var "α") (type_var "α"))
                               (type_fun (type_var "α") (type_var "α"))))))
                        bb_zero
-                       (expr_app (expr_app (expr_var "+") (expr_var "bb-zero")) (expr_var "bb-zero"))
+                       (expr_tm_app (expr_tm_app (expr_var "+") (expr_var "bb-zero")) (expr_var "bb-zero"))
   ).
 
-Definition t1 : expr_term := (expr_app (expr_var "x") (expr_var "x")).
+Definition t1 : expr_term := (expr_tm_app (expr_var "x") (expr_var "x")).
 
 Compute (expr_subst "x"
-    (expr_ty_abs "α" (expr_abs "a" (type_var "α") (expr_var "a")))
+    (expr_ty_abs "α" (expr_tm_abs "a" (type_var "α") (expr_var "a")))
     bb_one
 ).
 
 Example  example_let_reduction :
-    e1 -->β  (expr_app (expr_app (expr_var "+") bb_zero) bb_zero).
+    e1 -->β  (expr_tm_app (expr_tm_app (expr_var "+") bb_zero) bb_zero).
 Proof.
     apply E_AppLet.
 Qed.
 
-Compute     (expr_app bb_succ bb_zero) -->β bb_one.
+Compute     (expr_tm_app bb_succ bb_zero) -->β bb_one.
 
 Example  example_succ :
-    (expr_app bb_succ bb_zero) -->β bb_one.
+    (expr_tm_app bb_succ bb_zero) -->β bb_one.
 Proof.
 Admitted.

coq/smallstep.v

@@ -11,50 +11,28 @@ 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 expr_alpha : expr_term -> expr_term -> Prop :=
+Inductive alpha_step : expr_term -> expr_term -> Prop :=
-  | EAlpha_Rename : forall x x' τ e,
+  | E_Rename : forall x x' e,
-    (expr_abs x τ e) -->α (expr_abs x' τ (expr_subst x (expr_var x') e))
+    (expr_tm_abs x e) -->α (expr_tm_abs x' (expr_subst x (type_var x')))
-
+where "s '-->α' t" := (alpha_step s t).
-  | EAlpha_TyRename : forall α α' e,
-    (expr_ty_abs α e) -->α (expr_ty_abs α' (expr_specialize α (type_var α') e))
-
-  | EAlpha_SubAbs : forall x τ e e',
-    (e -->α e') ->
-    (expr_abs x τ e) -->α (expr_abs x τ e')
-
-  | EAlpha_SubTyAbs : forall α e e',
-    (e -->α e') ->
-    (expr_ty_abs α e) -->α (expr_ty_abs α e')
-
-  | EAlpha_SubApp1 : forall e1 e1' e2,
-    (e1 -->α e1') ->
-    (expr_app e1 e2) -->α (expr_app e1' e2)
-
-  | EAlpha_SubApp2 : forall e1 e2 e2',
-    (e2 -->α e2') ->
-    (expr_app e1 e2) -->α (expr_app e1 e2')
-
-where "s '-->α' t" := (expr_alpha s t).
 
 
 Example a1 : polymorphic_identity1 -->α polymorphic_identity2.
 Proof.
-  unfold polymorphic_identity1.
-  unfold polymorphic_identity2.
-  apply EAlpha_SubTyAbs.
-  apply EAlpha_Rename.
 Qed.
 
 
 Inductive beta_step : expr_term -> expr_term -> Prop :=
   | E_App1 : forall e1 e1' e2,
     e1 -->β e1' ->
-    (expr_app e1 e2) -->β (expr_app e1' e2)
+    (expr_tm_app e1 e2) -->β (expr_tm_app e1' e2)
 
   | E_App2 : forall e1 e2 e2',
     e2 -->β e2' ->
-    (expr_app e1 e2) -->β (expr_app e1 e2')
+    (expr_tm_app e1 e2) -->β (expr_tm_app e1 e2')
 
   | E_TypApp : forall e e' τ,
     e -->β e' ->
@@ -103,7 +81,8 @@ Inductive multi {X : Type} (R : X -> X -> Prop) : X -> X -> Prop :=
                     multi R y z ->
                     multi R x z.
 
-Notation " s -->α* t " := (multi expr_alpha s t) (at level 40).
 Notation " s -->β* t " := (multi beta_step s t) (at level 40).
+Notation " s -->δ* t " := (multi delta_step s t) (at level 40).
+Notation " s -->eval* t " := (multi eval_step s t) (at level 40).
 
 End Smallstep.

coq/soundness.v

@@ -0,0 +1 @@
+

coq/subst.v

@@ -112,9 +112,9 @@ Fixpoint expr_subst (v:string) (n:expr_term) (e0:expr_term) :=
   | expr_var name => if (eqb v name) then n else e0
   | expr_ty_abs x e => if (eqb v x) then e0 else expr_ty_abs x (expr_subst v n e)
   | expr_ty_app e t => expr_ty_app (expr_subst v n e) t
-  | expr_abs x t e => if (eqb v x) then e0 else expr_abs x t (expr_subst v n e)
+  | expr_tm_abs x t e => if (eqb v x) then e0 else expr_tm_abs x t (expr_subst v n e)
-  | expr_morph x t e => if (eqb v x) then e0 else expr_morph x t (expr_subst v n e)
+  | expr_tm_abs_morph x t e => if (eqb v x) then e0 else expr_tm_abs_morph x t (expr_subst v n e)
-  | expr_app e a => expr_app (expr_subst v n e) (expr_subst v n a)
+  | expr_tm_app e a => expr_tm_app (expr_subst v n e) (expr_subst v n a)
   | expr_let x t a e => expr_let x t (expr_subst v n a) (expr_subst v n e)
   | expr_ascend t e => expr_ascend t (expr_subst v n e)
   | expr_descend t e => expr_descend t (expr_subst v n e)

coq/terms.v

@@ -22,9 +22,9 @@ Inductive expr_term : Type :=
   | expr_var : string -> expr_term
   | expr_ty_abs : string -> expr_term -> expr_term
   | expr_ty_app : expr_term -> type_term -> expr_term
-  | expr_abs   : string -> type_term -> expr_term -> expr_term
+  | expr_tm_abs : string -> type_term -> expr_term -> expr_term
-  | expr_morph : string -> type_term -> expr_term -> expr_term
+  | expr_tm_abs_morph : string -> type_term -> expr_term -> expr_term
-  | expr_app : expr_term -> expr_term -> expr_term
+  | expr_tm_app : expr_term -> expr_term -> expr_term
   | expr_let : string -> type_term -> expr_term -> expr_term -> expr_term
   | expr_ascend : type_term -> expr_term -> expr_term
   | expr_descend : type_term -> expr_term -> expr_term
@@ -32,8 +32,8 @@ Inductive expr_term : Type :=
 
 (* values *)
 Inductive is_value : expr_term -> Prop :=
-  | V_Abs : forall x τ e,
+  | V_ValAbs : forall x τ e,
-    (is_value (expr_abs x τ e))
+    (is_value (expr_tm_abs x τ e))
 
   | V_TypAbs : forall τ e,
     (is_value (expr_ty_abs τ e))
@@ -43,8 +43,6 @@ Inductive is_value : expr_term -> Prop :=
     (is_value (expr_ascend τ e))
 .
 
-
-
 Declare Scope ladder_type_scope.
 Declare Scope ladder_expr_scope.
 Declare Custom Entry ladder_type.
@@ -73,14 +71,10 @@ Notation "[[ e ]]" := e
   (e custom ladder_expr at level 80) : ladder_expr_scope.
 Notation "'%' x '%'" := (expr_var x%string)
   (in custom ladder_expr at level 0, x constr) : ladder_expr_scope.
-Notation "'λ' x τ '↦' e" := (expr_abs x τ e) (in custom ladder_expr at level 0, x constr, τ custom ladder_type at level 99, e custom ladder_expr at level 99).
+Notation "'λ' x τ '↦' e" := (expr_tm_abs x τ e) (in custom ladder_expr at level 0, x constr, τ custom ladder_type at level 99, e custom ladder_expr at level 99).
 Notation "'Λ' t '↦' e" := (expr_ty_abs t e)
   (in custom ladder_expr at level 0, t constr, e custom ladder_expr at level 80).
 
-
-
-(* EXAMPLES *)
-
 Open Scope ladder_type_scope.
 Open Scope ladder_expr_scope.
 

coq/typing.v

@@ -52,12 +52,12 @@ Inductive expr_type : context -> expr_term -> type_term -> Prop :=
   | T_Abs : forall (Γ:context) (x:string) (σ:type_term) (t:expr_term) (τ:type_term),
     (context_contains Γ x σ) ->
     Γ |- t \is τ ->
-    Γ |- (expr_abs x σ t) \is (type_fun σ τ)
+    Γ |- (expr_tm_abs x σ t) \is (type_fun σ τ)
 
   | T_App : forall (Γ:context) (f:expr_term) (a:expr_term) (σ:type_term) (τ:type_term),
     Γ |- f \is (type_fun σ τ) ->
     Γ |- a \is σ ->
-    Γ |- (expr_app f a) \is τ
+    Γ |- (expr_tm_app f a) \is τ
 
   | T_Sub : forall Γ x τ τ',
     Γ |- x \is τ ->
@@ -88,17 +88,17 @@ Inductive expr_type_compatible : context -> expr_term -> type_term -> Prop :=
   | T_CompatMorphAbs : forall Γ x t τ τ',
     Γ |- t \compatible τ ->
     (τ ~<= τ') ->
-    Γ |- (expr_morph x τ t) \compatible (type_morph τ τ')
+    Γ |- (expr_tm_abs_morph x τ t) \compatible (type_morph τ τ')
 
   | T_CompatAbs : forall (Γ:context) (x:string) (σ:type_term) (t:expr_term) (τ:type_term),
     (context_contains Γ x σ) ->
     Γ |- t \compatible τ ->
-    Γ |- (expr_abs x σ t) \compatible (type_fun σ τ)
+    Γ |- (expr_tm_abs x σ t) \compatible (type_fun σ τ)
 
   | T_CompatApp : forall Γ f a σ τ,
     (Γ |- f \compatible (type_fun σ τ)) ->
     (Γ |- a \compatible σ) ->
-    (Γ |- (expr_app f a) \compatible τ)
+    (Γ |- (expr_tm_app f a) \compatible τ)
 
   | T_CompatImplicitCast : forall Γ h x τ τ',
     (context_contains Γ h (type_morph τ τ')) ->
@@ -112,13 +112,10 @@ Inductive expr_type_compatible : context -> expr_term -> type_term -> Prop :=
 
 where "Γ '|-' x '\compatible' τ" := (expr_type_compatible Γ x τ).
 
-Definition is_well_typed (e:expr_term) : Prop :=
-  exists Γ τ,
-  Γ |- e \compatible τ
-.
 
 (* Examples *)
 
+
 Example typing1 :
   forall Γ,
   (context_contains Γ "x" [ %"T"% ]) ->
@@ -137,6 +134,7 @@ Example typing2 :
   forall Γ,
   (context_contains Γ "x" [ %"T"% ]) ->
   Γ |- [[ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% ]] \is [ ∀"U", %"U"% -> %"U"% ].
+   (* Γ |- [ ΛT ↦ λx:T ↦ x ] : ∀T.(T->T) *)
 Proof.
   intros.
   apply T_Sub with (τ:=[∀"T",(%"T"% -> %"T"%)]).
@@ -190,23 +188,4 @@ Proof.
   apply TSubst_VarReplace.
 Qed.
 
-
-Example typing4 : (is_well_typed
-  [[ Λ"T" ↦ Λ"U" ↦ λ"x" %"T"% ↦ λ"y" %"U"% ↦ %"x"% ]]
-).
-Proof.
-  unfold is_well_typed.
-  exists (ctx_assign "x" [%"T"%]
-            (ctx_assign "y" [%"U"%] ctx_empty)).
-  exists [ ∀"T",∀"U",%"T"%->%"U"%->%"T"% ].
-  apply T_CompatTypeAbs.
-  apply T_CompatTypeAbs.
-  apply T_CompatAbs.
-  apply C_take.
-  apply T_CompatAbs.
-  apply C_shuffle. apply C_take.
-  apply T_CompatVar.
-  apply C_take.
-Qed.
-
 End Typing.

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})\)