Lambda λ Cube (by Hendrik 'Henk' Pieter Barendregt)

λcube.md

System λ

The untyped Lambda Calculus

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

System λ→

The first-order simply typed Lambda Calculus (Propositional Calculus/Logic)

• Terms depending on terms (allows terms to depend on terms, i.e. terms that can bind 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 λΠ

The first-order dependently typed Lambda Calculus (Predicate Calculus/Logic)

• Terms depending on terms (allows terms to depend on terms, i.e. terms that can bind terms)
• Types depending on terms (allows types to depend on terms, i.e. types that can bind 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

The second-order polymorphic typed Lambda Calculus (Propositional Calculus/Logic)

• Terms depending on terms (allows terms to depend on terms, i.e. terms that can bind terms)
• Terms depending on types (allows terms to depend on types, i.e. terms that can bind 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 λω_

The (weakly) higher-order (higher-kinded) typed Lambda Calculus (Propositional Calculus/Logic), Type Constructors

• Terms depending on terms (allows terms to depend on terms, i.e. terms that can bind terms)
• Types depending on types (allows types to depend on types, i.e. types that can bind 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 λΠ2 (λP2)

The second-order dependently typed polymorphic Lambda Calculus (Predicate Calculus/Logic)

λΠ + λ2

• Terms depending on terms (allows terms to depend on terms, i.e. terms that can bind terms)
• Types depending on terms (allows types to depend on terms, i.e. types that can bind terms)
• Terms depending on types (allows terms to depend on types, i.e. terms that can bind types)

System λΠω_ (λPω_)

The (weakly) higher-order (higher-kinded) dependently typed Lambda Calculus (Predicate Calculus/Logic)

λΠ + λω_

• Terms depending on terms (allows terms to depend on terms, i.e. terms that can bind terms)
• Types depending on terms (allows types to depend on terms, i.e. types that can bind terms)
• Types depending on types (allows types to depend on types, i.e. types that can bind types)

System λω

The higher-order (higher-kinded) typed polymorphic Lambda Calculus (Propositional Calculus/Logic)

Standard ML, OCaml, F#, Nemerle, Haskell, Scala 2

λ2 + λω_

• Terms depending on terms (allows terms to depend on terms, i.e. terms that can bind terms)
• Terms depending on types (allows terms to depend on types, i.e. terms that can bind types)
• Types depending on types (allows types to depend on types, i.e. types that can bind 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 λΠω (λPω, λC)

The higher-order (higher-kinded) dependently typed polymorphic Lambda Calculus (CoC - Calculus of Constructions)

Dependent ML, ATS, F*, Coq/Gallina, Matita, ALF, Cayenne, Epigram, Lean, LEGO, Agda, Idris, Ur/Web, Scala 3 (DOTty - Dependent Object Types)

λΠ + λ2 + λω_

• Terms depending on terms (allows terms to depend on terms, i.e. terms that can bind terms)
• Types depending on terms (allows types to depend on terms, i.e. types that can bind terms)
• Terms depending on types (allows terms to depend on types, i.e. terms that can bind types)
• Types depending on types (allows types to depend on types, i.e. types that can bind types)

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