Overview
In the previous part, we built a calculator language with integers, booleans, and a type system. While powerful, that language lacked one crucial feature: abstraction.
We could write + 1 2 but not define reusable functions like add_two(x) = x + 2.
In this part, we bridge this gap by introducing lambda calculus, the theoretical foundation of functional programming. We’ll progressively build up from the simplest possible function system to a rich language with various data types.
This part is organized as follows:
-
Variables and Abstraction introduces the untyped lambda calculus as the foundation for functional programming. You’ll learn about variables, function abstraction (), application, and the critical concepts of free vs bound variables and substitution.
-
Alpha-Equivalence and Capture-Avoiding Substitution covers the subtleties of variable naming and substitution. You’ll understand how to avoid variable capture and why alpha-equivalence (renaming bound variables) is essential for reasoning about programs.
-
Big Steps, Small Steps explores how computation actually happens through big-step and small-step semantics. Building on the rewriting systems from Part 1, we’ll study -reduction as the core computational step and understand different reduction strategies.
-
Multiple Steps and Normgalization introduces the concept of multi-step reduction and normalization. You’ll learn about normal forms and weak vs strong normalization.
-
Natural Numbers and Arithmetic reintroduces numbers, but this time from a more foundational perspective. Instead of primitive integers, we’ll build natural numbers using the Church encoding.
-
Extensions to Lambda Calculus is where we take our first steps outside the core of lambda calculus and start extending it with primitive booleans and natural numbers. The exercises in this chapter take quite a lot of work, so try to prepare at least a couple of hours for doing them.
By the end of this part, you’ll have built a significant programming language capable of expressing various kinds of computation.
The last exercise in chapter 7 ties everything together with a parser and a REPL.
As an example, here’s how one would define the power function in the sample language:
λ> power = fun n, fun m, rec m 1 (fun pred, fun ih, ih * n)
n => m => rec m 1 (pred => ih => rec ih 0 (pred => ih_ => rec n ih_ (pred => ih__ => S(ih__))))
λ> power 2 8
256For further reading into lambda calculus, see these well-motivated lecture notes Selinger: Lecture Notes on the Lambda Calculus.
The materials in this part are inspired by Programming Language Foundations: STLC chapter and Types and Programming Languages by Benjamin Pierce.