1 minute read

ProductsPermalink

For products, we have types τ:

  • Binary τ1×τ2
  • Nullary 1 or unit

and expressions e:

  • Ordered pairs e1,e2

  • Projections e1e2

Statics:

Γ:1 Γe1:τ1,Γe2:τ2Γe1,e2:τ1×τ2 Γe:τ1×τ2Γe1:τ1,e2:τ2

Dynamics (two cases, lazy or eager):

lazy:

e1,e2val

end lazy

eager:

e1e1e1,e2e1,e2 e1 val,e2e2e1,e2e1,e2 e1 val,e2 vale1,e2val

end eager

eee2e2 e1,e2vale1,e2iei

SumsPermalink

For sums, we have types τ:

  • Binary Sum/Coproducts τ1+τ2
  • Nullary 0 or void

and expressions e:

  • Binary 1e2e
case_τe{1xe1|2xe2}orcase_[τ](x.e1;x.e2)(e)
  • Nullary
case_{}orabort[τ]()

Note: abort doesn’t mean to abort!!!!!

Statics:

Γei:τiΓiei:τ1+τ2 Γe:τ1+τ and Γ,x:τ1e1:τ Γ,x:τ2e2:τΓcase_τe{1xe1|2xe2}:τ Γe:0Γcase_e{}:τ

Dynamics (two cases, lazy or eager):

lazy:

iei val

end lazy

eager:

eieiieiiei ei valiei val

end eager

eecase_τe{...}case_e{...} iei valcase_τiei{1xe1|2xe2}[ei/x]ei eecase_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)τ11

Functions can also be written by exponential notation:

(ρ1×ρ2)τρτ1×ρτ21τ1

Something like the dual:

(τ1+τ2)ρ(τ1ρ)×(τ2ρ)0ρ1

In exponential notation:

ρτ1+τ2ρτ1×ρτ2ρ01