How I learnt to love typed λ-calculus

Introduction

An experimental workshop to explore the computational foundation of the universe, and have fun

λ-Calculus Syntax

A term from the λ-Calculus is either:

• A Symbol: x, y, Foo, ++…
• An Abstraction: (lam (x) x)
• An Application: (foo bar)

λ-Calculus Rules

Terms from the λ-Calculus can be rewritten using various rules the two main ones being:

• α-renaming:

  (lam (x) x) ⟹ (lam (y) y)

• β-reduction:

  ((lam (x) body) term) ⟹ body[x ← term]

λ-Calculus Extensions

• Syntactic sugar:
  • (lam (x) (lam (y) y)) ⟹ (lam (x y) y)
  • ((foo bar) baz) ⟹ (foo bar baz)
• Local definitions: (let ((id (lam (x) x))) (id foo))
• Global definitions: (def id (lam (x) x))

λ-Calculus Extensions

• Primitive data:
  • booleans: true, false
  • numbers: 12, 0.27
  • strings: "λ-calculus rocks"

Typed λ-Calculus

• The λ-Calculus is the favorite playground of type theorists
• There’s a whole zoo of type systems we won’t dive into (see you next year!)
• Search for _λ Cube_online…
• We’ll introduce Simply Typed λ-Calculus aka. λ_→

The Code

Action

Conclusion