Categorial Types and Lambda Calculus

• Syntax of Lambda Calculus

  • (λx.λy.f x y) a b

• Categorial types (\ = abstraction, • = application)

  • (X \ Y \ (F • X • Y)) • A • B

• Currying (type inference rule)

  • ((X \ (Y \ ((F • X) • Y))) • A) • B)

• Beta-reduction (type inference rule) w/ unification

  • (F • A) • B

• Better notation for semantics (visible "cancelling"):

  • (((((F•X)•Y)/Y)/X)•A)•B -> (F•A)•B

Notes: