typing.txt

A ::= α | α' | A B | ∀α. A | ∃α. A || ∀α. A | ∃α. A | A → B | •A | S(A) | bool  | G(X)
X ::= I | X ⊗ ... ⊗ Y | X ⊸ Y | •X | F(X) | Window 

Γ ::= · | Γ, x:A[i] 
        | Γ, x::A[i] 
        | Γ, α 
        | Γ, α=λα…. μβ.[C A | ... | C A'] 
        | Γ, α'=? | Γ, α'=A | ▪[x]


Term Typing

x::A[i] ∈ Γ 
i ≤ j
—————————————————
Γ ▷ x ⇒ A[j] ◁ Γ


x:A[i] ∈ Γ
—————————————————
Γ ▷ x ⇒ A[i] ◁ Γ


Γ₀ ⊢ e ⇒ A[i] ⊣ Γ₁
Γ₁ ⊢ A ≤ B ⊣ Γ₂
——————————————————
Γ₀ ▷ e ⇐ B[i] ◁ Γ₂


Γ ⊢ A
Γ ⊢ e ⇐ A[i] ⊣ Γ'
———————————————————————
Γ ▷ (e:A) ⇒ A[i] ◁ Γ'


Γ₁ ⊢ e₁ ⇒ A[i] ⊣ Γ₂ 
Γ₂, x:A ⊢ e₂ ⇔ D[i] ⊣ Γ₃
——————————————————————————————————
Γ₁ ▷ let x = e₁ in e₂ ⇔ D[i] ◁ Γ₃


Γ₀,Γ₁ = Purify(Γ)
Γ₀,▪[x], x:A[i] ⊢ e ⇐ A[i] ⊣ Γ₀', ▪[x], Γ₀''
————————————————————————————————————————————
Γ ▷ μx. e ⇐ A[i] ▷ Merge[Γ](Γ₀';Γ₁)


Γ, α=A ⊢ e ⇔ D[i] ⊣ Γ', α=A, Γ''
——————————————————————————————————
Γ ▷ let α = A in e ⇔ D[i] ◁ Γ'


Variable types

Γ ▷ e ⇐ Γ(α')[i] ◁ Γ'
———————————————————————
Γ ⊢ e ⇐ α'[i] ⊣ Γ'


Γ ▷ e ⇐ A[i] ◁ Γ'  A ≠ α'  
————————————————————————————
Γ ⊢ e ⇐ A[i] ⊣ Γ'


Γ ▷ e ⇒ α'[i] ◁ Γ'
———————————————————————
Γ ⊢ e ⇒ Γ(α')[i] ⊣ Γ'


Γ ▷ e ⇒ A[i] ◁ Γ'   A ≠ α'  
—————————————————————————————
Γ ⊢ e ⇒ A[i] ⊣ Γ'


Boolean types

———————————————————
Γ ⊢ t/f ⇐ bool ⊣ Γ


————————————————————————————————————————
Γ, α'=?, Γ' ⊢ t/f ⇐ α' ⊣ Γ, α'=bool, Γ'


Γ₀ ⊢ e ⇒ bool[i] ⊣ Γ₁
Γ₁ ⊢ e₁ ⇐ A[i] ⊣ Γ₂
Γ₂ ⊢ e₂ ⇐ A[i] ⊣ Γ₃
——————————————————————————————
Γ₀ ⊢ if(e, e₁, e₂) ⇐ A[i] ⊣ Γ₃


Γ₀ ⊢ e ⇒ α'[i] ⊣ Γ₁,α'=?,Γ₁'
Γ₁,α'=bool,Γ₁' ⊢ e₁ ⇐ A[i] ⊣ Γ₂
Γ₂ ⊢ e₂ ⇐ A[i] ⊣ Γ₃
——————————————————————————————
Γ₀ ⊢ if(e, e₁, e₂) ⇐ A[i] ⊣ Γ₃


Function types 

Γ, ▪[x], x:A[i] ⊢ e ⇐ B[i] ⊣ Γ', ▪[x], Γ''
————————————————————————————————————————————
Γ ▷ λx.e ⇐ A → B[i] ◁ Γ'


Γ, β'=?, γ'=?, α'=β'→γ', Γ' ⊢ λx.e ⇐ α'[i] ▷ Γ''
———————————————————————————————————————————————
Γ, α'=?, Γ' ▷ λx.e ⇐ α'[i] ◁ Γ'


Γ₁ ⊢ e₁ ⇒ A → B[i] ⊣ Γ₂
Γ₂ ⊢ e₂ ⇐ A[i] ⊣ Γ₃
—————————————————————
Γ₁ ▷ e₁ e₂ ⇒ B[i] ◁ Γ₃

Γ ⊢ e₁ ⇒ α'[i] ⊣ Γ₁,α'=?,Γ₂
Γ₁,β'=?,γ'=?,α'=β'→γ',Γ₂ ⊢ e₂ ⇐ β'[i] ⊣ Γ'
——————————————————————————————————————————
Γ ▷ e₁ e₂ ⇒ γ' ◁ Γ'


Delay types 

Γ ⊢ e ⇐ A[i+1] ⊣ Γ'
————————————————————
Γ ▷ •e ⇐ •A[i] ⊣ Γ'


Γ,β'=?,α'=•β',Γ' ⊢ e ⇐ A[i+1] ⊣ Γ''
———————————————————————————————————
Γ,α'=?,Γ' ▷ •e ⇐ α'[i] ⊣ Γ''


Γ₁ ⊢ e₁ ⇒ •A[i] ⊣ Γ₂
Γ₂, ▪[x], x:A[i+1] ⊢ e₂ ⇔ D[i] ⊣ Γ₃, ▪[x], Γ'
—————————————————————————————————————————————
Γ₁ ▷ let •x = e₁ in e₂ ⇔ D[i] ◁ Γ₃


Γ₁ ⊢ e₁ ⇒ α'[i] ⊣ Γ₂,α'=?,Γ₂'
Γ₂, β'=?, α'=•α', Γ₂', ▪[x], x:A[i+1] ⊢ e₂ ⇔ D[i] ⊣ Γ₃, ▪[x], Γ'
————————————————————————————————————————————————————————————————
Γ₁ ▷ let •x = e₁ in e₂ ⇔ D[i] ◁ Γ₃


Stream types

Γ₀ ⊢ e₀ ⇐ alloc ⊣ Γ₁
Γ₁ ⊢ e₁ ⇐ A[i] ⊣ Γ₂
Γ₂ ⊢ e₂ ⇐ S(A)[i+1] ⊣ Γ₃ 
—————————————————————————
Γ₀ ▷ cons(e₀,e₁,e₂) ⇐ S(A)[i] ◁ Γ₃


Γ₁ ⊢ e₁ ⇒ S(A)[i] ⊣ Γ₂
Γ₂, x:A[i], y:S(A)[i+1] ⊢ e₂ ⇔ D[i] ⊣ Γ₃, x:A[i], y:S(A)[i+1], Γ'
—————————————————————————————————————————————————————————————————
Γ₁ ▷ let x :: y = e₁ in e₂ ⇔ D[i] ◁ Γ₃


Γ₁ ⊢ e₁ ⇒ α'[i] ⊣ Γ₂
Γ₂, β'=?, x:β'[i], y:S(β')[i+1] ⊢ e₂ ⇔ D[i] ⊣ Γ₃, x:β'[i], y:S(β')[i+1], Γ'
————————————————————————————————————————————————————————————————————————————————
Γ₁ ▷ let x :: y = e₁ in e₂ ⇔ D[i] ◁ Γ₃


Pure types 

Γ₀,Γ₁ = Purify(Γ)
Γ₀ ⊢ e ⇐ A[i] ⊣ Γ₀'
—————————————————————————————————
Γ ▷ !e ⇐ !A[i] ◁ Merge[Γ](Γ₀;Γ₁)


Γ₀,β'=?, α'=!β',Γ₁ ⊢ !e ⇐ α' ⊣ Γ' 
—————————————————————————————————
Γ₀,α'=?,Γ₁ ▷ !e ⇐ α'[i] ◁ Γ'


Γ₁ ⊢ e₁ ⇒ α' ⊣ Γ₂, α'=?, Γ₂'
Γ₂, β'=?, α'=•β', Γ₂', u::β'[i] ⊢ e₂ ⇔ D[i] ⊣ Γ₃, u::β'[i], Γ₃'
———————————————————————————————————————————————————————————————
Γ₁ ▷ let !u = e₁ in e₂ ⇔ D[i] ◁ Γ₃


Recursive Types

Γ, ▪[δ], K¹=?, ..., Kⁿ=?, δ:K¹ → ... → Kⁿ → ∗ = λα¹...αⁿ. μα.[C¹ A¹ | ... | Cⁿ Aⁿ] 
   ⊢ e ⇐ D[i] ⊣ Γ', ▪[δ], Γ''
————————————————————————————————————————————————————————————————————————————————————
Γ ▷ datatype δ α¹ ... αⁿ = μα.[C¹ A¹ | ... | Cⁿ Aⁿ] in e ⇐ D[i] ◁ Γ'


Γ(δ) = λα¹...αⁿ. μδ.[C¹ A¹ | ... | Cⁿ Aⁿ]
Γ ⊢ e ⇐ [A¹/α¹, ..., Aⁿ/αⁿ]Aʲ[i] ⊣ Γ'
————————————————————————————————————————
Γ ▷ Cʲ e ⇐ δ A¹ ... Aⁿ [i] ⊣ Γ'


Γ(δ) = λα¹...αⁿ. μδ.[C¹ A¹ | ... | Cⁿ Aⁿ] 
Γ, α¹'=?, ..., αⁿ'=?, α' = δ α¹' ... αⁿ' ⊢ Cʲ ⇐ α'[i] ⊣ Γ'
——————————————————————————————————————————————————————————
Γ, α'=?, Γ' ▷ Cʲ e ⇐ α' [i] ⊣ Γ'


Γ⁰ ⊢ e ⇒ A[i] ⊣ Γ¹

Γ¹ ⊢ p¹ : A[i] ⊣ Γ¹' ↝ Θ¹ 
Γ¹', ▪[p¹], Θ¹ ⊢ e¹ ⇐ C[i] ⊣ Γ₂, ▪[p¹], Θ¹'
...
Γⁿ ⊢ pⁿ : A[i] ⊣ Γⁿ' ↝ Θⁿ
Γⁿ', ▪[pⁿ], Θⁿ ⊢ eⁿ ⇐ C[i] ⊣ Γⁿ⁺¹, ▪[pⁿ], Θⁿ'

Γⁿ⁺¹ ⊢ p[1], ..., p[n] : A covers 
——————————————————————————————————————————————————————————
Γ⁰ ▷ case(e, p¹ → e¹ | ... | pⁿ → eⁿ) ⇐ C[i] ◁ Γⁿ⁺¹


Universal Types 

Γ, α ⊢ e ⇐ A[i] ⊣ Γ',α,Γ''
———————————————————————————
Γ ▷ e ⇐ ∀α.A[i] ◁ Γ'


Γ ⊢ e ⇒ ∀α.A[i] ⊣ Γ'
———————————————————————————————
Γ ▷ e ⇒ [α'/α]A[i] ◁ Γ', α'=?


Existential Types


Γ, α'=? ⊢ e ⇐ [α'/α]A[i] ⊣ Γ',α'=_,Γ''
————————————————————————————————————————
Γ ▷ e ⇐ ∃α.A[i] ◁ Γ'


Γ ⊢ e ⇒ ∃α.A[i] ⊣ Γ'
———————————————————————
Γ ▷ e ⇒ A[i] ◁ Γ', α


GUI Types

Γ;· ⊢ t ⇐ A ⊣ Γ'; ·
——————————————————————————
Γ ▷ G(t) ⇐ G(A)[i] ◁ Γ'


Γ₀, β'=?, α'=G(β'),Γ₁; · ⊢ t ⇐ A[i] ⊣ Γ'; ·
————————————————————————————————————————————
Γ₀,α'=?,Γ₁ ▷ G(t) ⇐ α'[i] ◁ Γ'



Γ ⊢ e ⇒ G(A)[i] ⊣ Γ'
——————————————————————————————
Γ;Δ ▷ run(e) ⇒ A[i] ◁ Γ';Δ


Γ₁ ⊢ e ⇒ G(A)[i] ⊣ Γ₂, α'=?, Γ₂'
————————————————————————————————————————
Γ₁;Δ ▷ run(e) ⇒ A[i] ◁ Γ₂, α'=?, Γ₂';Δ


Nonlinear Types

Γ₁ ⊢ e ⇐ A[i] ⊣ Γ₂
————————————————————————————————
Γ₁;Δ ▷ F(e) ⇐ F(A)[i] ◁ Γ₂; Δ


Γ₁, β'=?, α'=?, Γ₁' ⊢ e ⇐ β'[i] ⊣ Γ₂
—————————————————————————————————————————
Γ₁, α'=?, Γ₁';Δ ▷ F(e) ⇐ α'[i] ◁ Γ₂; Δ



Γ₁; Δ₁ ⊢ e₁ ⇒ F(A) ⊣ Γ₂;Δ₂
Γ₂, x:A[i]; Δ₂ ⊢ e₂ ⇔ C ⊣ Γ₃, x:A[i], Γ₃'; Δ₃
——————————————————————————————————————————————
Γ₁; Δ₁ ▷ let F(x) = e₁ in e₂ ⇔ C ◁ Γ₃; Δ₃


Γ₁; Δ₁ ⊢ e₁ ⇒ α'[i] ⊣ Γ₂, α'=?, Γ₂';Δ₂
Γ₂, β'=?, α'=F(α'), Γ₂', x:A[i]; Δ₂ ⊢ e₂ ⇔ D[i] ⊣ Γ₃, x:A[i], Γ₃'; Δ₃
—————————————————————————————————————————————————————————————————————
Γ₁; Δ₁ ▷ let F(x) = e₁ in e₂ ⇔ D[i] ◁ Γ₃; Δ₃


Linear Function Types


Γ₁; Δ₁, ▪[x], x:A[i] ⊢ e ⇐ B[i] ⊣ Γ₂; Δ₂, ▪[x], ·
———————————————————————————————————————————————————
Γ₁; Δ₁ ▷ λx.e ⇐ A ⊸ B[i] ◁ Γ₂; Δ₂


Γ₁, α'=?, Γ₁'; Δ₁, ▪[x], x:A[i] ⊢ e ⇐ B[i] ⊣ Γ₂; Δ₂, ▪[x], ·
—————————————————————————————————————————————————————————————
Γ₁, α'=?, Γ₁'; Δ₁ ▷ λx.e ⇐ A ⊸ B[i] ◁ Γ₂; Δ₂


Γ₁; Δ₁ ⊢ e₁ ⇒ A ⊸ B[i] ⊣ Γ₂; Δ₂ 
Γ₂; Δ₂ ⊢ e₂ ⇐ A[i] ⊣ Γ₃; Δ₃
————————————————————————————————
Γ₁; Δ₁ ▷ e₁ e₂ ⇒ B[i] ◁ Γ₃; Δ₃


Γ₁; Δ₁ ⊢ e₁ ⇒ α'[i] ⊣ Γ₂, α'=?, Γ₂'; Δ₂ 
Γ₂, β'=?, γ'=?, α'=β'⊸γ', Γ₂'; Δ₂ ⊢ e₂ ⇐ A[i] ⊣ Γ₃; Δ₃
——————————————————————————————————————————————————————
Γ₁; Δ₁ ▷ e₁ e₂ ⇒ B[i] ◁ Γ₃; Δ₃


Linear let-binders

———————————————————————————————————————————
Γ₁; Δ₁, x:A[i], Δ₁' ▷ x:A[i] ◁ Γ₁; Δ₁, Δ₁'


Γ₁; Δ₁ ⊢ e₁ ⇒ A[i+k] ⊣ Γ₂; Δ₂
Γ₂; Δ₂, ▪[x], x:A[i+k] ⊢ e₂ ⇔ D[i] ⊣ Γ₃; Δ₃, ▪[x], ·
—————————————————————————————————————————————————————
Γ₁; Δ₁ ▷ let[k] x = e₁ in e₂ ⇔ D[i] ◁ Γ₃; Δ₃


Γ₁ ⊢ e ⇒ A[i] ⊣ Γ₂
Γ₂, ▪[x], x:A[i]; Δ₁ ⊢ e' ⇔ D[i] ⊣ Γ₃, ▪[x], Γ₃'; Δ₂
—————————————————————————————————————————————————————
Γ₁;Δ₁ ▷ let int x = e in e ⇔ D[i] ◁ Γ₃; Δ₂


Linear Conditionals


Γ₁ ⊢ e ⇒ bool[i] ⊣ Γ₂
Γ₂; Δ₁ ⊢ e₂ ⇐ D[i] ⊣ Γ₃; Δ₂
Γ₃; Δ₁ ⊢ e₃ ⇐ D[i] ⊣ Γ₄; Δ₂
———————————————————————————————————————
Γ₁; Δ₁ ▷ if(e, e₂, e₃) ⇐ D[i] ◁ Γ₄; Δ₂



Datatypes and Pattern Matching

Add Γ ::= ... | α={C[1] τ[1] | … | C[n] τ[n]}

Intuitionistic patterns

p ::= x | •x | !x | p :: xs | (p[1], …, p[n]) | C p 


The rule for pattern matching:

Γ⁰ ⊢ e ⇒ A ⊣ Γ¹
Γ ⊢ p[1], ..., p[n] : A covers 
Γ¹ ⊢ p¹ : A[i] ⊧ Γ[1]     Γ¹, ▪[p¹], Γ[1] ⊢ e¹ ⇐ D[i] ⊣ Γ², ▪[p¹], Γ[1]'
...
Γⁿ ⊢ pⁿ : A[i] ⊧ Γ[n]     Γⁿ, ▪[pⁿ], Γ[n] ⊢ eⁿ ⇐ D[i] ⊣ Γⁿ⁺¹, ▪[pⁿ], Γ[n+1]'
————————————————————————————————————————————————————————————————————————————
Γ₀ ▷ case e of { p¹ → e¹ | ... | pⁿ → eⁿ } ⇐ D[i] ◁ Γⁿ⁺¹


The variable generation judgement:

Γ ⊢ p : A ⊣ Γ' ↝ Θ

———————————————————————————
Γ ⊢ x : A[i] ⊣ Γ' ↝ x:A[i]


Γ, ▪[p], α'=? ⊢ p : [α'/α]A[i] ⊣ Γ', ▪[p], Γ'' ↝ Θ
—————————————————————————————————————————————————————
Γ ⊢ p : ∀α.A[i] ⊣ Γ' ↝ Γ'', Θ


Γ, ▪[p], α ⊢ p : A[i] ⊣ Γ', ▪[p], Γ'' ↝ Θ
—————————————————————————————————————————————
Γ ⊢ p : ∃α.A[i] ⊣ Γ' ↝ Γ'', Θ



———————————————————————————————
Γ ⊢ •x : •A[i] ⊣ Γ' ↝ x:A[i+1]


——————————————————————————————————————————————————————————
Γ₀,α'=?,Γ₁ ⊢ •x : α'[i] ⊣ Γ₀, β'=?, α'=•β', Γ₁ ↝ x:α'[i+1]


—————————————————————————
Γ ⊢ !x : !A[i] ↝ x::A[i]


—————————————————————————————————————————————————————————
Γ₀,α'=?,Γ₁ ⊢ !x : α'[i] ⊣ Γ₀, β'=?, α'=!β', Γ₁ ↝ x::α'[i]


Γ ⊢ p : A[i] ⊣ Γ' ↝ Θ
—————————————————————————————————————————————
Γ ⊢ p :: xs : S(A)[i] ⊣ Γ' ↝ Θ, xs:S(A)[i+1]


Γ₀, β'=?, α'=S(β'), Γ₁ ⊢ p : β'[i] ⊣ Γ' ↝ Θ
——————————————————————————————————————————————————
Γ₀,α'=?,Γ₁ ⊢ p :: xs : α'[i] ⊣ Γ' ↝ Θ, xs:α'[i+1]


Γ¹ ⊢ p¹ : A¹ ⊣ Γ² ↝ Θ¹
...
Γⁿ ⊢ pⁿ : Aⁿ ⊣ Γⁿ⁺¹ ↝ Θⁿ
—————————————————————————————————————————————————————
Γ¹ ⊢ (p¹, ..., pⁿ) : A¹ × ... × Aⁿ ⊣ Γⁿ⁺¹ ↝ Θ¹, …, Θⁿ


Γ ⊢ p : [μα.A[α]/α]A ⊣ Γ' ↝ Θ
———————————————————————————————
Γ ⊢ C p : δ α₁ ...αᵢ  ⊣ Γ' ↝ Θ


Linear patterns


Γ ⊢ p : A[i] ↝ Γ'; Θ; Δ


Γ ⊢ p : A[0] ↝ Γ'; Θ
———————————————————————————
Γ ⊢ F p : F A[0] ↝ Γ; Θ; ·


Γ₁, β'=?, α'=F(β), Γ₂ ⊢ p : β' ⊢ Γ'; Θ
——————————————————————————————————————
Γ₁, α'=?, Γ₂ ⊢ F p : α'[0] ↝ Γ'; Θ; ·


Γ₁ ⊢ p₁ : A₁[i] ↝ Γ₂; Θ₁; Δ₁ 
...
Γⱼ ⊢ pⱼ : Aⱼ[i] ↝ Γⱼ₊₁; Θⱼ₊₁; Δⱼ₊₁
———————————————————————————————————————————————————————————————————
Γ₁ ⊢ (p₁, ..., pⱼ) : A₁ ⊗ ... ⊗ Aⱼ [i] ↝ Γⱼ₊₁; Θ₁,...,Θⱼ₊₁; Δ₁,...,Δⱼ₊₁


Γ₁,β'₁=?,...,β'ⱼ=?,α'=β'₁⊗...⊗β'ⱼ,Γ₁' ⊢ p₁ : β'₁[i] ↝ Γ₂; Θ₁; Δ₁ 
...
Γⱼ ⊢ pⱼ : β'ⱼ[i] ↝ Γⱼ₊₁; Θⱼ₊₁; Δⱼ₊₁
———————————————————————————————————————————————————————————————————
Γ₁,α'=?,Γ₁' ⊢ (p₁, ..., pⱼ) : α' [i] ↝ Γⱼ₊₁; Θ₁,...,Θⱼ₊₁; Δ₁,...,Δⱼ₊₁


Γ ⊢ p : A[i+1] ↝ Γ'; ·; Θ
———————————————————————————
Γ ⊢ •p : •A[i] ↝ Γ';·;Θ


Γ₁,β'=?, α'=•β', Γ₁' ⊢ p : A[i+1] ↝ Γ'; ·; Θ
—————————————————————————————————————————————
Γ₁,α=?,Γ₁' ⊢ •p : •A[i] ↝ Γ';·;Θ



——————————————————————————
Γ ⊢ x : A[i] ↝ Γ;·;x:A[i]


Coverage checking

Γ ⊢ p¹, ..., pⁿ : A fail

——————————————
Γ ⊢ · : A fail


∃j ∈ 1..n   Γ ⊢ pʲ, ... q^q : Aʲ fail 
————————————————————————————————————————————————————————–
Γ ⊢ (p¹, ..., pⁿ), ... (q¹, ..., qⁿ) : A¹ × ... × Aⁿ  fail


       ⊥
——————————————————————
Γ ⊢ x, ... p : A fail


        ⊥
————————————————————————
Γ ⊢ •x, ... p : •A fail


        ⊥
————————————————————————
Γ ⊢ !x, ... p : !A fail


Γ ⊢ p, ..., q : A fail
————————————————————————————————————————
Γ ⊢ (p :: xs), ... (q :: ys) : S(A) fail


Γ(α) = λα¹...αʲ. μδ. [C¹ B¹ | ... | Cⁿ Bⁿ]
∃l ∈ 1..n.  Γ ⊢ pˡ, ..., qˡ : [A¹/α¹, ..., Aʲ/αʲ]Bˡ
———————————————————————————————————————————————————————————
Γ ⊢ C¹ p¹, ... C¹ q¹, ..., Cⁿ pⁿ, ... Cⁿ qⁿ : α A¹ .. Aʲ fail