coq: add translate_typing

add one more typing example

coq/_CoqProject

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

coq/bbencode.v

@@ -55,13 +55,8 @@ Definition bb_succ : expr_term :=
                     (expr_var "z")))))))).
 
 Definition e1 : expr_term :=
-  (expr_let "bb-zero" (type_ladder (type_id "ℕ")
-                        (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_let "bb-zero" bb_zero
+      (expr_app (expr_app (expr_var "+") (expr_var "bb-zero")) (expr_var "bb-zero"))
   ).
 
 Definition t1 : expr_term := (expr_app (expr_var "x") (expr_var "x")).

coq/context.v

@@ -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.

coq/morph.v

@@ -3,66 +3,100 @@ Require Import terms.
 Require Import subst.
 Require Import equiv.
 Require Import subtype.
-Require Import typing.
+Require Import context.
 
 Include Terms.
 Include Subst.
 Include Equiv.
 Include Subtype.
-Include Typing.
+Include Context.
 
 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 :=
-
-  | Expand_Transform : forall Γ e h τ τ',
+  | M_Single : forall Γ h τ τ',
     (context_contains Γ h (type_morph τ τ')) ->
-    (Γ |- e \is τ) ->
-    (Γ |- [[ e ]] = (expr_app (expr_var h) e))
+    (Γ |- τ ~> τ')
 
-  | Expand_Otherwise : forall Γ e,
-    (Γ |- [[ e ]] = e)
+  | M_Chain : forall Γ τ τ' τ'',
+    (Γ |- τ ~> τ') ->
+    (Γ |- τ' ~> τ'') ->
+    (Γ |- τ ~> τ'')
 
-  | Expand_App : forall Γ f f' a a' σ τ,
-    (Γ |- f \compatible (type_fun σ τ)) ->
-    (Γ |- a \compatible σ) ->
-    (Γ |- [[ f ]] = f') ->
-    (Γ |- [[ a ]] = a') ->
-    (Γ |- [[ (expr_app f a) ]] = (expr_app f a'))
+  | M_Lift : forall Γ σ τ τ',
+    (Γ |- τ ~> τ') ->
+    (Γ |- (type_ladder σ τ) ~> (type_ladder σ τ'))
 
-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 *)
-Lemma well_typed_is_expandable :
-  forall (e:expr_term),
-  (is_well_typed e) ->
-  exists Γ e', (expand_morphisms Γ e e') -> (is_exactly_typed e')
+Inductive translate_morphism_path : context -> type_term -> type_term -> expr_term -> Prop :=
+  | Translate_Subtype : forall Γ τ τ',
+    (τ :<= τ') ->
+    (translate_morphism_path Γ τ τ'
+        (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.
-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.

coq/soundness.v

@@ -22,15 +22,6 @@ Definition is_stuck (e:expr_term) : Prop :=
   ~(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 *)
 Lemma progress :
   forall (e:expr_term),
@@ -40,32 +31,14 @@ Proof.
   
 Admitted.
 
-(* reduction step preserves the type *)
-Lemma exact_preservation :
+(* reduction step preserves well-typedness *)
+Lemma preservation :
   forall Γ e e' τ,
   (Γ |- e \is τ) ->
   (e -->β e') ->
   (Γ |- e' \is τ)
 .
 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.
 
 (* every well-typed expression can be reduced to a value *)

coq/subst.v

@@ -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_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_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_descend t e => expr_descend t (expr_subst v n e)
   end.

coq/terms.v

@@ -25,12 +25,11 @@ Inductive expr_term : Type :=
   | 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_let : string -> expr_term -> expr_term -> expr_term
   | expr_ascend : type_term -> expr_term -> expr_term
   | expr_descend : type_term -> expr_term -> expr_term
 .
 
-
 (* TODO
 
 Inductive type_DeBruijn : Type :=
@@ -99,11 +98,20 @@ 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_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).
-
-
+  (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 *)
 
@@ -112,7 +120,7 @@ Open Scope ladder_expr_scope.
 
 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"% }].
 
 Compute polymorphic_identity1.

coq/typing.v

@@ -6,64 +6,55 @@ Require Import terms.
 Require Import subst.
 Require Import equiv.
 Require Import subtype.
+Require Import context.
+Require Import morph.
 
 Include Terms.
 Include Subst.
 Include Equiv.
 Include Subtype.
+Include Context.
+Include Morph.
 
 Module Typing.
 
 (** 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 '\compatible' X"  (at level 101, x at next level, X at level 0).
 
 Inductive expr_type : context -> expr_term -> type_term -> Prop :=
   | T_Var : forall Γ x τ,
     (context_contains Γ x τ) ->
     (Γ |- (expr_var x) \is τ)
 
-  | T_Let : forall Γ s (σ:type_term) t τ x,
+  | T_Let : forall Γ s σ t τ x,
     (Γ |- s \is σ) ->
-    (Γ |- t \is τ) ->
-    (Γ |- (expr_let x σ s t) \is τ)
+    ((ctx_assign x σ Γ) |- t \is τ) ->
+    (Γ |- (expr_let x s t) \is τ)
 
-  | T_TypeAbs : forall Γ (e:expr_term) (τ:type_term) α,
+  | T_TypeAbs : forall Γ e τ α,
     Γ |- e \is τ ->
     Γ |- (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 α τ) ->
-    Γ |- (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),
-    (context_contains Γ x σ) ->
-    Γ |- t \is τ ->
-    Γ |- (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_Abs : forall Γ x σ t τ,
+    ((ctx_assign x σ Γ) |- t \is τ) ->
+    (Γ |- (expr_abs x σ t) \is (type_fun σ τ))
 
   | T_MorphAbs : forall Γ x σ e τ,
-    (context_contains Γ x σ) ->
-    Γ |- e \is τ ->
+    ((ctx_assign x σ Γ) |- e \is τ) ->
     Γ |- (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 σ τ,
     Γ |- f \is (type_morph σ τ) ->
     Γ |- f \is (type_fun σ τ)
@@ -73,84 +64,111 @@ Inductive expr_type : context -> expr_term -> type_term -> Prop :=
     (τ' :<= τ) ->
     (Γ |- (expr_ascend τ' e) \is τ')
 
-  | T_Descend : forall Γ x τ τ',
+  | T_DescendImplicit : forall Γ x τ τ',
     Γ |- x \is τ ->
     (τ :<= τ') ->
     Γ |- x \is τ'
 
+  | T_Descend : forall Γ x τ τ',
+    Γ |- x \is τ ->
+    (τ :<= τ') ->
+    Γ |- (expr_descend τ' x) \is τ'
+
 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 :=
   exists Γ τ,
-  Γ |- e \compatible τ
+  Γ |- e \is τ
 .
 
-Definition is_exactly_typed (e:expr_term) : Prop :=
-  exists Γ τ,
-  Γ |- e \is τ
+Inductive translate_typing : context -> expr_term -> type_term -> expr_term -> Prop :=
+  | Expand_Var : forall Γ x τ,
+    (Γ |- (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 *)
 
 Example typing1 :
-  forall Γ,
-  (context_contains Γ "x" [< %"T"% >]) ->
-  Γ |- [{ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% }] \is [< ∀"T", %"T"% -> %"T"% >].
-   (* Γ |- [ ΛT ↦ λx:T ↦ x ] : ∀T.(T->T) *)
+  ctx_empty |- [{ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% }] \is [< ∀"T", %"T"% -> %"T"% >].
 Proof.
   intros.
   apply T_TypeAbs.
   apply T_Abs.
-  apply H.
   apply T_Var.
-  apply H.
+  apply C_take.
 Qed.
 
 Example typing2 :
-  forall Γ,
-  (context_contains Γ "x" [< %"T"% >]) ->
-  Γ |- [{ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% }] \is [< ∀"U", %"U"% -> %"U"% >].
+  ctx_empty |- [{ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% }] \is [< ∀"U", %"U"% -> %"U"% >].
 Proof.
   intros.
-  apply T_Descend with (τ:=[< ∀"T",(%"T"% -> %"T"%) >]).
+  apply T_DescendImplicit with (τ:=[< ∀"T",(%"T"% -> %"T"%) >]).
   apply T_TypeAbs.
   apply T_Abs.
-  apply H.
   apply T_Var.
-  apply H.
+  apply C_take.
 
   apply TSubRepr_Refl.
   apply TEq_Alpha.
@@ -161,22 +179,18 @@ Proof.
 Qed.
 
 Example typing3 :
-  forall Γ,
-  (context_contains Γ "x" [< %"T"% >]) ->
-  (context_contains Γ "y" [< %"U"% >]) ->
-  Γ |- [{
+  ctx_empty |- [{
     Λ"T" ↦ Λ"U" ↦ λ"x" %"T"% ↦ λ"y" %"U"% ↦ %"y"%
   }] \is [<
        ∀"S",∀"T",(%"S"%->%"T"%->%"T"%)
   >].
 Proof.
   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 H.
   apply T_Abs.
-  apply H0.
-  apply T_Var, H0.
+  apply T_Var.
+  apply C_take.
 
   apply TSubRepr_Refl.
   apply TEq_Trans with (y:= [< ∀"S",∀"U",(%"S"%->%"U"%->%"U"%) >] ).
@@ -200,24 +214,70 @@ 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 ctx_empty.
   exists [< ∀"T",∀"U",%"T"%->%"U"%->%"T"% >].
-  apply TCompat_Native.
   apply T_TypeAbs.
   apply T_TypeAbs.
   apply T_Abs.
-  apply C_take.
   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 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.
 
 End Typing.

paper/main.tex

@@ -518,17 +518,23 @@ while preserving its semantics.
 \end{enumerate}
 \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 \}\)
 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}\)"
-can be derived from the context \(\Gamma\) where \(\metavariable{e} \in \nonterm{E}\) and \(\metavariable{\tau} \in \nonterm{T}\).
+
+%Using the inference rules given in \ref{def:pathrules} \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}\)"
+%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]
-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}
 \begin{mathpar}
 
@@ -783,6 +789,20 @@ D_1
 \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}
 	\inferrule[T-App]{
 		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]{
 	}{
-		\exprterminal{( \lambda \metavariable{x}:\metavariable{\sigma} \mapsto \metavariable{e} )}
+		\exprterminal{(( \lambda \metavariable{x}:\metavariable{\sigma} \mapsto \metavariable{e} )}
 		\exprterminal{\text{ as }}
 		\typeterminal{\metavariable{\tau}}
-		\metavariable{e}
+		\exprterminal{)}
+		\metavariable{a}
 		\rightarrow_\beta
-		\metavariable{v}
-		\metavariable{e}
+		\exprterminal{( \lambda \metavariable{x}:\metavariable{\sigma} \mapsto \metavariable{e} )}
+		\metavariable{a}
 	}
 \end{mathpar}
 \end{definition}
@@ -924,10 +945,13 @@ Evaluation of an expression \(\metavariable{e} \in \nonterm{E}\) is defined by e
 
 \begin{lemma}[Preservation]
 \label{lemma:preservation}
-Assume the expression \(\metavariable{e}\) is well typed, i.e. \(\emptyset \vdash \metavariable{e} : \metavariable{\tau}\)
-for some type \(\metavariable{\tau}\).
-Then forall \(\metavariable{e'}\) with \(\metavariable{e} \rightarrow_{\beta} \metavariable{e'}\)
-it holds that \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\) as well.
+Assume the expression \(\metavariable{e}\) is well typed,
+i.e. there is a type-derivation tree
+\(D :: \Gamma \vdash \metavariable{e} : \metavariable{\tau}\)
+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}
 \todo{}
@@ -936,38 +960,31 @@ it holds that \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\) as we
 
 \begin{lemma}[Progress]
 \label{lemma:progress}
-If \(\emptyset \vdash \metavariable{e} : \metavariable{\tau}\),
-then either \(\metavariable{e}\) is a value
-or there exists some \(\metavariable{e'}\) such that \(\metavariable{e} \rightarrow_{\beta} \metavariable{e'}\)
+Assume the expression \(\metavariable{e}\) is well typed,
+i.e. there is a type-derivation tree
+\(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}
 \todo{}
 \end{proof}
 \end{lemma}
 
-\begin{theorem}[Syntactic Type 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]
+\begin{theorem}[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.
 
 \begin{proof}
-Assume the typing derivation \(D :: \emptyset \vdash \metavariable{e}:\approx\metavariable{\tau}\).
-By \ref{lemma:translation}, \(\emptyset \vdash \llbracket D \rrbracket : \metavariable{\tau}\)
-and thus it follows by \ref{theorem:syntactic-soundness} that \metavariable{e} is not stuck.
+\todo{}
+%Assume the typing derivation \(D :: \Gamma \vdash \metavariable{e}:\approx\metavariable{\tau}\).
+%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{theorem}