Compare commits
1 commit
4323e7d09f
...
b0035e711a
Author | SHA1 | Date | |
---|---|---|---|
b0035e711a |
8 changed files with 90 additions and 104 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,5 +1,4 @@
|
||||||
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.
|
||||||
|
@ -8,37 +7,35 @@ 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_abs "s" (type_fun (type_var "α") (type_var "α"))
|
(expr_tm_abs "s" (type_fun (type_var "α") (type_var "α"))
|
||||||
(expr_abs "z" (type_var "α")
|
(expr_tm_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_abs "s" (type_fun (type_var "α") (type_var "α"))
|
(expr_tm_abs "s" (type_fun (type_var "α") (type_var "α"))
|
||||||
(expr_abs "z" (type_var "α")
|
(expr_tm_abs "z" (type_var "α")
|
||||||
(expr_app (expr_var "s") (expr_var "z"))))).
|
(expr_tm_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_abs "s" (type_fun (type_var "α") (type_var "α"))
|
(expr_tm_abs "s" (type_fun (type_var "α") (type_var "α"))
|
||||||
(expr_abs "z" (type_var "α")
|
(expr_tm_abs "z" (type_var "α")
|
||||||
(expr_app (expr_var "s") (expr_app (expr_var "s") (expr_var "z")))))).
|
(expr_tm_app (expr_var "s") (expr_tm_app (expr_var "s") (expr_var "z")))))).
|
||||||
|
|
||||||
|
|
||||||
Definition bb_succ : expr_term :=
|
Definition bb_succ : expr_term :=
|
||||||
(expr_abs "n" (type_ladder (type_id "ℕ")
|
(expr_tm_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 "α"))
|
||||||
|
@ -46,10 +43,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_abs "s" (type_fun (type_var "α") (type_var "α"))
|
(expr_tm_abs "s" (type_fun (type_var "α") (type_var "α"))
|
||||||
(expr_abs "z" (type_var "α")
|
(expr_tm_abs "z" (type_var "α")
|
||||||
(expr_app (expr_var "s")
|
(expr_tm_app (expr_var "s")
|
||||||
(expr_app (expr_app
|
(expr_tm_app (expr_tm_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")))))))).
|
||||||
|
@ -61,25 +58,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_app (expr_app (expr_var "+") (expr_var "bb-zero")) (expr_var "bb-zero"))
|
(expr_tm_app (expr_tm_app (expr_var "+") (expr_var "bb-zero")) (expr_var "bb-zero"))
|
||||||
).
|
).
|
||||||
|
|
||||||
Definition t1 : expr_term := (expr_app (expr_var "x") (expr_var "x")).
|
Definition t1 : expr_term := (expr_tm_app (expr_var "x") (expr_var "x")).
|
||||||
|
|
||||||
Compute (expr_subst "x"
|
Compute (expr_subst "x"
|
||||||
(expr_ty_abs "α" (expr_abs "a" (type_var "α") (expr_var "a")))
|
(expr_ty_abs "α" (expr_tm_abs "a" (type_var "α") (expr_var "a")))
|
||||||
bb_one
|
bb_one
|
||||||
).
|
).
|
||||||
|
|
||||||
Example example_let_reduction :
|
Example example_let_reduction :
|
||||||
e1 -->β (expr_app (expr_app (expr_var "+") bb_zero) bb_zero).
|
e1 -->β (expr_tm_app (expr_tm_app (expr_var "+") bb_zero) bb_zero).
|
||||||
Proof.
|
Proof.
|
||||||
apply E_AppLet.
|
apply E_AppLet.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
Compute (expr_app bb_succ bb_zero) -->β bb_one.
|
Compute (expr_tm_app bb_succ bb_zero) -->β bb_one.
|
||||||
|
|
||||||
Example example_succ :
|
Example example_succ :
|
||||||
(expr_app bb_succ bb_zero) -->β bb_one.
|
(expr_tm_app bb_succ bb_zero) -->β bb_one.
|
||||||
Proof.
|
Proof.
|
||||||
Admitted.
|
Admitted.
|
||||||
|
|
|
@ -11,50 +11,28 @@ 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 expr_alpha : expr_term -> expr_term -> Prop :=
|
Inductive alpha_step : expr_term -> expr_term -> Prop :=
|
||||||
| EAlpha_Rename : forall x x' τ e,
|
| E_Rename : forall x x' e,
|
||||||
(expr_abs x τ e) -->α (expr_abs x' τ (expr_subst x (expr_var x') e))
|
(expr_tm_abs x e) -->α (expr_tm_abs x' (expr_subst x (type_var x')))
|
||||||
|
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_app e1 e2) -->β (expr_app e1' e2)
|
(expr_tm_app e1 e2) -->β (expr_tm_app e1' e2)
|
||||||
|
|
||||||
| E_App2 : forall e1 e2 e2',
|
| E_App2 : forall e1 e2 e2',
|
||||||
e2 -->β e2' ->
|
e2 -->β e2' ->
|
||||||
(expr_app e1 e2) -->β (expr_app e1 e2')
|
(expr_tm_app e1 e2) -->β (expr_tm_app e1 e2')
|
||||||
|
|
||||||
| E_TypApp : forall e e' τ,
|
| E_TypApp : forall e e' τ,
|
||||||
e -->β e' ->
|
e -->β e' ->
|
||||||
|
@ -103,7 +81,8 @@ 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
coq/soundness.v
Normal file
1
coq/soundness.v
Normal file
|
@ -0,0 +1 @@
|
||||||
|
|
|
@ -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_abs x t e => if (eqb v x) then e0 else expr_abs x t (expr_subst v n e)
|
| expr_tm_abs x t e => if (eqb v x) then e0 else expr_tm_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_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_app e a => expr_app (expr_subst v n e) (expr_subst v n a)
|
| expr_tm_app e a => expr_tm_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_abs : string -> type_term -> expr_term -> expr_term
|
| expr_tm_abs : string -> type_term -> expr_term -> expr_term
|
||||||
| expr_morph : string -> type_term -> expr_term -> expr_term
|
| expr_tm_abs_morph : string -> type_term -> expr_term -> expr_term
|
||||||
| expr_app : expr_term -> expr_term -> expr_term
|
| expr_tm_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_Abs : forall x τ e,
|
| V_ValAbs : forall x τ e,
|
||||||
(is_value (expr_abs x τ e))
|
(is_value (expr_tm_abs x τ e))
|
||||||
|
|
||||||
| V_TypAbs : forall τ e,
|
| V_TypAbs : forall τ e,
|
||||||
(is_value (expr_ty_abs τ e))
|
(is_value (expr_ty_abs τ e))
|
||||||
|
@ -43,8 +43,6 @@ 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.
|
||||||
|
@ -73,14 +71,10 @@ 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_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_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)
|
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_abs x σ t) \is (type_fun σ τ)
|
Γ |- (expr_tm_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_app f a) \is τ
|
Γ |- (expr_tm_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_morph x τ t) \compatible (type_morph τ τ')
|
Γ |- (expr_tm_abs_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_abs x σ t) \compatible (type_fun σ τ)
|
Γ |- (expr_tm_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_app f a) \compatible τ)
|
(Γ |- (expr_tm_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,13 +112,10 @@ 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"% ]) ->
|
||||||
|
@ -137,6 +134,7 @@ 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"%)]).
|
||||||
|
@ -190,23 +188,4 @@ 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,11 +52,25 @@
|
||||||
|
|
||||||
|
|
||||||
\begin{abstract}
|
\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}.
|
This work explores the idea of \emph{representational polymorphism}
|
||||||
Using ladder-types, multi-layered embeddings of higher-level data-types into lower-level data-types can be described by a type-level structure.
|
to treat the coexistence of multiple equivalent representational forms for a single abstract concept.
|
||||||
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.
|
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}
|
\end{abstract}
|
||||||
|
|
||||||
\maketitle
|
\maketitle
|
||||||
|
@ -64,6 +78,29 @@ Further we show how the Boehm-Berarducci encoding can be used to implement algeb
|
||||||
|
|
||||||
|
|
||||||
%\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}
|
||||||
|
|
||||||
|
@ -301,7 +338,6 @@ 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