Compare commits
3 commits
b0035e711a
...
4323e7d09f
Author | SHA1 | Date | |
---|---|---|---|
4323e7d09f | |||
ad107759bf | |||
39f312b401 |
8 changed files with 104 additions and 90 deletions
|
@ -5,5 +5,5 @@ subst.v
|
|||
subtype.v
|
||||
typing.v
|
||||
smallstep.v
|
||||
soundness.v
|
||||
bbencode.v
|
||||
|
||||
|
|
|
@ -1,4 +1,5 @@
|
|||
From Coq Require Import Strings.String.
|
||||
|
||||
Require Import terms.
|
||||
Require Import subst.
|
||||
Require Import smallstep.
|
||||
|
@ -7,35 +8,37 @@ 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_tm_abs "s" (type_fun (type_var "α") (type_var "α"))
|
||||
(expr_tm_abs "z" (type_var "α")
|
||||
(expr_abs "s" (type_fun (type_var "α") (type_var "α"))
|
||||
(expr_abs "z" (type_var "α")
|
||||
(expr_var "z")))).
|
||||
|
||||
(* let bb_one = Λα ↦ λs: α->α ↦ λz: α ↦ s z
|
||||
*)
|
||||
Definition bb_one : expr_term :=
|
||||
(expr_ty_abs "α"
|
||||
(expr_tm_abs "s" (type_fun (type_var "α") (type_var "α"))
|
||||
(expr_tm_abs "z" (type_var "α")
|
||||
(expr_tm_app (expr_var "s") (expr_var "z"))))).
|
||||
(expr_abs "s" (type_fun (type_var "α") (type_var "α"))
|
||||
(expr_abs "z" (type_var "α")
|
||||
(expr_app (expr_var "s") (expr_var "z"))))).
|
||||
|
||||
(* let bb_two = Λα ↦ λs: α->α ↦ λz: α ↦ s (s z)
|
||||
*)
|
||||
Definition bb_two : expr_term :=
|
||||
(expr_ty_abs "α"
|
||||
(expr_tm_abs "s" (type_fun (type_var "α") (type_var "α"))
|
||||
(expr_tm_abs "z" (type_var "α")
|
||||
(expr_tm_app (expr_var "s") (expr_tm_app (expr_var "s") (expr_var "z")))))).
|
||||
(expr_abs "s" (type_fun (type_var "α") (type_var "α"))
|
||||
(expr_abs "z" (type_var "α")
|
||||
(expr_app (expr_var "s") (expr_app (expr_var "s") (expr_var "z")))))).
|
||||
|
||||
|
||||
Definition bb_succ : expr_term :=
|
||||
(expr_tm_abs "n" (type_ladder (type_id "ℕ")
|
||||
(expr_abs "n" (type_ladder (type_id "ℕ")
|
||||
(type_ladder (type_id "BBNat")
|
||||
(type_univ "α"
|
||||
(type_fun (type_fun (type_var "α") (type_var "α"))
|
||||
|
@ -43,10 +46,10 @@ Definition bb_succ : expr_term :=
|
|||
|
||||
(expr_ascend (type_ladder (type_id "ℕ") (type_id "BBNat"))
|
||||
(expr_ty_abs "α"
|
||||
(expr_tm_abs "s" (type_fun (type_var "α") (type_var "α"))
|
||||
(expr_tm_abs "z" (type_var "α")
|
||||
(expr_tm_app (expr_var "s")
|
||||
(expr_tm_app (expr_tm_app
|
||||
(expr_abs "s" (type_fun (type_var "α") (type_var "α"))
|
||||
(expr_abs "z" (type_var "α")
|
||||
(expr_app (expr_var "s")
|
||||
(expr_app (expr_app
|
||||
(expr_ty_app (expr_var "n") (type_var "α"))
|
||||
(expr_var "s"))
|
||||
(expr_var "z")))))))).
|
||||
|
@ -58,25 +61,25 @@ Definition e1 : expr_term :=
|
|||
(type_fun (type_fun (type_var "α") (type_var "α"))
|
||||
(type_fun (type_var "α") (type_var "α"))))))
|
||||
bb_zero
|
||||
(expr_tm_app (expr_tm_app (expr_var "+") (expr_var "bb-zero")) (expr_var "bb-zero"))
|
||||
(expr_app (expr_app (expr_var "+") (expr_var "bb-zero")) (expr_var "bb-zero"))
|
||||
).
|
||||
|
||||
Definition t1 : expr_term := (expr_tm_app (expr_var "x") (expr_var "x")).
|
||||
Definition t1 : expr_term := (expr_app (expr_var "x") (expr_var "x")).
|
||||
|
||||
Compute (expr_subst "x"
|
||||
(expr_ty_abs "α" (expr_tm_abs "a" (type_var "α") (expr_var "a")))
|
||||
(expr_ty_abs "α" (expr_abs "a" (type_var "α") (expr_var "a")))
|
||||
bb_one
|
||||
).
|
||||
|
||||
Example example_let_reduction :
|
||||
e1 -->β (expr_tm_app (expr_tm_app (expr_var "+") bb_zero) bb_zero).
|
||||
e1 -->β (expr_app (expr_app (expr_var "+") bb_zero) bb_zero).
|
||||
Proof.
|
||||
apply E_AppLet.
|
||||
Qed.
|
||||
|
||||
Compute (expr_tm_app bb_succ bb_zero) -->β bb_one.
|
||||
Compute (expr_app bb_succ bb_zero) -->β bb_one.
|
||||
|
||||
Example example_succ :
|
||||
(expr_tm_app bb_succ bb_zero) -->β bb_one.
|
||||
(expr_app bb_succ bb_zero) -->β bb_one.
|
||||
Proof.
|
||||
Admitted.
|
||||
|
|
|
@ -11,28 +11,50 @@ 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).
|
||||
Inductive expr_alpha : expr_term -> expr_term -> Prop :=
|
||||
| EAlpha_Rename : forall x x' τ e,
|
||||
(expr_abs x τ e) -->α (expr_abs x' τ (expr_subst x (expr_var x') e))
|
||||
|
||||
| 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_tm_app e1 e2) -->β (expr_tm_app e1' e2)
|
||||
(expr_app e1 e2) -->β (expr_app e1' e2)
|
||||
|
||||
| E_App2 : forall e1 e2 e2',
|
||||
e2 -->β e2' ->
|
||||
(expr_tm_app e1 e2) -->β (expr_tm_app e1 e2')
|
||||
(expr_app e1 e2) -->β (expr_app e1 e2')
|
||||
|
||||
| E_TypApp : forall e e' τ,
|
||||
e -->β e' ->
|
||||
|
@ -81,8 +103,7 @@ 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.
|
||||
|
|
|
@ -1 +0,0 @@
|
|||
|
|
@ -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_tm_abs x t e => if (eqb v x) then e0 else expr_tm_abs 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_tm_app e a => expr_tm_app (expr_subst v n e) (expr_subst v n a)
|
||||
| expr_abs x t e => if (eqb v x) then e0 else expr_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_app e a => expr_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)
|
||||
|
|
18
coq/terms.v
18
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_tm_abs : string -> type_term -> expr_term -> expr_term
|
||||
| expr_tm_abs_morph : string -> type_term -> expr_term -> expr_term
|
||||
| expr_tm_app : expr_term -> expr_term -> expr_term
|
||||
| expr_abs : string -> type_term -> expr_term -> expr_term
|
||||
| expr_morph : string -> type_term -> expr_term -> expr_term
|
||||
| expr_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_ValAbs : forall x τ e,
|
||||
(is_value (expr_tm_abs x τ e))
|
||||
| V_Abs : forall x τ e,
|
||||
(is_value (expr_abs x τ e))
|
||||
|
||||
| V_TypAbs : forall τ e,
|
||||
(is_value (expr_ty_abs τ e))
|
||||
|
@ -43,6 +43,8 @@ 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.
|
||||
|
@ -71,10 +73,14 @@ 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 "'λ' 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 "'Λ' 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.
|
||||
|
||||
|
|
35
coq/typing.v
35
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_tm_abs x σ t) \is (type_fun σ τ)
|
||||
Γ |- (expr_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_tm_app f a) \is τ
|
||||
Γ |- (expr_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_tm_abs_morph x τ t) \compatible (type_morph τ τ')
|
||||
Γ |- (expr_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_tm_abs x σ t) \compatible (type_fun σ τ)
|
||||
Γ |- (expr_abs x σ t) \compatible (type_fun σ τ)
|
||||
|
||||
| T_CompatApp : forall Γ f a σ τ,
|
||||
(Γ |- f \compatible (type_fun σ τ)) ->
|
||||
(Γ |- a \compatible σ) ->
|
||||
(Γ |- (expr_tm_app f a) \compatible τ)
|
||||
(Γ |- (expr_app f a) \compatible τ)
|
||||
|
||||
| T_CompatImplicitCast : forall Γ h x τ τ',
|
||||
(context_contains Γ h (type_morph τ τ')) ->
|
||||
|
@ -112,10 +112,13 @@ 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"% ]) ->
|
||||
|
@ -134,7 +137,6 @@ 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"%)]).
|
||||
|
@ -188,4 +190,23 @@ 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.
|
||||
|
|
|
@ -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}
|
||||
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}.
|
||||
|
||||
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.
|
||||
\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})\)
|
||||
|
|
Loading…
Reference in a new issue