Changes between Version 9 and Version 10 of LinearTypes


Ignore:
Timestamp:
Dec 21, 2016 4:44:09 PM (8 months ago)
Author:
aspiwack
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • LinearTypes

    v9 v10  
    6969{{{
    7070––––––––––––––––––––––– variable
    71   ωΓ, x :ρ A ⊢ x :ρ A
     71  ωΓ + x :1 A ⊢ x : A
    7272 
    7373
    74  Γ ⊢ f :ρ S -­> T     Δ ⊢ s :ω S
     74 Γ ⊢ f : S -­> T     Δ ⊢ s : S
    7575–––––––––––––––––––––––––––––––– unrestricted application
    76           Γ+Δ ⊢ f s  :ρ  T
    77 
    78  Γ ⊢ f :ρ S ⊸ T     Δ ⊢ s :ρ S
     76          Γ+ωΔ ⊢ f s  :  T
     77
     78 Γ ⊢ f : S ⊸ T     Δ ⊢ s : S
    7979––––––––––––––––––––––––––––––– linear application
    80           Γ+Δ ⊢ f s  :ρ  T
    81 
    82        Γ, x :ω S  ⊢   t :ρ T
     80          Γ+Δ ⊢ f s  :  T
     81
     82       Γ, x :ω S  ⊢   t : T
    8383–––––––––––––––––––––––––––––––––– unrestricted abstraction
    84      Γ ⊢ λx. t  :ρ S → T
    85 
    86        Γ, x :1 S  ⊢   t :ρ T
     84     Γ ⊢ λx. t  : S → T
     85
     86       Γ, x :1 S  ⊢   t : T
    8787–––––––––––––––––––––––––––––––––– linear abstraction
    88      Γ ⊢ λx. t  :ρ  S ⊸ T
     88     Γ ⊢ λx. t  :  S ⊸ T
    8989}}}
    9090(The above two rules can be generalized by using a single arrow type with weights, say {{{Π(x :π A). B}}})