Changes between Version 9 and Version 10 of LinearTypes
 Timestamp:
 Dec 21, 2016 4:44:09 PM (5 months ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

LinearTypes
v9 v10 69 69 {{{ 70 70 ––––––––––––––––––––––– variable 71 ωΓ , x :ρ A ⊢ x :ρA71 ωΓ + x :1 A ⊢ x : A 72 72 73 73 74 Γ ⊢ f : ρ S > T Δ ⊢ s :ωS74 Γ ⊢ f : S > T Δ ⊢ s : S 75 75 –––––––––––––––––––––––––––––––– unrestricted application 76 Γ+ Δ ⊢ f s :ρT77 78 Γ ⊢ f : ρ S ⊸ T Δ ⊢ s :ρS76 Γ+ωΔ ⊢ f s : T 77 78 Γ ⊢ f : S ⊸ T Δ ⊢ s : S 79 79 ––––––––––––––––––––––––––––––– linear application 80 Γ+Δ ⊢ f s : ρT81 82 Γ, x :ω S ⊢ t : ρT80 Γ+Δ ⊢ f s : T 81 82 Γ, x :ω S ⊢ t : T 83 83 –––––––––––––––––––––––––––––––––– unrestricted abstraction 84 Γ ⊢ λx. t : ρS → T85 86 Γ, x :1 S ⊢ t : ρT84 Γ ⊢ λx. t : S → T 85 86 Γ, x :1 S ⊢ t : T 87 87 –––––––––––––––––––––––––––––––––– linear abstraction 88 Γ ⊢ λx. t : ρS ⊸ T88 Γ ⊢ λx. t : S ⊸ T 89 89 }}} 90 90 (The above two rules can be generalized by using a single arrow type with weights, say {{{Π(x :π A). B}}})