wip

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/terms.v

@@ -32,40 +32,62 @@ Inductive expr_term : Type :=
   | expr_descend : type_term -> expr_term -> expr_term
 .
 
-Coercion type_var : string >-> type_term.
-Coercion expr_var : string >-> expr_term.
+(* values *)
+Inductive is_value : expr_term -> Prop :=
+  | V_ValAbs : forall x τ e,
+    (is_value (expr_tm_abs x τ e))
 
-(*
-Coercion type_var : string >-> type_term.
-Coercion expr_var : string >-> expr_term.
-*)
+  | V_TypAbs : forall τ e,
+    (is_value (expr_ty_abs τ e))
+
+  | V_Ascend : forall τ e,
+    (is_value e) ->
+    (is_value (expr_ascend τ e))
+.
 
 Declare Scope ladder_type_scope.
 Declare Scope ladder_expr_scope.
 Declare Custom Entry ladder_type.
+Declare Custom Entry ladder_expr.
 
-Notation "[ e ]" := e (e custom ladder_type at level 80) : ladder_type_scope.
+Notation "[ t ]" := t
+  (t custom ladder_type at level 80) : 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 σ τ)
+  (in custom ladder_type at level 80, left associativity) : ladder_type_scope.
+Notation "'(' τ ')'" := τ
+  (in custom ladder_type at level 70) : ladder_type_scope.
+Notation "σ '->' τ" := (type_fun σ τ)
+  (in custom ladder_type at level 75, right associativity) : ladder_type_scope.
+Notation "σ '->morph' τ" := (type_morph σ τ)
+  (in custom ladder_type at level 75, right associativity, τ at level 80) : ladder_type_scope.
+Notation "σ '~' τ" := (type_ladder σ τ)
+  (in custom ladder_type at level 70, right associativity) : ladder_type_scope.
+Notation "'$' x '$'" := (type_id x%string)
+  (in custom ladder_type at level 0, x constr) : ladder_type_scope.
+Notation "'%' x '%'" := (type_var x%string)
+  (in custom ladder_type at level 0, x constr) : ladder_type_scope.
 
-(* TODO: allow any variable names in notation, not just α,β,γ *)
-Notation "'∀α.' τ" := (type_univ "α" τ) (in custom ladder_type at level 80) : ladder_type_scope.
-Notation "'∀β.' τ" := (type_univ "β" τ) (in custom ladder_type at level 80) : ladder_type_scope.
-Notation "'∀γ.' τ" := (type_univ "γ" τ) (in custom ladder_type at level 80) : ladder_type_scope.
-Notation "'<' σ τ '>'" := (type_spec σ τ) (in custom ladder_type at level 80, left associativity) : ladder_type_scope.
-Notation "'(' τ ')'" := τ (in custom ladder_type at level 70) : ladder_type_scope.
-Notation "σ '->' τ" := (type_fun σ τ) (in custom ladder_type at level 75, right associativity) : ladder_type_scope.
-Notation "σ '->morph' τ" := (type_morph σ τ) (in custom ladder_type at level 75, right associativity) : ladder_type_scope.
-Notation "σ '~' τ" := (type_ladder σ τ) (in custom ladder_type at level 70, right associativity) : ladder_type_scope.
-Notation "'α'" := (type_var "α") (in custom ladder_type at level 60, right associativity) : ladder_type_scope.
-Notation "'β'" := (type_var "β") (in custom ladder_type at level 60, right associativity) : ladder_type_scope.
-Notation "'γ'" := (type_var "γ") (in custom ladder_type at level 60, right associativity) : ladder_type_scope.
+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_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).
 
 Open Scope ladder_type_scope.
+Open Scope ladder_expr_scope.
 
-Definition t1 : type_term := [ ∀α.∀β.(α~β~γ)->β->(α->α)->β ].
+Check [ ∀"α", (< $"Seq"$ %"α"% > ~ < $"List"$ %"α"% >) ].
+
+Definition polymorphic_identity1 : expr_term := [[ Λ"T" ↦ λ"x"%"T"% ↦ %"x"% ]].
+Definition polymorphic_identity2 : expr_term := [[ Λ"T" ↦ λ"y"%"T"% ↦ %"y"% ]].
+
+Compute polymorphic_identity1.
 
-Compute t1.
 Close Scope ladder_type_scope.
-
-
+Close Scope ladder_expr_scope.
 
 End Terms.

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).
 
@@ -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}.
-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}.
-Further we show how the Boehm-Berarducci encoding can be used to implement algebraic datatypes on the basis of the introduced core calculus.
+This work explores the idea of \emph{representational polymorphism}
+to treat the coexistence of multiple equivalent representational forms for a single abstract concept.
+
+
+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})\)