Sum and Product Types
ProductsPermalink
For products, we have types τ:
- Binary τ1×τ2
- Nullary 1 or unit
and expressions e:
-
Ordered pairs ⟨e1,e2⟩
-
Projections e⋅1e⋅2
Statics:
Γ⊢⟨⟩:1 Γ⊢e1:τ1,Γ⊢e2:τ2Γ⊢⟨e1,e2⟩:τ1×τ2 Γ⊢e:τ1×τ2Γ⊢e⋅1:τ1,e⋅2:τ2Dynamics (two cases, lazy or eager):
lazy:
⟨e1,e2⟩valend lazy
eager:
e1↦e′1⟨e1,e2⟩↦⟨e′1,e2⟩ e1 val,e2↦e′2⟨e1,e2⟩↦⟨e1,e′2⟩ e1 val,e2 val⟨e1,e2⟩valend eager
e↦e′e⋅2↦e′⋅2 ⟨e1,e2⟩val⟨e1,e2⟩⋅i↦eiSumsPermalink
For sums, we have types τ:
- Binary Sum/Coproducts τ1+τ2
- Nullary 0 or void
and expressions e:
- Binary 1⋅e2⋅e
- Nullary
Note: abort doesn’t mean to abort!!!!!
Statics:
Γ⊢ei:τiΓ⊢i⋅ei:τ1+τ2 Γ⊢e:τ1+τ and Γ,x:τ1⊢e1:τ Γ,x:τ2⊢e2:τΓ⊢case_τe{1⋅x↪e1|2⋅x↪e2}:τ Γ⊢e:0Γ⊢case_e{}:τDynamics (two cases, lazy or eager):
lazy:
i⋅ei valend lazy
eager:
ei↦e′ii⋅ei↦i⋅e′i ei vali⋅ei valend eager
e↦e′case_τe{...}↦case_e′{...} i⋅ei valcase_τi⋅ei{1⋅x↪e′1|2⋅x↪e′2}↦[ei/x]e′i e↦e′case_e{}↦case_e′{}Some Type AlgebraPermalink
τ×1≅ττ1×(τ2×τ3)≅(τ1×τ2)×τ3τ1×τ2≅τ2×τ1τ+0≅ττ1+(τ2+τ3)≅(τ1+τ2)+τ3τ1+τ2≅τ2+τ1τ1×(τ2+τ3)≅(τ1×τ2)+(τ1×τ3)Algebra about functions (using the arrow notation):
τ→(ρ1×ρ2)≅(τ→ρ1)×(τ→ρ2)τ→1≅1Functions can also be written by exponential notation:
(ρ1×ρ2)τ≅ρτ1×ρτ21τ≅1Something like the dual:
(τ1+τ2)→ρ≅(τ1→ρ)×(τ2→ρ)0→ρ≅1In exponential notation:
ρτ1+τ2≅ρτ1×ρτ2ρ0≅1