Sum and Product Types

February 17, 2018 1 minute read

ProductsPermalink

For products, we have types $τ$ :

and expressions $e$ :

Statics:

\frac{}{Γ ⊢ ⟨ ⟩ : 1}

\frac{Γ ⊢ e_{1} : τ_{1}, Γ ⊢ e_{2} : τ_{2}}{Γ ⊢ ⟨ e_{1}, e_{2} ⟩ : τ_{1} \times τ_{2}}

\frac{Γ ⊢ e : τ_{1} \times τ_{2}}{Γ ⊢ e \cdot 1 : τ_{1}, e \cdot 2 : τ_{2}}

Dynamics (two cases, lazy or eager):

lazy:

\frac{}{⟨ e_{1}, e_{2} ⟩ v a l}

end lazy

eager:

\frac{e_{1} \mapsto e_{1}^{'}}{⟨ e_{1}, e_{2} ⟩ \mapsto ⟨ e_{1}^{'}, e_{2} ⟩}

\frac{e_{1} v a l, e_{2} \mapsto e_{2}^{'}}{⟨ e_{1}, e_{2} ⟩ \mapsto ⟨ e_{1}, e_{2}^{'} ⟩}

\frac{e_{1} v a l, e_{2} v a l}{⟨ e_{1}, e_{2} ⟩ v a l}

end eager

\frac{e \mapsto e^{'}}{e \cdot 2 \mapsto e^{'} \cdot 2}

\frac{⟨ e_{1}, e_{2} ⟩ v a l}{⟨ e_{1}, e_{2} ⟩ \cdot i \mapsto e_{i}}

For sums, we have types $τ$ :

and expressions $e$ :

{\underline{c a s e}}_{τ} e {1 \cdot x ↪ e_{1} | 2 \cdot x ↪ e_{2}} o r \underline{c a s e} [τ] (x . e_{1}; x . e_{2}) (e)

\underline{c a s e} {} o r a b o r t [τ] ()

Note: $a b o r t$ doesn’t mean to abort!!!!!

Statics:

\frac{Γ ⊢ e_{i} : τ_{i}}{Γ ⊢ i \cdot e_{i} : τ_{1} + τ_{2}}

\frac{Γ ⊢ e : τ_{1} + τ a n d Γ, x : τ_{1} ⊢ e_{1} : τ Γ, x : τ_{2} ⊢ e_{2} : τ}{Γ ⊢ {\underline{c a s e}}_{τ} e {1 \cdot x ↪ e_{1} | 2 \cdot x ↪ e_{2}} : τ}

\frac{Γ ⊢ e : 0}{Γ ⊢ \underline{c a s e} e {} : τ}

Dynamics (two cases, lazy or eager):

lazy:

\frac{}{i \cdot e_{i} v a l}

end lazy

eager:

\frac{e_{i} \mapsto e_{i}^{'}}{i \cdot e_{i} \mapsto i \cdot e_{i}^{'}}

\frac{e_{i} v a l}{i \cdot e_{i} v a l}

end eager

\frac{e \mapsto e^{'}}{{\underline{c a s e}}_{τ} e {. . .} \mapsto \underline{c a s e} e^{'} {. . .}}

\frac{i \cdot e_{i} v a l}{{\underline{c a s e}}_{τ} i \cdot e_{i} {1 \cdot x ↪ e_{1}^{'} | 2 \cdot x ↪ e_{2}^{'}} \mapsto [e_{i} / x] e_{i}^{'}}

\frac{e \mapsto e^{'}}{\underline{c a s e} e {} \mapsto \underline{c a s e} e^{'} {}}

τ \times 1 ≅ τ τ_{1} \times (τ_{2} \times τ_{3}) ≅ (τ_{1} \times τ_{2}) \times τ_{3} τ_{1} \times τ_{2} ≅ τ_{2} \times τ_{1} τ + 0 ≅ τ τ_{1} + (τ_{2} + τ_{3}) ≅ (τ_{1} + τ_{2}) + τ 3 τ_{1} + τ_{2} ≅ τ_{2} + τ_{1} τ_{1} \times (τ_{2} + τ_{3}) ≅ (τ_{1} \times τ_{2}) + (τ_{1} \times τ_{3})

Algebra about functions (using the arrow notation):

τ \to (ρ_{1} \times ρ_{2}) ≅ (τ \to ρ_{1}) \times (τ \to ρ_{2}) τ \to 1 ≅ 1

Functions can also be written by exponential notation:

(ρ_{1} \times ρ_{2})^{τ} ≅ ρ_{1}^{τ} \times ρ_{2}^{τ} 1^{τ} ≅ 1

Something like the dual:

(τ_{1} + τ_{2}) \to ρ ≅ (τ_{1} \to ρ) \times (τ_{2} \to ρ) 0 \to ρ ≅ 1

In exponential notation:

ρ^{τ_{1} + τ_{2}} ≅ ρ^{τ_{1}} \times ρ^{τ_{2}} ρ^{0} ≅ 1