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
|
subtype.v
|
||||||
typing.v
|
typing.v
|
||||||
smallstep.v
|
smallstep.v
|
||||||
soundness.v
|
|
||||||
bbencode.v
|
bbencode.v
|
||||||
|
|
||||||
|
|
|
@ -1,4 +1,5 @@
|
||||||
From Coq Require Import Strings.String.
|
From Coq Require Import Strings.String.
|
||||||
|
|
||||||
Require Import terms.
|
Require Import terms.
|
||||||
Require Import subst.
|
Require Import subst.
|
||||||
Require Import smallstep.
|
Require Import smallstep.
|
||||||
|
@ -7,35 +8,37 @@ Include Terms.
|
||||||
Include Subst.
|
Include Subst.
|
||||||
Include Smallstep.
|
Include Smallstep.
|
||||||
|
|
||||||
|
Open Scope ladder_type_scope.
|
||||||
|
Open Scope ladder_expr_scope.
|
||||||
|
|
||||||
(* let bb_zero = Λα ↦ λs: α->α ↦ λz: α ↦ z
|
(* let bb_zero = Λα ↦ λs: α->α ↦ λz: α ↦ z
|
||||||
* ∀α.(α->α)->α->α
|
* ∀α.(α->α)->α->α
|
||||||
*)
|
*)
|
||||||
Definition bb_zero : expr_term :=
|
Definition bb_zero : expr_term :=
|
||||||
(expr_ty_abs "α"
|
(expr_ty_abs "α"
|
||||||
(expr_tm_abs "s" (type_fun (type_var "α") (type_var "α"))
|
(expr_abs "s" (type_fun (type_var "α") (type_var "α"))
|
||||||
(expr_tm_abs "z" (type_var "α")
|
(expr_abs "z" (type_var "α")
|
||||||
(expr_var "z")))).
|
(expr_var "z")))).
|
||||||
|
|
||||||
(* let bb_one = Λα ↦ λs: α->α ↦ λz: α ↦ s z
|
(* let bb_one = Λα ↦ λs: α->α ↦ λz: α ↦ s z
|
||||||
*)
|
*)
|
||||||
Definition bb_one : expr_term :=
|
Definition bb_one : expr_term :=
|
||||||
(expr_ty_abs "α"
|
(expr_ty_abs "α"
|
||||||
(expr_tm_abs "s" (type_fun (type_var "α") (type_var "α"))
|
(expr_abs "s" (type_fun (type_var "α") (type_var "α"))
|
||||||
(expr_tm_abs "z" (type_var "α")
|
(expr_abs "z" (type_var "α")
|
||||||
(expr_tm_app (expr_var "s") (expr_var "z"))))).
|
(expr_app (expr_var "s") (expr_var "z"))))).
|
||||||
|
|
||||||
(* let bb_two = Λα ↦ λs: α->α ↦ λz: α ↦ s (s z)
|
(* let bb_two = Λα ↦ λs: α->α ↦ λz: α ↦ s (s z)
|
||||||
*)
|
*)
|
||||||
Definition bb_two : expr_term :=
|
Definition bb_two : expr_term :=
|
||||||
(expr_ty_abs "α"
|
(expr_ty_abs "α"
|
||||||
(expr_tm_abs "s" (type_fun (type_var "α") (type_var "α"))
|
(expr_abs "s" (type_fun (type_var "α") (type_var "α"))
|
||||||
(expr_tm_abs "z" (type_var "α")
|
(expr_abs "z" (type_var "α")
|
||||||
(expr_tm_app (expr_var "s") (expr_tm_app (expr_var "s") (expr_var "z")))))).
|
(expr_app (expr_var "s") (expr_app (expr_var "s") (expr_var "z")))))).
|
||||||
|
|
||||||
|
|
||||||
Definition bb_succ : expr_term :=
|
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_ladder (type_id "BBNat")
|
||||||
(type_univ "α"
|
(type_univ "α"
|
||||||
(type_fun (type_fun (type_var "α") (type_var "α"))
|
(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_ascend (type_ladder (type_id "ℕ") (type_id "BBNat"))
|
||||||
(expr_ty_abs "α"
|
(expr_ty_abs "α"
|
||||||
(expr_tm_abs "s" (type_fun (type_var "α") (type_var "α"))
|
(expr_abs "s" (type_fun (type_var "α") (type_var "α"))
|
||||||
(expr_tm_abs "z" (type_var "α")
|
(expr_abs "z" (type_var "α")
|
||||||
(expr_tm_app (expr_var "s")
|
(expr_app (expr_var "s")
|
||||||
(expr_tm_app (expr_tm_app
|
(expr_app (expr_app
|
||||||
(expr_ty_app (expr_var "n") (type_var "α"))
|
(expr_ty_app (expr_var "n") (type_var "α"))
|
||||||
(expr_var "s"))
|
(expr_var "s"))
|
||||||
(expr_var "z")))))))).
|
(expr_var "z")))))))).
|
||||||
|
@ -58,25 +61,25 @@ Definition e1 : expr_term :=
|
||||||
(type_fun (type_fun (type_var "α") (type_var "α"))
|
(type_fun (type_fun (type_var "α") (type_var "α"))
|
||||||
(type_fun (type_var "α") (type_var "α"))))))
|
(type_fun (type_var "α") (type_var "α"))))))
|
||||||
bb_zero
|
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"
|
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
|
bb_one
|
||||||
).
|
).
|
||||||
|
|
||||||
Example example_let_reduction :
|
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.
|
Proof.
|
||||||
apply E_AppLet.
|
apply E_AppLet.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Compute (expr_tm_app bb_succ bb_zero) -->β bb_one.
|
Compute (expr_app bb_succ bb_zero) -->β bb_one.
|
||||||
|
|
||||||
Example example_succ :
|
Example example_succ :
|
||||||
(expr_tm_app bb_succ bb_zero) -->β bb_one.
|
(expr_app bb_succ bb_zero) -->β bb_one.
|
||||||
Proof.
|
Proof.
|
||||||
Admitted.
|
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 '-->β' 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 :=
|
Inductive expr_alpha : expr_term -> expr_term -> Prop :=
|
||||||
| E_Rename : forall x x' e,
|
| EAlpha_Rename : forall x x' τ e,
|
||||||
(expr_tm_abs x e) -->α (expr_tm_abs x' (expr_subst x (type_var x')))
|
(expr_abs x τ e) -->α (expr_abs x' τ (expr_subst x (expr_var x') e))
|
||||||
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.
|
Example a1 : polymorphic_identity1 -->α polymorphic_identity2.
|
||||||
Proof.
|
Proof.
|
||||||
|
unfold polymorphic_identity1.
|
||||||
|
unfold polymorphic_identity2.
|
||||||
|
apply EAlpha_SubTyAbs.
|
||||||
|
apply EAlpha_Rename.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
Inductive beta_step : expr_term -> expr_term -> Prop :=
|
Inductive beta_step : expr_term -> expr_term -> Prop :=
|
||||||
| E_App1 : forall e1 e1' e2,
|
| E_App1 : forall e1 e1' e2,
|
||||||
e1 -->β e1' ->
|
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',
|
| E_App2 : forall e1 e2 e2',
|
||||||
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_TypApp : forall e e' τ,
|
||||||
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 y z ->
|
||||||
multi R x 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 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.
|
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_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_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_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_abs x t e => if (eqb v x) then e0 else expr_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_morph x t e => if (eqb v x) then e0 else expr_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_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_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_ascend t e => expr_ascend t (expr_subst v n e)
|
||||||
| expr_descend t e => expr_descend 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_var : string -> expr_term
|
||||||
| expr_ty_abs : string -> expr_term -> expr_term
|
| expr_ty_abs : string -> expr_term -> expr_term
|
||||||
| expr_ty_app : expr_term -> type_term -> expr_term
|
| expr_ty_app : expr_term -> type_term -> expr_term
|
||||||
| expr_tm_abs : string -> type_term -> expr_term -> expr_term
|
| expr_abs : string -> type_term -> expr_term -> expr_term
|
||||||
| expr_tm_abs_morph : string -> type_term -> expr_term -> expr_term
|
| expr_morph : string -> type_term -> expr_term -> expr_term
|
||||||
| expr_tm_app : expr_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_let : string -> type_term -> expr_term -> expr_term -> expr_term
|
||||||
| expr_ascend : type_term -> expr_term -> expr_term
|
| expr_ascend : type_term -> expr_term -> expr_term
|
||||||
| expr_descend : type_term -> expr_term -> expr_term
|
| expr_descend : type_term -> expr_term -> expr_term
|
||||||
|
@ -32,8 +32,8 @@ Inductive expr_term : Type :=
|
||||||
|
|
||||||
(* values *)
|
(* values *)
|
||||||
Inductive is_value : expr_term -> Prop :=
|
Inductive is_value : expr_term -> Prop :=
|
||||||
| V_ValAbs : forall x τ e,
|
| V_Abs : forall x τ e,
|
||||||
(is_value (expr_tm_abs x τ e))
|
(is_value (expr_abs x τ e))
|
||||||
|
|
||||||
| V_TypAbs : forall τ e,
|
| V_TypAbs : forall τ e,
|
||||||
(is_value (expr_ty_abs τ e))
|
(is_value (expr_ty_abs τ e))
|
||||||
|
@ -43,6 +43,8 @@ Inductive is_value : expr_term -> Prop :=
|
||||||
(is_value (expr_ascend τ e))
|
(is_value (expr_ascend τ e))
|
||||||
.
|
.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
Declare Scope ladder_type_scope.
|
Declare Scope ladder_type_scope.
|
||||||
Declare Scope ladder_expr_scope.
|
Declare Scope ladder_expr_scope.
|
||||||
Declare Custom Entry ladder_type.
|
Declare Custom Entry ladder_type.
|
||||||
|
@ -71,10 +73,14 @@ Notation "[[ e ]]" := e
|
||||||
(e custom ladder_expr at level 80) : ladder_expr_scope.
|
(e custom ladder_expr at level 80) : ladder_expr_scope.
|
||||||
Notation "'%' x '%'" := (expr_var x%string)
|
Notation "'%' x '%'" := (expr_var x%string)
|
||||||
(in custom ladder_expr at level 0, x constr) : ladder_expr_scope.
|
(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)
|
Notation "'Λ' t '↦' e" := (expr_ty_abs t e)
|
||||||
(in custom ladder_expr at level 0, t constr, e custom ladder_expr at level 80).
|
(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_type_scope.
|
||||||
Open Scope ladder_expr_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),
|
| T_Abs : forall (Γ:context) (x:string) (σ:type_term) (t:expr_term) (τ:type_term),
|
||||||
(context_contains Γ x σ) ->
|
(context_contains Γ x σ) ->
|
||||||
Γ |- t \is τ ->
|
Γ |- 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),
|
| T_App : forall (Γ:context) (f:expr_term) (a:expr_term) (σ:type_term) (τ:type_term),
|
||||||
Γ |- f \is (type_fun σ τ) ->
|
Γ |- f \is (type_fun σ τ) ->
|
||||||
Γ |- a \is σ ->
|
Γ |- a \is σ ->
|
||||||
Γ |- (expr_tm_app f a) \is τ
|
Γ |- (expr_app f a) \is τ
|
||||||
|
|
||||||
| T_Sub : forall Γ x τ τ',
|
| T_Sub : forall Γ x τ τ',
|
||||||
Γ |- x \is τ ->
|
Γ |- x \is τ ->
|
||||||
|
@ -88,17 +88,17 @@ Inductive expr_type_compatible : context -> expr_term -> type_term -> Prop :=
|
||||||
| T_CompatMorphAbs : forall Γ x t τ τ',
|
| T_CompatMorphAbs : forall Γ x t τ τ',
|
||||||
Γ |- t \compatible τ ->
|
Γ |- 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),
|
| T_CompatAbs : forall (Γ:context) (x:string) (σ:type_term) (t:expr_term) (τ:type_term),
|
||||||
(context_contains Γ x σ) ->
|
(context_contains Γ x σ) ->
|
||||||
Γ |- t \compatible τ ->
|
Γ |- t \compatible τ ->
|
||||||
Γ |- (expr_tm_abs x σ t) \compatible (type_fun σ τ)
|
Γ |- (expr_abs x σ t) \compatible (type_fun σ τ)
|
||||||
|
|
||||||
| T_CompatApp : forall Γ f a σ τ,
|
| T_CompatApp : forall Γ f a σ τ,
|
||||||
(Γ |- f \compatible (type_fun σ τ)) ->
|
(Γ |- f \compatible (type_fun σ τ)) ->
|
||||||
(Γ |- a \compatible σ) ->
|
(Γ |- a \compatible σ) ->
|
||||||
(Γ |- (expr_tm_app f a) \compatible τ)
|
(Γ |- (expr_app f a) \compatible τ)
|
||||||
|
|
||||||
| T_CompatImplicitCast : forall Γ h x τ τ',
|
| T_CompatImplicitCast : forall Γ h x τ τ',
|
||||||
(context_contains Γ h (type_morph τ τ')) ->
|
(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 τ).
|
where "Γ '|-' x '\compatible' τ" := (expr_type_compatible Γ x τ).
|
||||||
|
|
||||||
|
Definition is_well_typed (e:expr_term) : Prop :=
|
||||||
|
exists Γ τ,
|
||||||
|
Γ |- e \compatible τ
|
||||||
|
.
|
||||||
|
|
||||||
(* Examples *)
|
(* Examples *)
|
||||||
|
|
||||||
|
|
||||||
Example typing1 :
|
Example typing1 :
|
||||||
forall Γ,
|
forall Γ,
|
||||||
(context_contains Γ "x" [ %"T"% ]) ->
|
(context_contains Γ "x" [ %"T"% ]) ->
|
||||||
|
@ -134,7 +137,6 @@ Example typing2 :
|
||||||
forall Γ,
|
forall Γ,
|
||||||
(context_contains Γ "x" [ %"T"% ]) ->
|
(context_contains Γ "x" [ %"T"% ]) ->
|
||||||
Γ |- [[ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% ]] \is [ ∀"U", %"U"% -> %"U"% ].
|
Γ |- [[ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% ]] \is [ ∀"U", %"U"% -> %"U"% ].
|
||||||
(* Γ |- [ ΛT ↦ λx:T ↦ x ] : ∀T.(T->T) *)
|
|
||||||
Proof.
|
Proof.
|
||||||
intros.
|
intros.
|
||||||
apply T_Sub with (τ:=[∀"T",(%"T"% -> %"T"%)]).
|
apply T_Sub with (τ:=[∀"T",(%"T"% -> %"T"%)]).
|
||||||
|
@ -188,4 +190,23 @@ Proof.
|
||||||
apply TSubst_VarReplace.
|
apply TSubst_VarReplace.
|
||||||
Qed.
|
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.
|
End Typing.
|
||||||
|
|
|
@ -6,7 +6,7 @@
|
||||||
\usepackage{mathpartir}
|
\usepackage{mathpartir}
|
||||||
\usepackage{hyperref}
|
\usepackage{hyperref}
|
||||||
\usepackage{url}
|
\usepackage{url}
|
||||||
\usepackage{stmaryrd}
|
|
||||||
\usepackage{minted}
|
\usepackage{minted}
|
||||||
\usemintedstyle{tango}
|
\usemintedstyle{tango}
|
||||||
|
|
||||||
|
@ -52,25 +52,11 @@
|
||||||
|
|
||||||
|
|
||||||
\begin{abstract}
|
\begin{abstract}
|
||||||
This work explores the idea of \emph{representational polymorphism}
|
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}.
|
||||||
to treat the coexistence of multiple equivalent representational forms for a single abstract concept.
|
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}.
|
||||||
interchangeability
|
Further we show how the Boehm-Berarducci encoding can be used to implement algebraic datatypes on the basis of the introduced core calculus.
|
||||||
%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}
|
\end{abstract}
|
||||||
|
|
||||||
\maketitle
|
\maketitle
|
||||||
|
@ -78,29 +64,6 @@ and prove its \emph{soundness}.
|
||||||
|
|
||||||
|
|
||||||
%\newpage
|
%\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}
|
\section{Core Calculus}
|
||||||
\subsection{Syntax}
|
\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]
|
\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 \}\),
|
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}\)
|
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})\)
|
in an expression \(e \in \nonterm{E} \) with the \(\psi_e(\metavariable{x_i})\)
|
||||||
|
|
Loading…
Reference in a new issue