From b0035e711a9cfab84fa3358d2777256e1f539029 Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Wed, 21 Aug 2024 20:19:03 +0200 Subject: [PATCH] wip --- coq/_CoqProject | 2 +- coq/smallstep.v | 12 ++++++++++++ coq/soundness.v | 1 + paper/main.tex | 50 ++++++++++++++++++++++++++++++++++++++++++------- 4 files changed, 57 insertions(+), 8 deletions(-) create mode 100644 coq/soundness.v diff --git a/coq/_CoqProject b/coq/_CoqProject index dd816a6..bf211ac 100644 --- a/coq/_CoqProject +++ b/coq/_CoqProject @@ -5,5 +5,5 @@ subst.v subtype.v typing.v smallstep.v +soundness.v bbencode.v - diff --git a/coq/smallstep.v b/coq/smallstep.v index c3da0a3..cb10874 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/soundness.v b/coq/soundness.v new file mode 100644 index 0000000..8b13789 --- /dev/null +++ b/coq/soundness.v @@ -0,0 +1 @@ + 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})\)