simple extensions

Posted on In Views:

  • extensions to the simple typed λ-calculus

  • product types

  • sum types

  • fixed point

  • product types A×B = tuples, pairs, records, unit

  • sum types A+B = disjoint unions

  • fixed point construct = recursion

syntax, typing rules, reduction rules

  • product types

A₁×A₂ pair (e₁, e₂): A₁×A₂ projections fst e snd e

type A::= ⋯ | A×A expr e::= ⋯ | (e₁, e₂) | fst e | snd e value v::= ⋯ | (v₁, v₂)

typing rules

Γ ⊢ e₁:A₁ Γ ⊢ e₂:A₂ ----------------------------×I Γ ⊢ (e₁, e₂): A₁×A₂

Γ ⊢ e: A₁×A₂ ----------------------------×E₁ Γ ⊢ fst e:A₁

Γ ⊢ e: A₁×A₂ ----------------------------×E₂ Γ ⊢ snd e:A₂

reduction rules for (e₁, e₂) fst e snd e 1) "eager" (e₁, e₂)≠ a value 2) "lazy" (e₁, e₂) = a value

rule1 e₁ ↦ e₁' ----------------------------fst (e₁, e₂) ↦ (e₁', e₂)

e₁ -> -> -> v₁

rule2 e₂ ↦ e₂' ----------------------------snd (v₁, e₂) ↦ (v₁, e₂')

e₂ -> -> -> v₂

(v₁, v₂)

rule3 e ↦ e' ----------------------------fst fst e ↦ fst e'

e -> -> -> v

----------------------------fst' fst (v₁ v₂) ↦ v₁

----------------------------snd' snd (v₁ v₂) ↦ v₂

"lazy strategy"

(e₁, e₂) a value

rule4 e ↦ e' ----------------------------fst fst e ↦ fst e'

rule5 e ↦ e' ----------------------------snd fst (e₁, e₂) ↦ e₁

e₁ -> -> -> v₁

  • generalized product types

type A::= ⋯ | A₁ × A₂ × ⋯ × Aₙ|unit expr e::= ⋯ | (e₁, e₂, ⋯ eₙ) | projᵢ e | () value v::= ⋯ | (v₁, v₂)

Γ ⊢ eᵢ:Aᵢ 1≤i≤n ----------------------------————-×I Γ ⊢ (e₁, e₂, ⋯ eₙ): A₁×A₂× ⋯ × Aₙ

Γ ⊢ e: A₁×A₂× ⋯ × Aₙ ----------------------------×E Γ ⊢ projᵢ e:Aᵢ

n = 0 <- null-ary case

()

  • sum types a value of A₁ + A₂ => contains a value of A₁ or a value of A₂ not both.

e:A₁ e:A₂ :A₁+A₂ :A₁+A₂

inl_A₂ e:A₁+A₂ inr_A₁ e:A₁+A₂

inleft: injection left inright: injection right

e:A₁+A₂ e:A₁ or e:A₂

λx:A₁+A₂ e

=> case analysis e=>inl_A₂ v e=>inr_A₁ v

case e of inl x₁ e₁ | inr x₂ e₂

type A::= ⋯ | A₁+A₂ expr e::= ⋯ | inl_A e | inr_A e | case e of inl x e | inr x e

Γ ⊢ e:A₁ --------------------------- +Iₗ Γ ⊢ inl_A₂ e: A₁ + A₂

Γ ⊢ e:A₂ --------------------------- +Iᵣ Γ ⊢ inr_A₁ e: A₁ + A₂

Γ ⊢ e: A₁ + A₂ Γ, x₁:A₁ ⊢ e₁:C Γ, x₂:A₂ ⊢ e₂:C --------------------------------------------- case Γ ⊢ case e of inl x₁ e₁ | inr x₂ e₂ : C

if e then e₁ else e₂

  • reduction rules

inl e inl v value v::= ⋯ | inl_A v | inr_A v

e ↦ e' --------------------inl inl_A e ↦ inl_A e'

e ↦ e' --------------------inr inr_A e ↦ inr_A e'

e ↦ e' ----------------------------------------case case e of inl x₁ e₁ | inr x₂ e₂ ↦ case e' of inl x₁ e₁ | inr x₂ e₂

--------------------------------------------------case' case inl_A v of inl x₁ e₁ | inr x₂ e₂ ↦ [v|x₁]e₁ inr_A v ↦ [v|x₂]e₂

A::= ⋯|A×A|uint|A+A bool = unit + unit true = inl_unit () false = inr_unit ()

if e then e₁ else e₂ = case e of inl x₁ e₁ | inr x₂ e₂ — x₁ x₂ unit dummy variable

A::= ⋯|A₁+A₂+ ⋯ + Aₙ n ≥ 2 n = 0 A::= ⋯|void expr::=⋯|abort e

  • extension fixed point

  • fixed point construct (for recursive func) ≠ fixed point combinator in untyped λ = primitive construct

expr e::= ⋯|fix x:A.e

fix x:A.e = fixed point of λx:A.e A→A

f(x) = 2 - x: int -> int f(1) = 1

Γ, x:A ⊢ e:A -------------------------fix Γ ⊢ fix x:A.e

λx:A.e (fix x:A.e) = fix x:A.e

↦ [fix x:A.e | x]e

------------------------------fix fix x:A.e ↦ [fix x:A.e | x]e

fix x:A.e under CB-value

fix f:A→B. λx:A.e ↦ [fix f:A→B. λx:A.e | f] λx:A.e ↦ λx:A[fix f:A→B. λx:A.e | f] e