diff --git a/coq/smallstep.v b/coq/smallstep.v index c3da0a3..1efbdd4 100644 --- a/coq/smallstep.v +++ b/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' -> diff --git a/coq/terms.v b/coq/terms.v index 5d81179..b998fa7 100644 --- a/coq/terms.v +++ b/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. diff --git a/coq/typing.v b/coq/typing.v index e49b6af..be5b5a4 100644 --- a/coq/typing.v +++ b/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 τ, diff --git a/paper/main.tex b/paper/main.tex index 1073bc8..d61255c 100644 --- a/paper/main.tex +++ b/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})\)