01Overview

Church proposed the lambda calculus in 1936: everything is a function and computation is reduction. λx.x+1 is the add-one function, and (λx.x+1) 2 reduces to 3. Church encodings represent numbers, Booleans and data structures with pure functions, showing that this tiny system is as powerful as a Turing machine.

Its value goes beyond computability. It gave birth to LISP, ML and Haskell, and it carries type theory and program semantics. Simply typed lambda calculus corresponds to intuitionistic logic, and the Curry–Howard correspondence identifies programs with proofs — writing a well-typed program is constructing a proof of a theorem.

02History

  1. 1936

    Church introduces the lambda calculus

    An equivalent model of computability, built from function abstraction.

  2. 1940

    Simply typed lambda calculus

    Church adds types to avoid paradoxes.

  3. 1958

    LISP appears

    McCarthy designs it at MIT, bringing the lambda calculus into programming languages.

  4. 1969

    Curry–Howard correspondence

    Programs and proofs are shown to be the same kind of object.

  5. 1970

    Denotational semantics

    Scott builds a model of the lambda calculus from domain theory.

03Core concepts

α / β reduction

Renaming bound variables, and applying a function to an argument.

Higher-order functions

Functions as arguments and results: the basic unit of composition.

Church encodings

Representing numbers, Booleans and lists with nothing but functions.

04Hands-on

Do it once — it beats reading it ten times

Implement TRUE/FALSE/IF and Church-numeral addition and multiplication using only JS arrow functions

05Self-check

Say it in your own words first, then open the answer. Whatever you cannot explain is what to review next.

Can you explain "α / β reduction"?

Renaming bound variables, and applying a function to an argument.

Can you explain "Higher-order functions"?

Functions as arguments and results: the basic unit of composition.

Can you explain "Church encodings"?

Representing numbers, Booleans and lists with nothing but functions.

What problem did it solve, and why was there nothing better at the time?

Go back to the history section: how was this done before, and what did it cost?

If you had to build it today, how would you break it down?

Use the hands-on task above: write a plan of at most three steps before you start.

06Key people

A

Alonzo Church

1903 – 1995

Inventor of the lambda calculus.

H

Haskell Curry

1900 – 1982

Combinatory logic and the Curry–Howard correspondence.

07Further reading

  • Introduction to Combinators and λ-CalculusHindley & Seldin · 1986
  • The Implementation of Functional Programming LanguagesSimon Peyton Jones · 1987