λcube.md

System λ

The untyped lambda calculus

e ::=             terms:
  x               variable
  e e             application
  λ x . e         abstraction

System λ→

The simply Typed Lambda Calculus

• Terms depending on terms

k :: =            kinds:
  *               type of types

t ::=             types:
  a               variable
  t → t           arrow type

e ::=             terms:
  x               variable
  e e             application
  λ x : t . e     abstraction

Where bool : * and int : *

idBool : bool → bool
idBool = λ x : bool . x

idInt : int → int
idInt = λ x : int . x

System λΠ

• Terms depending on terms
• Types depending on terms

t ::=             types:
  a               variable
  t → t           arrow type
  Π x : t . e     abstraction

e ::=             terms:
  x               variable
  e e             application
  λ x : t . e     abstraction

System λ2

• Terms depending on terms
• Terms depending on types

k :: =            kinds:
  *               type of types

t ::=             types:
  a               variable
  t → t           arrow type

e ::=             terms:
  x               variable
  e e             application
  λ x : t . e     abstraction
  e t             type application
  Λ a : k . e     type abstraction

System λω_

• Terms depending on terms
• Types depending on types

k :: =            kinds:
  *               type of types
  k → k           arrow kind

t ::=             types:
  a               variable
  t → t           arrow type
  t t             application
  ∀ a : k . t     universal quantification

e ::=             terms:
  x               variable
  e e             application
  λ x : t . e     abstraction

System λω

Haskell, SML, Ocaml, Elm

λ2 + λω_

• Terms depending on terms
• Terms depending on types
• Types depending on types

k :: =            kinds:
  *               type of types
  k → k           arrow kind

t ::=             types:
  a               variable
  t → t           arrow type
  t t             application
  ∀ a : k . t     universal quantification

e ::=             terms:
  x               variable
  e e             application
  λ x : t . e     abstraction
  e t             type application
  Λ a : k . e     type abstraction

id : ∀ a : * . a → a
id = Λ a : * . λ x : a . x

System λΠω (Calculus of Constructions)

Idris, Agda, Lean, Coq

• Terms depending on terms
• Terms depending on types
• Types depending on types
• Types depending on terms

e ::=
  x              variables
  *              type of types
  e e            application
  ∀ x : e . e    quantification (∀ + Π)
  λ x : e . e    abstraction (λ + Λ)