Some modal effect typing rules

modal-effect-types.md

effect_context, Σ ::=
  | ε
  | E, Σ

effect_diff, Δ ::=
  | 1
  | -E, Σ
  | +E, Σ
  | Δ ∘ Δ

type, t ::=
    1
  | μ t -> μ t
  | t * t
  | { s }
  | < t >

scheme, s ::=
  | t 
  | t [ Σ ]

simple_mode, m ::=
  | global
  | local

mode, μ ::=
  | global
  | local (Δ)
  | data

context, Γ ::=
    ∅
  | Γ, x : s @ μ
  | Γ, lock(μ)

expression, e ::=
    𝔁
  | λ𝔁. e
  | e e
  | e e @ Δ
  | e e @ data
  | (e, e)
  | fst e
  | snd e
  | ()
  | let 𝔁 = e in e
  | wrap e @ s
  | unwarp e @ s
  | box e
  | unbox e
  | handle e with E
  | perform E
  | shift E e

Diff composition and inverse

    (Δ₁ ∘ Δ₂) ∘ Δ₃ = Δ₁ ∘ (Δ₂ ∘ Δ₃)

    ε ∘ Δ = Δ

    Δ ∘ ε = Δ

    +Σ₁ ∘ +Σ₂ = +Σ₁,Σ₂

    -Σ₁ ∘ -Σ₂ = -Σ₂,Σ₁

    -E,Σ₁ ∘ +E,Σ₂ = -Σ₁ ∘ +Σ₂

    +Σ₁,E ∘ -Σ₂,E = +Σ₁ ∘ -Σ₂

    (-Σ)⁻¹ = +Σ

    (+Σ)⁻¹ = -Σ

    ε⁻¹ = ε

    (Δ₁ ∘ Δ₂)⁻¹ = Δ₂⁻¹ ∘ Δ₁⁻¹

Diff applying judements

   ————————————————— apply_plus
    +Σ₁(Σ₂) = Σ₁,Σ₂

   ————————————————— apply_minus
    -Σ₁(Σ₁,Σ₂) = Σ₂

   ——————————— apply_empty
    ε(Σ) = Σ

    Δ₂(Σ₁) = Σ₂
    Δ₁(Σ₂) = Σ₃
   ———————————————————— apply_compose
    (Δ₁ ∘ Δ₂)(Σ₁) = Σ₃

   ————————————————————————————————— apply_mode_local
    Δ₁(local(Δ₂)) = local(Δ₁ ∘ Δ₂)

   ————————————————————— apply_mode_global
    Δ(global) = global

   ————————————————————— apply_mode_data
    Δ(data) = data

   ———————————— apply_context_empty
    ∅(μ) = μ

    Γ(μ₁) = μ₂
   ————————————————————————— apply_context_extend
    (Γ, x : s @ μ₃)(μ₁) = μ₂

    Γ(μ₁) = global
   —————————————————————————————— apply_context_global_lock
    (Γ, lock(global))(μ₁) = global

    Γ(μ₁) = μ₂
   —————————————————————————————— apply_context_data_lock
    (Γ, lock(data))(μ₁) = μ₂

    Γ(μ₁) = μ₂
    Δ⁻¹(μ₂) = μ₃
   ———————————————————————————— apply_context_local_lock
    (Γ, lock(local(Δ)))(μ₁) = μ₃

Subsumption judgements

   ——————————————————— global_local
    global ≤ local(Δ)

   ——————————————————— local_data
    local(Δ) ≤ data

   ———————— empty
    ε ≤ Σ

    Σ₁ ≤ Σ₂
   ——————————————— cons
    E, Σ₁ ≤ E, Σ₂

   —————————————— effect_local
    Σ ≤ local

   ———————————— effect_global
    ε ≤ global

