jonnifyfsharp

Dive C0.1.1

From λ-calculus to LISP

A model where functions are the unit of computation, and the first language to make them data.

The functional tradition has a single root. In the 1930s, Alonzo Church described computation with nothing but functions — the λ-calculus. Two decades later, John McCarthy turned that idea into a working language — LISP — by making functions ordinary data a program can pass around and build. F# stands at the far end of that line: functions are values in F# because they were values in LISP, and they were values in LISP because they were the whole of the λ-calculus.

Reduce a term Module hub
C0.1.1 · part 1

Church's λ-calculus

Alonzo Church introduced the λ-calculus in the 1930s (the system was formalised around 1936) as a formal account of what it means to compute. It has a striking economy: everything is built from two acts.

Abstraction writes a function. The term λx.M denotes the function that, given an argument, returns the body M with that argument put in for x. Application calls one. The term M N applies the function M to the argument N. That is the entire grammar: variables, abstraction, and application.

From those two acts the λ-calculus is a universal model of computation — equal in power to the Turing machine, the result that underpins the Church–Turing thesis. Numbers are not built in; they are encoded as functions (the Church numerals), where a number n is the function that applies another function n times.

abstraction
λx.M — the function with parameter x and body M.
application
M N — apply the function M to the argument N.
β-reduction
the one computation step: apply a function by substituting its argument for the bound variable.
α-conversion
rename a bound variable; λx.x and λy.y are the same function.
bound / free
a variable is bound when a λ binds it; otherwise it is free.

Notation: λx.λy.x is a function of one argument that returns a function of one argument. Application associates to the left, so f a b means (f a) b — apply f to a, then apply the result to b.

One step at a time: β-reduction

Computation in the λ-calculus is β-reduction: find an application of a function to an argument — a redex — and replace it with the body of the function, the argument substituted in. Repeat until no redex remains. The result is the value.

Walk the canonical example below. The term (λx.λy.x) a b is the function that takes two arguments and returns the first — logicians call it K. Each step highlights the redex it is about to reduce.

β-reduction of (λx.λy.x) a b · return the first argument

@ apply @ λx.λy.x K a arg 1 b arg 2 K keeps arg 1 · result is a
  1. (λx.λy.x a) b redex: apply K to a · substitute x := a
  2. (λy.a) b redex: apply to b · substitute y := b (a has no y)
  3. a normal form — no redex remains
step 1 of 3 · the redex applies K to a · next, K returns a function ignoring its second argument

Computation is substitution. A function call is a redex; reducing it puts the argument in and moves on. The whole of the λ-calculus is that one rule, applied until nothing is left to apply.

λ-calculus

A function is the unit of computation; calling it means substituting the argument into the body.

F# today

(fun x -> x) is a value; applying it runs the same substitution the λ-calculus describes.

C0.1.1 · part 2

LISP: functions become data

The λ-calculus is a theory. LISP made it run. John McCarthy designed LISP and it was first implemented around 1958; his 1960 paper, Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I, set out the design. The name is short for LISt Processor: the list — written as a parenthesised s-expression — is the central structure, and the same s-expression notation writes both the data and the program (homoiconicity, code as data).

LISP took Church's λ notation directly: an anonymous function is written (lambda (x) ...), the same idea of abstraction made executable. It carried the rest of the functional kit with it — functions as first-class data that a program can pass and return, recursion and conditionals as the means of control, and automatic memory management (garbage collection), so a program building lists never had to free them by hand.

(lambda (x) (* x x))      ; LISP: an anonymous function — Church's λx. x*x
((lambda (x) (* x x)) 5)  ; apply it to 5  => 25

// F#: the same anonymous function, the same application
(fun x -> x * x) 5            // => 25
first implemented
c. 1958 (John McCarthy); the design paper is 1960.
name
LISP — LISt Processor.
central structure
the list / s-expression — and code is written as data.
from Church
the lambda form — anonymous functions as values.
introduced
first-class functions, recursion, conditionals, automatic garbage collection.

The λ-calculus said functions are the computation. LISP said functions are also data — values to build, pass, and return — and gave the idea a runtime. Every functional language since, F# included, descends from that move.

The thread into F#

Two milestones, one idea growing more concrete. The λ-calculus is the theory: functions are the unit of computation, and a call is a substitution. LISP is the first practical language to treat functions as data and run them on a real machine, with recursion, conditionals, and garbage collection in the box.

What F# carries from this root is exactly that: functions are ordinary values. A function can be bound to a name, passed to another function, returned from one, and built at run time — the same first-class status LISP gave them, now with the static types the next dive adds. The line continues in C0.1.2, where the ML family makes those functions typed without making a programmer write the types down.

↑ C0.1 · ML lineage C0.1.2 · The ML family → C0.1.3 · F#'s birth

References

Sources

Related in this course