Compare commits

..

9 commits

9 changed files with 327 additions and 218 deletions

View file

@ -3,8 +3,9 @@ terms.v
equiv.v equiv.v
subst.v subst.v
subtype.v subtype.v
typing.v context.v
morph.v morph.v
typing.v
smallstep.v smallstep.v
soundness.v soundness.v
bbencode.v bbencode.v

View file

@ -55,12 +55,7 @@ Definition bb_succ : expr_term :=
(expr_var "z")))))))). (expr_var "z")))))))).
Definition e1 : expr_term := Definition e1 : expr_term :=
(expr_let "bb-zero" (type_ladder (type_id "") (expr_let "bb-zero" bb_zero
(type_ladder (type_id "BBNat")
(type_univ "α"
(type_fun (type_fun (type_var "α") (type_var "α"))
(type_fun (type_var "α") (type_var "α"))))))
bb_zero
(expr_app (expr_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"))
). ).

21
coq/context.v Normal file
View file

@ -0,0 +1,21 @@
From Coq Require Import Strings.String.
Require Import terms.
Include Terms.
Module Context.
Inductive context : Type :=
| ctx_assign : string -> type_term -> context -> context
| ctx_empty : context
.
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 Γ,
(context_contains Γ x X) ->
(context_contains (ctx_assign y Y Γ) x X).
End Context.

View file

@ -3,66 +3,100 @@ Require Import terms.
Require Import subst. Require Import subst.
Require Import equiv. Require Import equiv.
Require Import subtype. Require Import subtype.
Require Import typing. Require Import context.
Include Terms. Include Terms.
Include Subst. Include Subst.
Include Equiv. Include Equiv.
Include Subtype. Include Subtype.
Include Typing. Include Context.
Module Morph. Module Morph.
(* Given a context, there is a morphism path from τ to τ' *)
Reserved Notation "Γ '|-' σ '~>' τ" (at level 101, σ at next level, τ at next level).
Reserved Notation "Γ '|-' '[[' e ']]' '=' t" (at level 101, e at next level, t at level 0). Inductive morphism_path : context -> type_term -> type_term -> Prop :=
| M_Sub : forall Γ τ τ',
(τ :<= τ') ->
(Γ |- τ ~> τ')
Inductive expand_morphisms : context -> expr_term -> expr_term -> Prop := | M_Single : forall Γ h τ τ',
| Expand_Transform : forall Γ e h τ τ',
(context_contains Γ h (type_morph τ τ')) -> (context_contains Γ h (type_morph τ τ')) ->
(Γ |- e \is τ) -> (Γ |- τ ~> τ')
(Γ |- [[ e ]] = (expr_app (expr_var h) e))
| Expand_Otherwise : forall Γ e, | M_Chain : forall Γ τ τ' τ'',
(Γ |- [[ e ]] = e) (Γ |- τ ~> τ') ->
(Γ |- τ' ~> τ'') ->
(Γ |- τ ~> τ'')
| Expand_App : forall Γ f f' a a' σ τ, | M_Lift : forall Γ σ τ τ',
(Γ |- f \compatible (type_fun σ τ)) -> (Γ |- τ ~> τ') ->
(Γ |- a \compatible σ) -> (Γ |- (type_ladder σ τ) ~> (type_ladder σ τ'))
(Γ |- [[ f ]] = f') ->
(Γ |- [[ a ]] = a') ->
(Γ |- [[ (expr_app f a) ]] = (expr_app f a'))
where "Γ '|-' '[[' e ']]' '=' t" := (expand_morphisms Γ e t). | M_MapSeq : forall Γ τ τ',
(Γ |- τ ~> τ') ->
(Γ |- (type_spec (type_id "Seq") τ) ~> (type_spec (type_id "Seq") τ'))
where "Γ '|-' s '~>' t" := (morphism_path Γ s t).
(* For every well-typed term, there is an expanded exactly typed term *) Inductive translate_morphism_path : context -> type_term -> type_term -> expr_term -> Prop :=
Lemma well_typed_is_expandable : | Translate_Subtype : forall Γ τ τ',
forall (e:expr_term), (τ :<= τ') ->
(is_well_typed e) -> (translate_morphism_path Γ τ τ'
exists Γ e', (expand_morphisms Γ e e') -> (is_exactly_typed e') (expr_morph "x" τ (expr_var "x")))
| Translate_Lift : forall Γ σ τ τ' m,
(Γ |- τ ~> τ') ->
(translate_morphism_path Γ τ τ' m) ->
(translate_morphism_path Γ (type_ladder σ τ) (type_ladder σ τ')
(expr_morph "x" (type_ladder σ τ)
(expr_ascend (type_ladder σ τ') (expr_app m (expr_descend τ (expr_var "x"))))))
| Translate_Single : forall Γ h τ τ',
(context_contains Γ h (type_morph τ τ')) ->
(translate_morphism_path Γ τ τ' (expr_var h))
| Translate_Chain : forall Γ τ τ' τ'' m1 m2,
(translate_morphism_path Γ τ τ' m1) ->
(translate_morphism_path Γ τ' τ'' m2) ->
(translate_morphism_path Γ τ τ''
(expr_morph "x" τ (expr_app m2 (expr_app m1 (expr_var "x")))))
| Translate_MapSeq : forall Γ τ τ' m,
(translate_morphism_path Γ τ τ' m) ->
(translate_morphism_path Γ
(type_spec (type_id "Seq") τ)
(type_spec (type_id "Seq") τ')
(expr_morph "xs"
(type_spec (type_id "Seq") τ)
(expr_app (expr_app (expr_ty_app (expr_ty_app
(expr_var "map") τ) τ') m)
(expr_var "xs"))))
.
Example morphism_paths :
(ctx_assign "degrees-to-turns" [< $"Angle"$~$"Degrees"$~$""$ ->morph $"Angle"$~$"Turns"$~$""$ >]
(ctx_assign "turns-to-radians" [< $"Angle"$~$"Turns"$~$""$ ->morph $"Angle"$~$"Radians"$~$""$ >]
ctx_empty))
|- [< <$"Seq"$ $"Hue"$~$"Angle"$~$"Degrees"$~$""$> >]
~> [< <$"Seq"$ $"Hue"$~$"Angle"$~$"Radians"$~$""$> >]
. .
Proof. Proof.
Admitted. intros.
apply M_MapSeq.
apply M_Lift.
apply M_Chain with (τ':=[<$"Angle"$~$"Turns"$~$""$>]).
apply M_Single with (h:="degrees-to-turns"%string).
apply C_take.
apply M_Single with (h:="turns-to-radians"%string).
apply C_shuffle.
apply C_take.
Qed.
Example expand1 :
(ctx_assign "morph-radix"
[< <%"PosInt"% %"16"%> ->morph <%"PosInt"% %"10"%> >]
(ctx_assign "fn-decimal"
[< <%"PosInt"% %"10"%> -> <%"PosInt"% %"10"%> >]
(ctx_assign "x"
[< <%"PosInt"% %"16"%> >]
ctx_empty)))
|- [[ (expr_app (expr_var "fn-decimal") (expr_var "x")) ]]
= (expr_app (expr_var "fn-decimal")
(expr_app (expr_var "morph-radix") (expr_var "x")))
.
Proof.
apply Expand_App with (f':=(expr_var "fn-decimal")) (σ:=[< < %"PosInt"% %"10"% > >]) (τ:=[< < %"PosInt"% %"10"% > >]).
apply TCompat_Native.
Admitted.
End Morph. End Morph.

View file

@ -22,15 +22,6 @@ Definition is_stuck (e:expr_term) : Prop :=
~(exists e', e -->β e') ~(exists e', e -->β e')
. .
(* every exactly typed term is not stuck *)
Lemma exact_progress :
forall (e:expr_term),
(is_exactly_typed e) -> ~(is_stuck e)
.
Proof.
Admitted.
(* every well typed term is not stuck *) (* every well typed term is not stuck *)
Lemma progress : Lemma progress :
forall (e:expr_term), forall (e:expr_term),
@ -40,32 +31,14 @@ Proof.
Admitted. Admitted.
(* reduction step preserves the type *) (* reduction step preserves well-typedness *)
Lemma exact_preservation : Lemma preservation :
forall Γ e e' τ, forall Γ e e' τ,
(Γ |- e \is τ) -> (Γ |- e \is τ) ->
(e -->β e') -> (e -->β e') ->
(Γ |- e' \is τ) (Γ |- e' \is τ)
. .
Proof. Proof.
(*
intros.
generalize dependent e'.
induction H.
intros e' I.
inversion I.
*)
Admitted.
(* reduction step preserves well-typedness *)
Lemma preservation :
forall Γ e e' τ,
(Γ |- e \compatible τ) ->
(e -->β e') ->
(Γ |- e' \compatible τ)
.
Proof.
Admitted. Admitted.
(* every well-typed expression can be reduced to a value *) (* every well-typed expression can be reduced to a value *)

View file

@ -115,7 +115,7 @@ Fixpoint expr_subst (v:string) (n:expr_term) (e0:expr_term) :=
| expr_abs x t e => if (eqb v x) then e0 else expr_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_morph x t e => if (eqb v x) then e0 else expr_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_app e a => expr_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 a e => expr_let x (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)
end. end.

View file

@ -25,12 +25,11 @@ Inductive expr_term : Type :=
| expr_abs : string -> type_term -> expr_term -> expr_term | expr_abs : string -> type_term -> expr_term -> expr_term
| expr_morph : 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_app : expr_term -> expr_term -> expr_term
| expr_let : string -> type_term -> expr_term -> expr_term -> expr_term | expr_let : string -> 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
. .
(* TODO (* TODO
Inductive type_DeBruijn : Type := Inductive type_DeBruijn : Type :=
@ -99,11 +98,20 @@ 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 "'Λ' 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 10, t constr, e custom ladder_expr at level 80) : ladder_expr_scope.
Notation "'λ' x τ '↦' e" := (expr_abs x τ e)
(in custom ladder_expr at level 10, x constr, τ custom ladder_type at level 99, e custom ladder_expr at level 99) :ladder_expr_scope.
Notation "'λ' x τ '↦morph' e" := (expr_morph x τ e)
(in custom ladder_expr at level 10, x constr, τ custom ladder_type at level 99, e custom ladder_expr at level 99) :ladder_expr_scope.
Notation "'let' x ':=' e 'in' t" := (expr_let x e t)
(in custom ladder_expr at level 20, x constr, e custom ladder_expr at level 99, t custom ladder_expr at level 99) : ladder_expr_scope.
Notation "e 'as' τ" := (expr_ascend τ e)
(in custom ladder_expr at level 30, e custom ladder_expr, τ custom ladder_type at level 99) : ladder_expr_scope.
Notation "e1 e2" := (expr_app e1 e2)
(in custom ladder_expr at level 50) : ladder_expr_scope.
Notation "'(' e ')'" := e
(in custom ladder_expr at level 0) : ladder_expr_scope.
(* EXAMPLES *) (* EXAMPLES *)
@ -112,7 +120,7 @@ Open Scope ladder_expr_scope.
Check [< "α", (< $"Seq"$ %"α"% > ~ < $"List"$ %"α"% >) >]. Check [< "α", (< $"Seq"$ %"α"% > ~ < $"List"$ %"α"% >) >].
Definition polymorphic_identity1 : expr_term := [{ Λ"T" λ"x"%"T"% %"x"% }]. Definition polymorphic_identity1 : expr_term := [{ Λ"T" λ"x"%"T"% (%"x"%) }].
Definition polymorphic_identity2 : expr_term := [{ Λ"T" λ"y"%"T"% %"y"% }]. Definition polymorphic_identity2 : expr_term := [{ Λ"T" λ"y"%"T"% %"y"% }].
Compute polymorphic_identity1. Compute polymorphic_identity1.

View file

@ -6,64 +6,55 @@ Require Import terms.
Require Import subst. Require Import subst.
Require Import equiv. Require Import equiv.
Require Import subtype. Require Import subtype.
Require Import context.
Require Import morph.
Include Terms. Include Terms.
Include Subst. Include Subst.
Include Equiv. Include Equiv.
Include Subtype. Include Subtype.
Include Context.
Include Morph.
Module Typing. Module Typing.
(** Typing Derivation *) (** Typing Derivation *)
Inductive context : Type :=
| ctx_assign : string -> type_term -> context -> context
| ctx_empty : context
.
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 Γ,
(context_contains Γ x X) ->
(context_contains (ctx_assign y Y Γ) x X).
Reserved Notation "Gamma '|-' x '\is' X" (at level 101, x at next level, X at level 0). Reserved Notation "Gamma '|-' x '\is' X" (at level 101, x at next level, X at level 0).
Reserved Notation "Gamma '|-' x '\compatible' X" (at level 101, x at next level, X at level 0).
Inductive expr_type : context -> expr_term -> type_term -> Prop := Inductive expr_type : context -> expr_term -> type_term -> Prop :=
| T_Var : forall Γ x τ, | T_Var : forall Γ x τ,
(context_contains Γ x τ) -> (context_contains Γ x τ) ->
(Γ |- (expr_var x) \is τ) (Γ |- (expr_var x) \is τ)
| T_Let : forall Γ s (σ:type_term) t τ x, | T_Let : forall Γ s σ t τ x,
(Γ |- s \is σ) -> (Γ |- s \is σ) ->
(Γ |- t \is τ) -> ((ctx_assign x σ Γ) |- t \is τ) ->
(Γ |- (expr_let x σ s t) \is τ) (Γ |- (expr_let x s t) \is τ)
| T_TypeAbs : forall Γ (e:expr_term) (τ:type_term) α, | T_TypeAbs : forall Γ e τ α,
Γ |- e \is τ -> Γ |- e \is τ ->
Γ |- (expr_ty_abs α e) \is (type_univ α τ) Γ |- (expr_ty_abs α e) \is (type_univ α τ)
| T_TypeApp : forall Γ α (e:expr_term) (σ:type_term) (τ:type_term), | T_TypeApp : forall Γ α e σ τ τ',
Γ |- e \is (type_univ α τ) -> Γ |- e \is (type_univ α τ) ->
Γ |- (expr_ty_app e σ) \is (type_subst α σ τ) (type_subst1 α σ τ τ') ->
Γ |- (expr_ty_app e σ) \is τ'
| T_Abs : forall (Γ:context) (x:string) (σ:type_term) (t:expr_term) (τ:type_term), | T_Abs : forall Γ x σ t τ,
(context_contains Γ x σ) -> ((ctx_assign x σ Γ) |- t \is τ) ->
Γ |- t \is τ -> (Γ |- (expr_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_app f a) \is τ
| T_MorphAbs : forall Γ x σ e τ, | T_MorphAbs : forall Γ x σ e τ,
(context_contains Γ x σ) -> ((ctx_assign x σ Γ) |- e \is τ) ->
Γ |- e \is τ ->
Γ |- (expr_morph x σ e) \is (type_morph σ τ) Γ |- (expr_morph x σ e) \is (type_morph σ τ)
| T_App : forall Γ f a σ' σ τ,
(Γ |- f \is (type_fun σ τ)) ->
(Γ |- a \is σ') ->
(Γ |- σ' ~> σ) ->
(Γ |- (expr_app f a) \is τ)
| T_MorphFun : forall Γ f σ τ, | T_MorphFun : forall Γ f σ τ,
Γ |- f \is (type_morph σ τ) -> Γ |- f \is (type_morph σ τ) ->
Γ |- f \is (type_fun σ τ) Γ |- f \is (type_fun σ τ)
@ -73,84 +64,111 @@ Inductive expr_type : context -> expr_term -> type_term -> Prop :=
(τ' :<= τ) -> (τ' :<= τ) ->
(Γ |- (expr_ascend τ' e) \is τ') (Γ |- (expr_ascend τ' e) \is τ')
| T_Descend : forall Γ x τ τ', | T_DescendImplicit : forall Γ x τ τ',
Γ |- x \is τ -> Γ |- x \is τ ->
(τ :<= τ') -> (τ :<= τ') ->
Γ |- x \is τ' Γ |- x \is τ'
| T_Descend : forall Γ x τ τ',
Γ |- x \is τ ->
(τ :<= τ') ->
Γ |- (expr_descend τ' x) \is τ'
where "Γ '|-' x '\is' τ" := (expr_type Γ x τ). where "Γ '|-' x '\is' τ" := (expr_type Γ x τ).
Inductive expr_type_compatible : context -> expr_term -> type_term -> Prop :=
| TCompat_Native : forall Γ e τ,
(Γ |- e \is τ) ->
(Γ |- e \compatible τ)
| TCompat_Let : forall Γ s (σ:type_term) t τ x,
(Γ |- s \is σ) ->
(context_contains Γ x σ) ->
(Γ |- t \compatible τ) ->
(Γ |- (expr_let x σ s t) \compatible τ)
| T_CompatTypeApp : forall Γ α (e:expr_term) (σ:type_term) (τ:type_term),
Γ |- e \compatible (type_univ α τ) ->
Γ |- (expr_ty_app e σ) \compatible (type_subst α σ τ)
| TCompat_App : forall Γ f a σ τ,
(Γ |- f \compatible (type_fun σ τ)) ->
(Γ |- a \compatible σ) ->
(Γ |- (expr_app f a) \compatible τ)
| TCompat_Morph : forall Γ h x τ τ',
(context_contains Γ h (type_morph τ τ')) ->
(Γ |- x \compatible τ) ->
(Γ |- x \compatible τ')
| TCompat_Sub : forall Γ x τ τ',
(Γ |- x \compatible τ) ->
(τ ~<= τ') ->
(Γ |- x \compatible τ')
where "Γ '|-' x '\compatible' τ" := (expr_type_compatible Γ x τ).
Definition is_well_typed (e:expr_term) : Prop := Definition is_well_typed (e:expr_term) : Prop :=
exists Γ τ, exists Γ τ,
Γ |- e \compatible τ Γ |- e \is τ
. .
Definition is_exactly_typed (e:expr_term) : Prop := Inductive translate_typing : context -> expr_term -> type_term -> expr_term -> Prop :=
exists Γ τ, | Expand_Var : forall Γ x τ,
Γ |- e \is τ (Γ |- (expr_var x) \is τ) ->
(translate_typing Γ (expr_var x) τ (expr_var x))
| Expand_Let : forall Γ x e e' t t' σ τ,
(Γ |- e \is σ) ->
((ctx_assign x σ Γ) |- t \is τ) ->
(translate_typing Γ e σ e') ->
(translate_typing (ctx_assign x σ Γ) t τ t') ->
(translate_typing Γ (expr_let x e t) τ (expr_let x e' t'))
| Expand_TypeAbs : forall Γ α e e' τ,
(Γ |- e \is τ) ->
(translate_typing Γ e τ e') ->
(translate_typing Γ
(expr_ty_abs α e)
(type_univ α τ)
(expr_ty_abs α e'))
| Expand_TypeApp : forall Γ e e' σ α τ,
(Γ |- e \is (type_univ α τ)) ->
(translate_typing Γ e τ e') ->
(translate_typing Γ (expr_ty_app e τ) (type_subst α σ τ) (expr_ty_app e' τ))
| Expand_Abs : forall Γ x σ e e' τ,
((ctx_assign x σ Γ) |- e \is τ) ->
(Γ |- (expr_abs x σ e) \is (type_fun σ τ)) ->
(translate_typing (ctx_assign x σ Γ) e τ e') ->
(translate_typing Γ (expr_abs x σ e) (type_fun σ τ) (expr_abs x σ e'))
| Expand_MorphAbs : forall Γ x σ e e' τ,
((ctx_assign x σ Γ) |- e \is τ) ->
(Γ |- (expr_abs x σ e) \is (type_fun σ τ)) ->
(translate_typing (ctx_assign x σ Γ) e τ e') ->
(translate_typing Γ (expr_morph x σ e) (type_morph σ τ) (expr_morph x σ e'))
| Expand_App : forall Γ f f' a a' m σ τ σ',
(Γ |- f \is (type_fun σ τ)) ->
(Γ |- a \is σ') ->
(Γ |- σ' ~> σ) ->
(translate_typing Γ f (type_fun σ τ) f') ->
(translate_typing Γ a σ' a') ->
(translate_morphism_path Γ σ' σ m) ->
(translate_typing Γ (expr_app f a) τ (expr_app f' (expr_app m a')))
| Expand_MorphFun : forall Γ f f' σ τ,
(Γ |- f \is (type_morph σ τ)) ->
(Γ |- f \is (type_fun σ τ)) ->
(translate_typing Γ f (type_morph σ τ) f') ->
(translate_typing Γ f (type_fun σ τ) f')
| Expand_Ascend : forall Γ e e' τ τ',
(Γ |- e \is τ) ->
(τ' :<= τ) ->
(Γ |- (expr_ascend τ' e) \is τ') ->
(translate_typing Γ e τ e') ->
(translate_typing Γ (expr_ascend τ' e) τ' (expr_ascend τ' e'))
| Expand_Descend : forall Γ e e' τ τ',
(Γ |- e \is τ) ->
(τ :<= τ') ->
(Γ |- e \is τ') ->
(translate_typing Γ e τ e') ->
(translate_typing Γ e τ' e')
. .
(* Examples *) (* Examples *)
Example typing1 : Example typing1 :
forall Γ, ctx_empty |- [{ Λ"T" λ "x" %"T"% %"x"% }] \is [< "T", %"T"% -> %"T"% >].
(context_contains Γ "x" [< %"T"% >]) ->
Γ |- [{ Λ"T" λ "x" %"T"% %"x"% }] \is [< "T", %"T"% -> %"T"% >].
(* Γ |- [ ΛT ↦ λx:T ↦ x ] : ∀T.(T->T) *)
Proof. Proof.
intros. intros.
apply T_TypeAbs. apply T_TypeAbs.
apply T_Abs. apply T_Abs.
apply H.
apply T_Var. apply T_Var.
apply H. apply C_take.
Qed. Qed.
Example typing2 : Example typing2 :
forall Γ, ctx_empty |- [{ Λ"T" λ "x" %"T"% %"x"% }] \is [< "U", %"U"% -> %"U"% >].
(context_contains Γ "x" [< %"T"% >]) ->
Γ |- [{ Λ"T" λ "x" %"T"% %"x"% }] \is [< "U", %"U"% -> %"U"% >].
Proof. Proof.
intros. intros.
apply T_Descend with (τ:=[< "T",(%"T"% -> %"T"%) >]). apply T_DescendImplicit with (τ:=[< "T",(%"T"% -> %"T"%) >]).
apply T_TypeAbs. apply T_TypeAbs.
apply T_Abs. apply T_Abs.
apply H.
apply T_Var. apply T_Var.
apply H. apply C_take.
apply TSubRepr_Refl. apply TSubRepr_Refl.
apply TEq_Alpha. apply TEq_Alpha.
@ -161,22 +179,18 @@ Proof.
Qed. Qed.
Example typing3 : Example typing3 :
forall Γ, ctx_empty |- [{
(context_contains Γ "x" [< %"T"% >]) ->
(context_contains Γ "y" [< %"U"% >]) ->
Γ |- [{
Λ"T" Λ"U" λ"x" %"T"% λ"y" %"U"% %"y"% Λ"T" Λ"U" λ"x" %"T"% λ"y" %"U"% %"y"%
}] \is [< }] \is [<
"S","T",(%"S"%->%"T"%->%"T"%) "S","T",(%"S"%->%"T"%->%"T"%)
>]. >].
Proof. Proof.
intros. intros.
apply T_Descend with (τ:=[< "T","U",(%"T"%->%"U"%->%"U"%) >]) (τ':=[< "S","T",(%"S"%->%"T"%->%"T"%) >]). apply T_DescendImplicit with (τ:=[< "T","U",(%"T"%->%"U"%->%"U"%) >]) (τ':=[< "S","T",(%"S"%->%"T"%->%"T"%) >]).
apply T_TypeAbs, T_TypeAbs, T_Abs. apply T_TypeAbs, T_TypeAbs, T_Abs.
apply H.
apply T_Abs. apply T_Abs.
apply H0. apply T_Var.
apply T_Var, H0. apply C_take.
apply TSubRepr_Refl. apply TSubRepr_Refl.
apply TEq_Trans with (y:= [< "S","U",(%"S"%->%"U"%->%"U"%) >] ). apply TEq_Trans with (y:= [< "S","U",(%"S"%->%"U"%->%"U"%) >] ).
@ -200,24 +214,70 @@ Proof.
apply TSubst_VarReplace. apply TSubst_VarReplace.
Qed. Qed.
Example typing4 : (is_well_typed Example typing4 : (is_well_typed
[{ Λ"T" Λ"U" λ"x" %"T"% λ"y" %"U"% %"x"% }] [{ Λ"T" Λ"U" λ"x" %"T"% λ"y" %"U"% %"x"% }]
). ).
Proof. Proof.
unfold is_well_typed. unfold is_well_typed.
exists (ctx_assign "x" [< %"T"% >] exists ctx_empty.
(ctx_assign "y" [< %"U"% >] ctx_empty)).
exists [< "T","U",%"T"%->%"U"%->%"T"% >]. exists [< "T","U",%"T"%->%"U"%->%"T"% >].
apply TCompat_Native.
apply T_TypeAbs. apply T_TypeAbs.
apply T_TypeAbs. apply T_TypeAbs.
apply T_Abs. apply T_Abs.
apply C_take.
apply T_Abs. apply T_Abs.
apply C_shuffle. apply C_take. apply T_Var.
apply C_shuffle, C_take.
Qed.
Open Scope ladder_expr_scope.
Example typing5 : (is_well_typed
[{
let "deg2turns" :=
(λ"x" $"Angle"$~$"Degrees"$~$""$
morph (((%"/"% %"x"%) %"360"%) as $"Angle"$~$"Turns"$~$""$))
in ( %"deg2turns"% (%"60"% as $"Angle"$~$"Degrees"$~$""$) )
}]
).
Proof.
unfold is_well_typed.
exists (ctx_assign "60" [< $""$ >]
(ctx_assign "360" [< $""$ >]
(ctx_assign "/" [< $""$ -> $""$ -> $""$ >]
ctx_empty))).
exists [< $"Angle"$~$"Turns"$~$""$ >].
apply T_Let with (σ:=[< $"Angle"$~$"Degrees"$~$""$ ->morph $"Angle"$~$"Turns"$~$""$ >]).
apply T_MorphAbs.
apply T_Ascend with (τ:=[< $""$ >]).
apply T_App with (σ := [< $""$ >]) (σ' := [< $""$ >]).
apply T_App with (σ := [< $""$ >]) (σ' := [< $""$ >]).
apply T_Var.
apply C_shuffle. apply C_shuffle. apply C_shuffle. apply C_take.
apply T_DescendImplicit with (τ := [< $"Angle"$~$"Degrees"$~$""$ >]).
apply T_Var. apply T_Var.
apply C_take. apply C_take.
apply TSubRepr_Ladder. apply TSubRepr_Ladder.
apply TSubRepr_Refl. apply TEq_Refl.
apply M_Sub.
apply TSubRepr_Refl. apply TEq_Refl.
apply T_Var.
apply C_shuffle, C_shuffle, C_take.
apply M_Sub.
apply TSubRepr_Refl.
apply TEq_Refl.
apply TSubRepr_Ladder, TSubRepr_Ladder, TSubRepr_Refl.
apply TEq_Refl.
apply T_App with (σ:=[<$"Angle"$~$"Degrees"$~$""$>]) (σ':=[<$"Angle"$~$"Degrees"$~$""$>]).
apply T_MorphFun.
apply T_Var.
apply C_take.
apply T_Ascend with (τ:=[<$""$>]).
apply T_Var.
apply C_shuffle. apply C_take.
apply TSubRepr_Ladder.
apply TSubRepr_Ladder.
apply TSubRepr_Refl. apply TEq_Refl.
apply M_Sub. apply TSubRepr_Refl. apply TEq_Refl.
Qed. Qed.
End Typing. End Typing.

View file

@ -518,17 +518,23 @@ while preserving its semantics.
\end{enumerate} \end{enumerate}
\end{example} \end{example}
\subsubsection{Inference of Expression Types} \subsubsection{Typing Context}
As usual, the typing-context \(\Gamma = \{ \metavariable{x_1} : \metavariable{\tau_1} , \quad \metavariable{x_2} : \metavariable{\tau_2} , \quad \ldots \}\) As usual, the typing-context \(\Gamma = \{ \metavariable{x_1} : \metavariable{\tau_1} , \quad \metavariable{x_2} : \metavariable{\tau_2} , \quad \ldots \}\)
is a finite mapping which assigns variables \(\metavariable{x_i} \in \exprvars\) to types \(\metavariable{\tau_i} \in \nonterm{T}\). is a finite mapping which assigns variables \(\metavariable{x_i} \in \exprvars\) to types \(\metavariable{\tau_i} \in \nonterm{T}\).
Using the inference rules given in \ref{def:typerules}, further typing-judgements
of the form \(\Gamma \vdash \metavariable{e} : \metavariable{\tau} \quad\) read as "expression \(\metavariable{e}\) is of type \(\metavariable{\tau}\)" %Using the inference rules given in \ref{def:pathrules} \ref{def:typerules}, further typing-judgements
can be derived from the context \(\Gamma\) where \(\metavariable{e} \in \nonterm{E}\) and \(\metavariable{\tau} \in \nonterm{T}\). %of the form \(\Gamma \vdash \metavariable{e} : \metavariable{\tau} \quad\) read as "expression \(\metavariable{e}\) is of type \(\metavariable{\tau}\)"
%can be derived from the context \(\Gamma\) where \(\metavariable{e} \in \nonterm{E}\) and \(\metavariable{\tau} \in \nonterm{T}\).
\subsubsection{Morphism Graph}
Every typing context \(\Gamma\) implies a \emph{Morphism Graph}, a directed graph whose vertices are types
and the edges represent a type-transformations, as defined by morphisms.
A type \(\metavariable{\tau}\) can be implicitly coerced into a type \(\metavariable{\tau'}\),
provided there is a path from \(\metavariable{\tau}\) to \(\metavariable{\tau'}\) in the \emph{Morphism-Graph} of \(\Gamma\),
written as \(\Gamma \vdash \metavariable{\tau} \leadsto \metavariable{\tau'}\).
\begin{definition}[Morphism Paths] \begin{definition}[Morphism Paths]
Given a typing context \(\Gamma\), any type \(\metavariable{\tau}\) can be transformed into \(\metavariable{\tau'}\), provided there is a path from \(\metavariable{\tau}\) to \(\metavariable{\tau'}\) in the \emph{Morphism-Graph} of \(\Gamma\), written as \(\Gamma \vdash \metavariable{\tau} \leadsto \metavariable{\tau'}\).
\label{def:pathrules} \label{def:pathrules}
\begin{mathpar} \begin{mathpar}
@ -783,6 +789,20 @@ D_1
\and \and
\Big{\llbracket}
\inferrule[T-MorphAbs]{
D_1 :: \Gamma,\metavariable{x}:\metavariable{\tau} \vdash \metavariable{e} : \metavariable{\tau'} \\
\metavariable{\tau} \precsim \metavariable{\tau'}
}{
\Gamma \vdash (\exprterminal{\lambda} \metavariable{x} \exprterminal{:} \metavariable{\tau} \exprterminal{\mapsto_{morph}} \metavariable{e}) : \metavariable{\tau}\typeterminal{\rightarrow_\text{morph}}\metavariable{\tau'}
}
\Big{\rrbracket} =
\exprterminal{\lambda} \metavariable{x} \exprterminal{:} \metavariable{\tau}
\exprterminal{\mapsto_\text{morph}} \Big{\llbracket}D_1\Big{\rrbracket}
\and
\Big{\llbracket} \Big{\llbracket}
\inferrule[T-App]{ \inferrule[T-App]{
D_1 :: \Gamma \vdash \metavariable{f} : \metavariable{\sigma} \typeterminal{\rightarrow} \metavariable{\tau}\\ D_1 :: \Gamma \vdash \metavariable{f} : \metavariable{\sigma} \typeterminal{\rightarrow} \metavariable{\tau}\\
@ -908,13 +928,14 @@ Evaluation of an expression \(\metavariable{e} \in \nonterm{E}\) is defined by e
\inferrule[E-AppLamAscribe]{ \inferrule[E-AppLamAscribe]{
}{ }{
\exprterminal{( \lambda \metavariable{x}:\metavariable{\sigma} \mapsto \metavariable{e} )} \exprterminal{(( \lambda \metavariable{x}:\metavariable{\sigma} \mapsto \metavariable{e} )}
\exprterminal{\text{ as }} \exprterminal{\text{ as }}
\typeterminal{\metavariable{\tau}} \typeterminal{\metavariable{\tau}}
\metavariable{e} \exprterminal{)}
\metavariable{a}
\rightarrow_\beta \rightarrow_\beta
\metavariable{v} \exprterminal{( \lambda \metavariable{x}:\metavariable{\sigma} \mapsto \metavariable{e} )}
\metavariable{e} \metavariable{a}
} }
\end{mathpar} \end{mathpar}
\end{definition} \end{definition}
@ -924,10 +945,13 @@ Evaluation of an expression \(\metavariable{e} \in \nonterm{E}\) is defined by e
\begin{lemma}[Preservation] \begin{lemma}[Preservation]
\label{lemma:preservation} \label{lemma:preservation}
Assume the expression \(\metavariable{e}\) is well typed, i.e. \(\emptyset \vdash \metavariable{e} : \metavariable{\tau}\) Assume the expression \(\metavariable{e}\) is well typed,
for some type \(\metavariable{\tau}\). i.e. there is a type-derivation tree
Then forall \(\metavariable{e'}\) with \(\metavariable{e} \rightarrow_{\beta} \metavariable{e'}\) \(D :: \Gamma \vdash \metavariable{e} : \metavariable{\tau}\)
it holds that \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\) as well. for some type \(\metavariable{\tau}\) and context \(\Gamma\).
Then forall \(\metavariable{e'}\) with \(\llbracket D \rrbracket \rightarrow_{\beta} \metavariable{e'}\)
it holds that \(\Gamma \vdash \metavariable{e'} : \metavariable{\tau}\) as well.
\begin{proof} \begin{proof}
\todo{} \todo{}
@ -936,38 +960,31 @@ it holds that \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\) as we
\begin{lemma}[Progress] \begin{lemma}[Progress]
\label{lemma:progress} \label{lemma:progress}
If \(\emptyset \vdash \metavariable{e} : \metavariable{\tau}\), Assume the expression \(\metavariable{e}\) is well typed,
then either \(\metavariable{e}\) is a value i.e. there is a type-derivation tree
or there exists some \(\metavariable{e'}\) such that \(\metavariable{e} \rightarrow_{\beta} \metavariable{e'}\) \(D :: \Gamma \vdash \metavariable{e} : \metavariable{\tau}\)
for some type \(\metavariable{\tau}\) and context \(\Gamma\).
Then either \(\metavariable{e}\) is a value
or there exists some \(\metavariable{e'}\) such that \(\llbracket D \rrbracket \rightarrow_{\beta} \metavariable{e'}\)
\begin{proof} \begin{proof}
\todo{} \todo{}
\end{proof} \end{proof}
\end{lemma} \end{lemma}
\begin{theorem}[Syntactic Type Soundness] \begin{theorem}[Soundness]
\label{theorem:syntactic-soundness}
No syntactically well-typed expression is stuck.
Assume the typing derivation \(D :: \emptyset \vdash \metavariable{e}:\metavariable{\tau}\).
Then it never occurs that \(\metavariable{e} \rightarrow_{\beta}^{*} \metavariable{e'}\) where \metavariable{e'} is in normal form but not a value.
\begin{proof}
Follows from \ref{lemma:progress} and \ref{lemma:preservation}.
\end{proof}
\end{theorem}
\begin{theorem}[Semantic Type Soundness]
\label{theorem:semantic-soundness} \label{theorem:semantic-soundness}
No semantically well-typed expression is stuck. No well-typed expression is stuck.
Assume the typing derivation \(D :: \emptyset \vdash \metavariable{e}:\approx\metavariable{\tau}\). Assume the typing derivation \(D :: \Gamma \vdash \metavariable{e}:\metavariable{\tau}\).
Then it never occurs that \(\llbracket D \rrbracket \rightarrow_{\beta}^{*} \metavariable{e'}\) where \metavariable{e'} is in normal form but not a value. Then it never occurs that \(\llbracket D \rrbracket \rightarrow_{\beta}^{*} \metavariable{e'}\) where \metavariable{e'} is in normal form but not a value.
\begin{proof} \begin{proof}
Assume the typing derivation \(D :: \emptyset \vdash \metavariable{e}:\approx\metavariable{\tau}\). \todo{}
By \ref{lemma:translation}, \(\emptyset \vdash \llbracket D \rrbracket : \metavariable{\tau}\) %Assume the typing derivation \(D :: \Gamma \vdash \metavariable{e}:\approx\metavariable{\tau}\).
and thus it follows by \ref{theorem:syntactic-soundness} that \metavariable{e} is not stuck. %By \ref{lemma:translation}, \(\Gamma \vdash \llbracket D \rrbracket : \metavariable{\tau}\)
%and thus it follows by \ref{theorem:syntactic-soundness} that \metavariable{e} is not stuck.
\end{proof} \end{proof}
\end{theorem} \end{theorem}