Manuscript I@2 · I.tex · section · 85631fa7

Typing

Language, typing, and ownership › Typing · lines 353–407

Contexts assign types to distinct source variables and runtime names. Contexts separated in a multiplicative rule are disjoint. There is no structural weakening or contraction.

x : A ⊢ x : A q : Q ⊢ q : Q ⊢ * : 1 ⊢ 0 : Bit ⊢ 1 : Bit

\frac{Γ , x : A ⊢ t : B}{Γ ⊢ λ x : A . t : A ⊸ B} \frac{Γ ⊢ t : A ⊸ B Δ ⊢ u : A}{Γ , Δ ⊢ t u : B}

\frac{Γ ⊢ t : A Δ ⊢ u : B}{Γ , Δ ⊢ ⟨ t , u ⟩ : A \otimes B}

\frac{Γ ⊢ t : A \otimes B Δ , x : A , y : B ⊢ u : C}{Γ , Δ ⊢ let ⟨ x , y ⟩ = t in u : C}

\frac{Γ ⊢ t : 1 Δ ⊢ u : C}{Γ , Δ ⊢ let * = t in u : C}

\frac{Γ ⊢ b : Bit Δ ⊢ u : A Δ ⊢ u ^{'} : A}{Γ , Δ ⊢ if b then u else u ^{'} : A}

⊢ new : Q \frac{Γ ⊢ t : Q ^{\otimes n}}{Γ ⊢ V ( t ) : Q ^{\otimes n}} \frac{Γ ⊢ t : Q ^{\otimes n}}{Γ ⊢ Enter ( t ) : Bit ^{\otimes n}} .

The conditional is additive: its alternatives use the same context, but only one alternative executes. The bit $1$ selects the then-branch and $0$ the else-branch.

Displayed formulas in this passage

unlabeled · line 358
$x : A ⊢ x : A q : Q ⊢ q : Q ⊢ * : 1 ⊢ 0 : Bit ⊢ 1 : Bit$
unlabeled · line 369
$\frac{Γ , x : A ⊢ t : B}{Γ ⊢ λ x : A . t : A ⊸ B} \frac{Γ ⊢ t : A ⊸ B Δ ⊢ u : A}{Γ , Δ ⊢ t u : B}$
unlabeled · line 376
$\frac{Γ ⊢ t : A Δ ⊢ u : B}{Γ , Δ ⊢ ⟨ t , u ⟩ : A \otimes B}$
unlabeled · line 380
$\frac{Γ ⊢ t : A \otimes B Δ , x : A , y : B ⊢ u : C}{Γ , Δ ⊢ let ⟨ x , y ⟩ = t in u : C}$
unlabeled · line 386
$\frac{Γ ⊢ t : 1 Δ ⊢ u : C}{Γ , Δ ⊢ let * = t in u : C}$
unlabeled · line 390
$\frac{Γ ⊢ b : Bit Δ ⊢ u : A Δ ⊢ u ^{'} : A}{Γ , Δ ⊢ if b then u else u ^{'} : A}$
unlabeled · line 395
$⊢ new : Q \frac{Γ ⊢ t : Q ^{\otimes n}}{Γ ⊢ V ( t ) : Q ^{\otimes n}} \frac{Γ ⊢ t : Q ^{\otimes n}}{Γ ⊢ Enter ( t ) : Bit ^{\otimes n}} .$