Typing judgement

    μ₁ ≤ μ₂
    Γ ⊢ e : t @ μ₁ / Σ₁ / Σ₂
  ——————————————————————————— mode subsumption
    Γ ⊢ e : t @ μ₂ / Σ₁ / Σ₂

    Σ₁ ≤ Σ₂
    Γ ⊢ e : s @ μ / Σ₁ / Σ₃
  —————————————————————————— delayed effect context subsumption
    Γ ⊢ e : s @ μ / Σ₂ / Σ₃

    Σ₁ ≤ Σ₂
    Γ ⊢ e : s @ μ / Σ₃ / Σ₁
  —————————————————————————— curent effect context subsumption
    Γ ⊢ e : s @ μ / Σ₃ / Σ₂

    Γ ⊢ e : t [ Σ₁ ] @ μ / Σ₂ / Σ₃
  —————————————————————————————————— instantiation
    Γ ⊢ e : t @ μ / Σ₁ / Σ₃

    Γ ⊢ e : t @ μ / Σ₁ / Σ₂
  ———————————————————————————————— generalization
    Γ ⊢ e : t [ Σ₁ ] @ μ / ε / Σ₂

    Γ'(μ₁) = μ₂
  —————————————————————————————————————————— var
    Γ, 𝔁 : s @ μ₁, Γ' ⊢ 𝔁 : s @ μ₂ / ε / ε

    Σ₁ ≤ Σ₃
    Σ₂ ≤ Σ₃
    Σ₁ ≤ μ₃
    Γ , lock(μ₁), 𝔁 : t₁ @ μ₂ ⊢ e : t₂ @ μ₃ / Σ₁ / Σ₂
  ——————————————————————————————————————————————————————— lam
    Γ ⊢ λ 𝔁 . e : μ₂ t₁ → m₃ t₂ @ μ₁ / Σ₃ / ε

    Σ₁ ≤ Σ₅
    Σ₂ ≤ Σ₅
    Σ₃ ≤ Σ₅
    Σ₄ ≤ Σ₅
    Σ₃ ≤ m
    Γ ⊢ e₁ : m t₁ → μ t₂ @ local / Σ₁ / Σ₂
    Γ ⊢ e₂ : t₁ @ m / Σ₃ / Σ₄
  ——————————————————————————————————— apply_simple
    Γ ⊢ e₁ e₂ : t₂ @ μ / ε / Σ₅

    Σ₁ ≤ Σ₅
    Σ₂ ≤ Σ₅
    Δ⁻¹(Σ₃) = Σ₆
    Σ₄ ≤ Σ₅
    Σ₆ ≤ Σ₅
    Γ ⊢ e₁ : local(Δ) t₁ → μ t₂ @ local / Σ₁ / Σ₂
    Γ ⊢ e₂ : t₁ @ local(Δ) / Σ₃ / Σ₄
  —————————————————————————————————————————————————— apply_diff
    Γ ⊢ e₁ e₂ @ Δ : t₂ @ μ / ε / Σ₅

    Σ₁ ≤ Σ₅
    Σ₂ ≤ Σ₅
    Σ₄ ≤ Σ₅
    Γ ⊢ e₁ : data t₁ → μ t₂ @ local / Σ₁ / Σ₂
    Γ ⊢ e₂ : t₁ @ data / Σ₃ / Σ₄
  ————————————————————————————————————————————— apply_data
    Γ ⊢ e₁ e₂ @ data : t₂ @ μ / ε / Σ₅

    Γ ⊢ e₁ : t₁ @ μ / Σ₁ / Σ₂
    Γ ⊢ e₂ : t₂ @ μ / Σ₁ / Σ₂
  ——————————————————————————————————————— pair
    Γ ⊢ (e₁, e₂) : t₁ * t₂ @ μ / Σ₁ / Σ₂

    Γ ⊢ e : t₁ * t₂ @ μ / Σ₁ / Σ₂
  ————————————————————————————————— fst
    Γ ⊢ fst e : t₁ @ μ / Σ₁ / Σ₂

    Γ ⊢ e : t₁ * t₂ @ μ / Σ₁ / Σ₂
  ————————————————————————————————— snd
    Γ ⊢ snd e : t₂ @ μ / Σ₁ / Σ₂

  ————————————————————————— unit
    Γ ⊢ () : 1 @ μ / ε / ε

    Γ ⊢ e₁ : s₁ @ μ₁ / ε / Σ₂
    Γ, 𝔁 : s₁ @ μ₁ ⊢ e₂ : s₂ @ μ₂ / Σ₁ / Σ₂
  ——————————————————————————————————————————— let
    Γ ⊢ let 𝔁 = e₁ in e₂ : s₂ @ μ₂ / Σ₁ / Σ₂

    Γ ⊢ e : s @ m / Σ₁ / Σ₂
  ——————————————————————————————————————— wrap
    Γ ⊢ wrap e @ s : { s } @ m / Σ₁ / Σ₂

    Γ ⊢ e : { s } @ m / Σ₁ / Σ₂
  ————————————————————————————————————— unwrap
    Γ ⊢ unwrap e @ s : s @ m / Σ₁ / Σ₂

    Γ ⊢ e : t @ global / Σ₁ / Σ₂
  ————————————————————————————————————————————————— box
    Γ ⊢ box e : < t > @ μ / Σ₁ / Σ₂

    Γ ⊢ e : < t > @ μ / Σ₁ / Σ₂
  —————————————————————————————————————— unbox
    Γ ⊢ unbox e : t @ global / Σ₁ / Σ₂

    Γ, lock(local(+E,ε)) ⊢ e : s @ μ₁ / Σ₁ / E, Σ₂
    (-E,ε)(μ) = μ₂
  ———————————————————————————————————————————————————— handle
    Γ ⊢ handle e with E : s @ μ₂ / Σ₁ / Σ₂

    Γ, lock(local(-E,ε)) ⊢ e : s @ μ₁ / Σ₁ / Σ₂
    μ₁ + local(+E,ε) = μ₂
  ———————————————————————————————————————————————————— shift
    Γ ⊢ shift E e : s @ μ₂ / Σ₁ / E, Σ₂

  ——————————————————————————————————————— perform
    Γ ⊢ perform E : unit @ global / E, ε