title: Curious OCaml author:

• Lukasz Stafiniak
• Claude Opus 4.5
• GPT-5.2 illustrator: Gemini 3 Nano Banana header-includes:
• |

documentclass: report classoption:

• openany fontsize: 11pt geometry:
• margin=1in toc-depth: 3

{.cover-image}

::: {.illustrator-credit} Illustrated by: Gemini 3 Nano Banana :::

Curious OCaml

Curious OCaml invites you to explore programming through the lens of types, logic, and algebra. OCaml is a language that rewards curiosity—its type system catches errors before your code runs, its functional style encourages clear thinking about data transformations, and its mathematical foundations reveal deep connections between programming and logic. Whether you're new to programming, experienced with OCaml, or a seasoned developer discovering functional programming for the first time, this book aims to spark that "aha!" moment when abstract concepts click into place.

This book is intended for three audiences:

• New to programming: ambitious students in areas with formal rigor -- math, computer science, philosophy, linguistics, etc.
• Intermediate: OCaml programmers.
• Advanced: programmers who are new to functional programming.

Chapter 1: Logic

{.chapter-image}

From logic rules to programming constructs

In this chapter, you will:

• Learn natural-deduction rules for the core connectives ($\top, \bot, \wedge, \vee, \rightarrow$)
• Practice reading and building derivation trees (including hypothetical derivations)
• See the Curry–Howard correspondence emerge in OCaml typing rules
• Connect logical reasoning patterns (cases, induction) to programming patterns (pattern matching, recursion)

Conventions. OCaml code blocks are intended to be runnable unless marked with ocaml skip (used for illustrative or partial snippets).

Throughout this chapter we use natural deduction in the style of intuitionistic (constructive) logic. This choice is not accidental: it is exactly the fragment of logic that lines up with the “pure” core of functional programming via the Curry–Howard correspondence.

1.1 In the Beginning there was Logos

What logical connectives do you know? Before we write any code, let us take a step back and think about logic itself. The connectives listed below form the foundation of reasoning, and as we will discover, they also form the foundation of programming.

How can we define these connectives precisely? The key insight is to think in terms of derivation trees. A derivation tree shows how we arrive at conclusions from premises, building up knowledge step by step:

$$ \frac{ \frac{\frac{,}{\text{a premise}} ; \frac{,}{\text{another premise}}}{\text{some fact}} ; \frac{\frac{,}{\text{this we have by default}}}{\text{another fact}}} {\text{final conclusion}} $$

We define connectives by providing rules for using them. For example, a rule $\frac{a ; b}{c}$ matches parts of the tree that have two premises, represented by variables $a$ and $b$, and have any conclusion, represented by variable $c$. These variables act as placeholders that can match any proposition.

Design principle: When defining a connective, we try to use only that connective in its definition. This keeps definitions self-contained and avoids circular dependencies between connectives.

1.2 Rules for Logical Connectives

Each logical connective comes with two kinds of rules:

Introduction rules tell us how to produce or construct a connective. If you want to prove "A and B", the introduction rule tells you what you need: proofs of both A and B.

Elimination rules tell us how to use or consume a connective. If you already have "A and B", the elimination rules tell you what you can get from it: either A or B (your choice but there is no limit on how many times you decide).

In the table below, text in parentheses provides informal commentary. Letters like $a$, $b$, and $c$ are variables that can stand for any proposition.

Notation for Hypothetical Derivations

The notation $\hyp{[a]^x}{b}$ (sometimes written as a tree) matches any subtree that derives $b$ and can use $a$ as an assumption (marked with label $x$), even though $a$ might not otherwise be warranted. The square brackets around $a$ indicate that this is a hypothetical assumption, not something we have actually established. The superscript $x$ is a label that helps us track which assumption gets "discharged" when we complete the derivation.

This is the key to proving implications: to prove "if A then B", we temporarily assume A and show we can derive B. For example, we can derive "sunny $\rightarrow$ happy" by showing that assuming it is sunny, we can derive happiness:

$$ \frac{\frac{\frac{\frac{\frac{,}{\text{sunny}}^x}{\text{go outdoor}}}{\text{playing}}}{\text{happy}}}{\text{sunny} \rightarrow \text{happy}} \text{ using } x $$

Notice how the assumption "sunny" (marked with $x$) appears at the top of the derivation tree. We use this assumption to derive "go outdoor", then "playing", and finally "happy". Once we complete the derivation, the assumption is discharged: we no longer need to assume it is sunny because we have established the conditional "sunny $\rightarrow$ happy".

A crucial point: such assumptions can only be used within the matched subtree! However, they can be used multiple times within that subtree. For example, if someone's mood is more difficult to influence and requires multiple sunny conditions:

$$ \frac{\frac{ \frac{\frac{\frac{,}{\text{sunny}}^x}{\text{go outdoor}}}{\text{playing}} \quad \frac{\frac{,}{\text{sunny}}^x \quad \frac{\frac{,}{\text{sunny}}^x}{\text{go outdoor}}}{\text{nice view}} }{\text{happy}}}{\text{sunny} \rightarrow \text{happy}} \text{ using } x $$

In this more complex derivation, the assumption "sunny" (labeled $x$) is used three times: once to derive "go outdoor", and twice more in deriving "nice view". All three uses are valid because they occur within the same hypothetical subtree.

Reasoning by Cases

The elimination rule for disjunction deserves special attention because it represents reasoning by cases, one of the most fundamental proof techniques.

Suppose we know "A or B" is true, but we do not know which one. How can we still derive a conclusion C? We must show that C follows regardless of which alternative holds. In other words, we need to prove: (1) assuming A, we can derive C, and (2) assuming B, we can derive C. Since one of A or B must be true, and both lead to C, we can conclude C.

Here is a concrete example: How can we use the fact that it is sunny $\vee$ cloudy (but not rainy)?

$$ \frac{ \frac{,}{\text{sunny} \vee \text{cloudy}}^{\text{forecast}} \quad \frac{\frac{,}{\text{sunny}}^x}{\text{no-umbrella}} \quad \frac{\frac{,}{\text{cloudy}}^y}{\text{no-umbrella}} }{\text{no-umbrella}} \text{ using } x, y $$

We know that it will be sunny or cloudy (by watching the weather forecast). Now we reason by cases: If it will be sunny, we will not need an umbrella. If it will be cloudy, we will not need an umbrella. Since one of these must be the case, and both lead to the same conclusion, we can confidently say: we will not need an umbrella.

Reasoning by Induction

We need one more kind of rule to do serious math: reasoning by induction. This rule is somewhat similar to reasoning by cases, but instead of considering a finite number of alternatives, it allows us to prove properties that hold for infinitely many cases, such as all natural numbers.

Here is the example rule for induction on natural numbers:

$$ \frac{p(0) \quad \hyp{[p(x)]^x}{p(x+1)}}{p(n)} \text{ by induction, using } x $$

This rule says: we get property $p$ for any natural number $n$, provided we can do two things:

1. Base case: Establish $p(0)$, that is, prove the property holds for zero.
2. Inductive step: Show that assuming $p(x)$ holds for some arbitrary $x$, we can derive $p(x+1)$. This assumption $p(x)$ is called the induction hypothesis.

Here $x$ is a unique variable representing an arbitrary natural number. We cannot substitute a particular number for it because we write "using $x$" on the side, indicating that the derivation works for any choice of $x$.

The power of induction lies in this: once we have the base case and the inductive step, we have implicitly covered all natural numbers. Starting from $p(0)$, we can derive $p(1)$, then $p(2)$, then $p(3)$, and so on, reaching any natural number $n$ we wish.

1.3 Logos was Programmed in OCaml

We now arrive at one of the most remarkable discoveries in the foundations of computer science: the Curry–Howard correspondence, also known as "propositions as types" or the "proofs-as-programs" interpretation. In a pure, intuitionistic setting, this correspondence is not just a metaphor: proof rules and typing rules are the same kind of object.

Under this correspondence:

• Propositions (logical statements) correspond to types
• Proofs (derivations showing a proposition is true) correspond to programs (expressions of a given type)
• Introduction rules correspond to constructors (ways to build values)
• Elimination rules correspond to destructors (ways to use values)

When you write a well-typed program, you are (implicitly) constructing a derivation tree that proves a typing judgement.

The following table shows how each logical connective corresponds to a programming construct in OCaml:

For example, the identity function corresponds to the tautology $a \rightarrow a$:

# fun x -> x;;
- : 'a -> 'a = <fun>

Let us now see the precise typing rules for each OCaml construct, presented in the same style as our logical rules:

Typing rules for OCaml constructs:

• Unit (truth): $\frac{}{\texttt{()} : \texttt{unit}}$

  The unit value () always has type unit. This is like $\top$ in logic: we can always produce it without any premises.

• Empty type (falsehood): in OCaml we can define an empty type (a type with no constructors):

  type void = |
  

  There is no way to construct a value of type void using ordinary, terminating code. But if we somehow have a v : void, then we can derive anything from it (falsity elimination):

  let absurd (v : void) : 'a =
    match v with _ -> .
  

  This corresponds closely to the logical rule $\frac{\bot}{a}$.

  OCaml also has effects (notably exceptions). Because raise e never returns normally, the type checker allows it to have any result type: $$ \frac{e : \texttt{exn}}{\texttt{raise } e : a} $$ This is useful in practice, but it is also a good reminder that effects complicate the neat “proofs-as-programs” story.

• Pair (conjunction):

  • Introduction: $\frac{s : a \quad t : b}{(s, t) : a * b}$
  • Elimination: from p : a * b we can extract either component (e.g. by pattern matching, or via fst/snd)

  To construct a pair, you need both components. To use a pair, you can extract either component. This mirrors conjunction perfectly: to prove "A and B", you need proofs of both; given "A and B", you can conclude either A or B.

• Variant (disjunction): first, we define a sum type (a two-way choice):

  type ('a, 'b) either = Left of 'a | Right of 'b
  

  • Introduction: from x : a we get Left x : (a, b) either, and from y : b we get Right y : (a, b) either
  • Elimination: given t : (a, b) either and a branch for each case, produce a result c (pattern matching)

  The shape of the elimination rule is exactly “reasoning by cases”: to use an either, you must handle both Left and Right.

  let either f g = function
    | Left x -> f x
    | Right y -> g y
  

  A built-in example is bool, which you can think of as a two-constructor variant; the if ... then ... else ... expression is just a specialized form of case analysis on a boolean.

  let choose b x y =
    if b then x else y
  
  let choose' b x y =
    match b with
    | true -> x
    | false -> y
  

  To construct a variant, you only need one of the alternatives. To use a variant, you must handle all possible cases (pattern matching). This mirrors disjunction: to prove "A or B", you only need one; to use "A or B", you must consider both possibilities.

• Function (implication):

  • Introduction: $\frac{\hyp{[x : a]}{e : b}}{\texttt{fun}~x \to e : a \to b}$
  • Elimination (application): $\frac{f : a \to b \quad t : a}{f~t : b}$

  To construct a function, you assume you have an input of type $a$ (the parameter $x$) and show how to produce a result of type $b$. To use a function, you apply it to an argument. This mirrors implication: to prove "A implies B", assume A and derive B; given "A implies B" and A, conclude B.

• Recursion (induction): recursion is not a connective, but it matches the shape of induction: in a recursive definition you are allowed to assume the function being defined (the “induction hypothesis”) when defining its body.

  In OCaml, recursion is introduced with let rec (there is no standalone rec expression).

Definitions

Writing out expressions and types repetitively quickly becomes tedious. More importantly, without definitions we cannot give names to our concepts, making code harder to understand and maintain. This is why we need definitions.

Type definitions are written: type ty = some type.

• In OCaml, disjunction-like types are not written as something like a | b directly; instead, you define a variant type and then use its constructors. For example:

  type int_string_choice = A of int | B of string
  

  This allows us to write A x : int_string_choice for any x : int, and B y : int_string_choice for any y : string.

• Why do we need to define variant types? The reasons are: exhaustiveness checks, performance of generated code, and ease of type inference. When OCaml sees A 5, it needs to figure out (or "infer") the type. Without a type definition, how would OCaml know whether this is A of int | B of string or A of int | B of float | C of bool? The definition tells OCaml exactly what variants exist. When you match | A i -> ..., the compiler will warn you if you forgot to also cover C b in your match patterns.

• OCaml does provide an alternative: polymorphic variants, written with a backtick. We can write `A x : [ `A of a | `B of b ]. With ` variants, OCaml does infer what other variants might exist based on usage. These types are powerful and flexible; we will discuss them in chapter 11.

• Tuple elements do not need labels because we always know at which position a tuple element stands: the first element is first, the second is second, and so on. However, having labels makes code much clearer, especially when tuples have many components or components of the same type. For this reason, we can define a record type:

  type int_string_record = { a : int; b : string }
  

  and create its values: {a = 7; b = "Mary"}. OCaml 5.4 and newer also support labeled tuples, we will not discuss these.

• We access the fields of records using the dot notation: {a = 7; b = "Mary"}.b = "Mary". Unlike tuples where you must remember "the second element is the name", with records you can write .b to get the field named b.

Expression Definitions

In many presentations of the Curry–Howard correspondence (and in programming language theory), recursion is introduced via a standalone operator often called fix. OCaml does not have a standalone fix expression: recursion is introduced only as part of a let rec definition.

This brings us to expression definitions, which let us give names to values. The typing rules for definitions are a bit more complex than what we have seen so far:

$$ \frac{e_1 : a \quad \hyp{[x : a]}{e_2 : b}}{\texttt{let } x = e_1 \texttt{ in } e_2 : b} $$

This rule says: if $e_1$ has type $a$, and assuming $x$ has type $a$ we can show that $e_2$ has type $b$, then the whole let expression has type $b$. Interestingly, this rule is equivalent to introducing a function and immediately applying it: let x = e1 in e2 behaves the same as (fun x -> e2) e1. This equivalence reflects a deep connection in the Curry–Howard correspondence.

For recursive definitions, we need an additional rule:

$$ \frac{\hyp{[x : a]}{e_1 : a} \quad \hyp{[x : a]}{e_2 : b}}{\texttt{let rec } x = e_1 \texttt{ in } e_2 : b} $$

Notice the crucial difference: in the recursive case, $x$ can appear in $e_1$ itself! This is what allows functions to call themselves. The name $x$ is visible both in its own definition ($e_1$) and in the body that uses the definition ($e_2$).

These rules are slightly simplified. The full rules involve a concept called polymorphism, which we will cover in a later chapter. Polymorphism explains how the same function can work with different types.

Scoping Rules

Understanding scope—where names are visible—is essential for reading and writing OCaml programs.

• Type definitions we have seen above are global: they need to be at the top-level (not nested in expressions), and they extend from the point they occur till the end of the source file or interactive session. You cannot define a type inside a function.

• let-in definitions for expressions: let x = e1 in e2 are local—the name $x$ is only visible within $e_2$. Once you exit the in part, $x$ no longer exists. This is useful for temporary values that should not pollute the global namespace.

• let definitions without in are global: placing let x = e1 at the top-level makes $x$ visible from after $e_1$ till the end of the source file or interactive session. This is how you define functions and values that the rest of your program can use.

• In the interactive session (toplevel/REPL), we mark the end of a top-level "sentence" with ;;. This tells OCaml "I am done typing, please evaluate this." In source files compiled by the build system, ;; is unnecessary because the end of each definition is clear from context.

Operators

Operators like +, *, <, = are simply names of functions. In OCaml, there is nothing magical about operators; they are ordinary functions that happen to have special characters in their names and can be used in infix position (between their arguments).

Just like other names, you can define your own operators:

# let (+:) a b = String.concat "" [a; b];;
val ( +: ) : string -> string -> string = <fun>
# "Alpha" +: "Beta";;
- : string = "AlphaBeta"

Notice the asymmetry here: when defining an operator, we wrap it in parentheses to tell OCaml "this is the name I am defining". When using the operator, we write it in the normal infix position between its arguments. This asymmetry exists because the definition syntax needs to distinguish between "the name +:" and "the expression a +: b".

An important feature of OCaml is that operators are not overloaded. This means that a single operator cannot work for multiple types. Each type needs its own set of operators:

• +, *, / work for integers
• +., *., /. work for floating point numbers

This design choice makes type inference simpler and more predictable. When you see x + y, OCaml knows immediately that x and y must be integers.

Exception: The comparison operators <, =, <=, >=, <> do work for all values other than functions. These are called polymorphic comparisons.

1.4 Exercises

The following exercises are adapted from Think OCaml: How to Think Like a Computer Scientist by Nicholas Monje and Allen Downey. They will help you get comfortable with OCaml's syntax and type system.

Exercise 1: Type and Value Predictions

Assume that we execute the following assignment statements:

let width = 17
let height = 12.0
let delimiter = '.'

For each of the following expressions, write the value of the expression and the type (of the value of the expression), or the resulting type error.

1. width/2
2. width/.2.0
3. height/3
4. 1 + 2 * 5
5. delimiter * 5

Exercise 2: REPL Calculator Drills

Practice using the OCaml interpreter as a calculator:

1. The volume of a sphere with radius $r$ is $\frac{4}{3} \pi r^3$. What is the volume of a sphere with radius 5? (Hint: 392.6 is wrong!)
2. Suppose the cover price of a book is $24.95, but bookstores get a 40% discount. Shipping costs $3 for the first copy and 75 cents for each additional copy. What is the total wholesale cost for 60 copies?
3. If I leave my house at 6:52 am and run 1 mile at an easy pace (8:15 per mile), then 3 miles at tempo (7:12 per mile) and 1 mile at easy pace again, what time do I get home for breakfast?

Exercise 3: Recursive Fibonacci

You've probably heard of the Fibonacci numbers before, but in case you haven't, they're defined by the following recursive relationship:

$$ \begin{cases} f(0) = 0 \ f(1) = 1 \ f(n+1) = f(n) + f(n-1) & \text{for } n = 2, 3, \ldots \end{cases} $$

Write a recursive function to calculate these numbers.

Exercise 4: Recursive Palindromes

A palindrome is a word that is spelled the same backward and forward, like "noon" and "redivider". Recursively, a word is a palindrome if the first and last letters are the same and the middle is a palindrome.

The following are functions that take a string argument and return the first, last, and middle letters:

let first_char word = word.[0]
let last_char word =
  let len = String.length word - 1 in
  word.[len]
let middle word =
  let len = String.length word - 2 in
  String.sub word 1 len

1. Enter these functions into the toplevel and test them out. What happens if you call middle with a string with two letters? One letter? What about the empty string ""?
2. Write a function called is_palindrome that takes a string argument and returns true if it is a palindrome and false otherwise.

Exercise 5: Euclid's GCD

The greatest common divisor (GCD) of $a$ and $b$ is the largest number that divides both of them with no remainder.

One way to find the GCD of two numbers is Euclid's algorithm, which is based on the observation that if $r$ is the remainder when $a$ is divided by $b$, then $\gcd(a, b) = \gcd(b, r)$. As a base case, we can consider $\gcd(a, 0) = a$.

Write a function called gcd that takes parameters a and b and returns their greatest common divisor.

If you need help, see http://en.wikipedia.org/wiki/Euclidean_algorithm.

Chapter 2: Algebra

{.chapter-image}

Algebraic data types and some curious analogies

In this chapter, we will deepen our understanding of OCaml's type system by working through type inference examples by hand. Then we will explore algebraic data types---a cornerstone of functional programming that allows us to define rich, structured data. Along the way, we will discover a surprising and beautiful connection between these types and ordinary polynomials from high-school algebra.

In this chapter, you will:

• Practice type inference by hand (constraints, unification intuition)
• Define and manipulate algebraic data types (variants, records, recursion, parameters)
• Interpret types as polynomials (and learn what this analogy buys you)
• Differentiate types to compute “one-hole contexts” (derivatives of data structures)

2.1 A Glimpse at Type Inference

For a refresher, let us apply the type inference rules introduced in Chapter 1 to some simple examples. We will start with the identity function fun x -> x---perhaps the simplest possible function, yet one that reveals important aspects of polymorphism. In the derivations below, $[?]$ means “unknown (to be inferred)”.

We begin with an incomplete derivation:

$$ \frac{[?]}{\texttt{fun x -> x} : [?]} $$

Using the $\rightarrow$ introduction rule, we need to derive the body x assuming x has some type $a$:

$$ \frac{\hyp{[x : a]^x}{\texttt{x} : a}}{\texttt{fun x -> x} : [?] \rightarrow [?]} $$

The premise is a hypothetical derivation: inside the body we are allowed to use the assumption x : a. Since the body is just x, the result type is also $a$, and we conclude:

$$ \frac{\hyp{[x : a]^x}{\texttt{x} : a}}{\texttt{fun x -> x} : a \rightarrow a} $$

Because $a$ is arbitrary (we made no assumptions constraining it), OCaml introduces a type variable 'a to represent it. This is how polymorphism emerges naturally from the inference process---the identity function can work with values of any type:

# fun x -> x;;
- : 'a -> 'a = <fun>

A More Complex Example

Now let us try something that will constrain the types more: fun x -> x+1. This is the same as fun x -> ((+) x) 1 (try it in OCaml to verify!). The addition operator forces specific types upon us.

We will use the notation $[?\alpha]$ to mean "type unknown yet, but the same as in other places marked $[?\alpha]$." This notation helps us track how constraints propagate through the derivation.

Starting the derivation and applying $\rightarrow$ introduction:

$$ \frac{\frac{[?]}{\texttt{((+) x) 1} : [?\alpha]}}{\texttt{fun x -> ((+) x) 1} : [?] \rightarrow [?\alpha]} $$

Applying $\rightarrow$ elimination (function application) to ((+) x) 1:

$$ \frac{\frac{\frac{[?]}{\texttt{(+) x} : [?\beta] \rightarrow [?\alpha]} \quad \frac{[?]}{\texttt{1} : [?\beta]}}{\texttt{((+) x) 1} : [?\alpha]}}{\texttt{fun x -> ((+) x) 1} : [?] \rightarrow [?\alpha]} $$

We know that 1 : int, so $[?\beta] = \texttt{int}$:

$$ \frac{\frac{\frac{[?]}{\texttt{(+) x} : \texttt{int} \rightarrow [?\alpha]} \quad \frac{,}{\texttt{1} : \texttt{int}}^{\text{(constant)}}}{\texttt{((+) x) 1} : [?\alpha]}}{\texttt{fun x -> ((+) x) 1} : [?] \rightarrow [?\alpha]} $$

Applying function application again to (+) x:

$$ \frac{\frac{\frac{\frac{[?]}{\texttt{(+)} : [?\gamma] \rightarrow \texttt{int} \rightarrow [?\alpha]} \quad \frac{[?]}{\texttt{x} : [?\gamma]}}{\texttt{(+) x} : \texttt{int} \rightarrow [?\alpha]} \quad \frac{,}{\texttt{1} : \texttt{int}}^{\text{(constant)}}}{\texttt{((+) x) 1} : [?\alpha]}}{\texttt{fun x -> ((+) x) 1} : [?\gamma] \rightarrow [?\alpha]} $$

Since (+) : int -> int -> int, we have $[?\gamma] = \texttt{int}$ and $[?\alpha] = \texttt{int}$:

$$ \frac{\frac{\frac{\frac{,}{\texttt{(+)} : \texttt{int} \rightarrow \texttt{int} \rightarrow \texttt{int}}^{\text{(constant)}} \quad \frac{,}{\texttt{x} : \texttt{int}}^x}{\texttt{(+) x} : \texttt{int} \rightarrow \texttt{int}} \quad \frac{,}{\texttt{1} : \texttt{int}}^{\text{(constant)}}}{\texttt{((+) x) 1} : \texttt{int}}}{\texttt{fun x -> ((+) x) 1} : \texttt{int} \rightarrow \texttt{int}} $$

Curried Form

When there are several arrows "on the same depth" in a function type, it means that the function returns a function. For example, (+) : int -> int -> int is just a shorthand for (+) : int -> (int -> int). The arrow associates to the right, so we can omit the parentheses.

This is very different from:

$$ \texttt{fun f -> (f 1) + 1} : (\texttt{int} \rightarrow \texttt{int}) \rightarrow \texttt{int} $$

In the first case, (+) is a function that takes an integer and returns a function from integers to integers. In the second case, we have a function that takes a function as an argument---a higher-order function. The parentheses around int -> int are essential here; without them, the meaning would be completely different.

This style of defining multi-argument functions, where each function takes one argument and returns another function expecting the remaining arguments, is called curried form (named after logician Haskell Curry). It enables a powerful technique called partial application.

For example, instead of writing (fun x -> x+1), we can simply write ((+) 1). Here we apply (+) to just one argument, getting back a function that adds 1 to its input. What expanded form does ((+) 1) correspond to exactly (computationally)?

Think about it before reading on...

It corresponds to fun y -> 1 + y. We have "baked in" the first argument, and the resulting function waits for the second.

We will become more familiar with functions returning functions when we study the lambda calculus in a later chapter.

2.2 Algebraic Data Types

In Chapter 1, we learned about the unit type and variant types like:

type int_string_choice = A of int | B of string

We also covered tuple types, record types, and type definitions. Now let us explore these concepts more deeply, building up to the powerful notion of algebraic data types.

Variants Without Arguments

Variants do not have to carry arguments. Instead of writing A of unit, we can simply use A. This is more convenient and idiomatic:

type color = Red | Green | Blue

This defines a type with exactly three possible values---no more, no less. The compiler knows this, which enables exhaustive pattern matching checks.

A subtle point about OCaml: In OCaml, variants take multiple arguments rather than taking tuples as arguments. This means A of int * string is different from A of (int * string). The first takes two separate arguments, while the second takes a single tuple argument. This distinction is usually not important---until you get bitten by it in some corner case! For most purposes, you can ignore it.

Recursive Type Definitions

Here is where things get really interesting: type definitions can be recursive! This allows us to define data structures of arbitrary size using a finite definition:

type int_list = Empty | Cons of int * int_list

Let us see what values inhabit int_list. The definition tells us there are two ways to build an int_list:

• Empty represents the empty list---a list with no elements
• Cons (5, Empty) is a list containing just 5
• Cons (5, Cons (7, Cons (13, Empty))) is a list containing 5, 7, and 13.

Notice how Cons takes an integer and another int_list, allowing us to chain together as many elements as we like. This recursive structure is the essence of how functional languages represent unbounded data.

The built-in type bool really does behave like a two-constructor variant with values true and false---but note a small OCaml wrinkle: user-defined constructors must start with a capital letter, while a few built-in constructors like true, false, [], and (::) are special-cased.

Similarly, int can be thought of as a very large finite variant (“one constructor per integer”), even though the compiler implements it as an efficient machine integer rather than as a gigantic sum type.

Parametric Type Definitions

Our int_list type only works with integers. But what if we want a list of strings? Or a list of booleans? We would have to define separate types for each, duplicating the same structure.

Type definitions can be parametric with respect to the types of their components. This allows us to define generic data structures that work with any element type. OCaml already has a built-in parametric list type, so to avoid shadowing it we will define our own simplified list type:

type 'a my_list = Empty | Cons of 'a * 'a my_list

The 'a is a type parameter---a placeholder that gets filled in when we use the type. We can have a string my_list, an int my_list, or even an (int my_list) my_list (a list of lists of integers).

Several conventions and syntax rules apply to parametric types:

• Type variables must start with '. When printing inferred types, OCaml may rename these variables, so it is customary to stick to the standard names 'a, 'b, 'c, 'd, etc.

• The OCaml syntax places the type parameter before the type name, mimicking English word order. A silly example that reads almost like English:

  type 'white_color dog = Dog of 'white_color
  

  This defines a "white-color dog" type---the syntax reads naturally!

• With multiple parameters, OCaml uses parentheses:

  type ('a, 'b) choice = Left of 'a | Right of 'b
  

  Compare this to F# syntax: type choice<'a,'b> = Left of 'a | Right of 'b

  And Haskell syntax: data Choice a b = Left a | Right b

  Different languages have different conventions, but the underlying concept is the same.

2.3 Syntactic Bread and Sugar

OCaml provides various syntactic conveniences---sometimes called syntactic sugar---that make code more pleasant to write and read. Let us survey the most important ones.

Constructor Naming

Names of variants, called constructors, must start with a capital letter. If we wanted to define our own booleans, we would write:

type my_bool = True | False

Only constructors and module names can start with capital letters in OCaml. Everything else (values, functions, type names) must start with a lowercase letter. This convention makes it easy to distinguish constructors at a glance.

(As noted above, a few built-in constructors like true, false, [], and (::) are special exceptions to the capitalization rule.)

Modules are organizational units (like "shelves") containing related values. For example, the List module provides operations on lists, including List.map and List.filter. We will learn more about modules in later chapters.

Accessing Record Fields

Did we mention that we can use dot notation to access record fields? The syntax record.field extracts a field value. For example, if we have let person = {name="Alice"; age=30}, we can write person.name to get "Alice".

Function Definition Shortcuts

Several syntactic shortcuts make function definitions more concise. These are worth memorizing, as you will see them constantly in OCaml code:

• fun x y -> e stands for fun x -> fun y -> e. Note that fun x -> fun y -> e parses as fun x -> (fun y -> e). This shorthand aligns with curried form---we can write multi-argument functions without nesting fun expressions.

• function A x -> e1 | B y -> e2 stands for fun p -> match p with A x -> e1 | B y -> e2. The general form is: function PATTERN-MATCHING stands for fun v -> match v with PATTERN-MATCHING. This is handy when you want to immediately pattern-match on a function's argument.

• let f ARGS = e is a shorthand for let f = fun ARGS -> e. This is probably the most common way to define functions in practice.

2.4 Pattern Matching

Pattern matching is one of the most powerful features of OCaml and similar languages. It lets us examine the structure of data and extract components in a single, elegant construct.

Recall that we introduced fst and snd as means to access elements of a pair. But what about larger tuples? There is no built-in thd for the third element. The fundamental way to access any tuple---or any algebraic data type---uses the match construct. In fact, fst and snd can easily be defined using pattern matching:

let fst p = match p with (a, b) -> a
let snd p = match p with (a, b) -> b

The pattern (a, b) destructures the pair, binding its first component to a and its second to b. We then return whichever component we want.

Matching on Records

Pattern matching also works with records, letting us extract multiple fields at once:

type person = { name : string; surname : string; age : int }

let greet_person () =
  match { name = "Walker"; surname = "Johnnie"; age = 207 } with
  | { name = _; surname = sn; age = _ } -> "Hi " ^ sn ^ "!"

Here we match against a record pattern. Note that we use wildcards _ for name and age (ignoring them), while binding surname to sn---then use sn in the greeting.

Understanding Patterns

The left-hand sides of -> in match expressions are called patterns. Patterns describe the structure of values we want to match against. They can include:

• Constants (like 1, "hello", or true)
• Variables (which bind to the matched value)
• Constructors (like None, Some x, or Cons (h, t))
• Tuples and records
• Nested combinations of all the above

Patterns can be nested to arbitrary depth, allowing us to match complex structures in one go:

match Some (5, 7) with
| None -> "sum: nothing"
| Some (x, y) -> "sum: " ^ string_of_int (x + y)

Here Some (x, y) is a nested pattern: we match Some of something, and that something must be a pair, whose components we bind to x and y.

Simple Patterns and Wildcards

A pattern can simply bind the entire value without destructuring. Writing match f x with v -> ... is the same as let v = f x in .... This is occasionally useful when you want the syntax of match but do not need to take the value apart.

When we do not need a value in a pattern, it is good practice to use the underscore _, which is a wildcard. The wildcard matches anything but does not bind it to a name. This signals to the reader (and the compiler) that we are intentionally ignoring that part:

let fst (a, _) = a
let snd (_, b) = b

Using _ instead of an unused variable name avoids compiler warnings about unused bindings.

Pattern Linearity

A variable can only appear once in a pattern. This property is called linearity. You might think this is a limitation---what if we want to check that two parts of a structure are equal? We cannot write (x, x) to match pairs with equal components.

However, we can add conditions to patterns using when, so linearity is not really a limitation in practice:

let describe_point p =
  match p with
  | (x, y) when x = y -> "diag"
  | _ -> "off-diag"

The when clause acts as a guard: the pattern matches only if both the structure matches and the condition is true.

Here is a more elaborate example showing how to implement a comparison function (without shadowing the standard compare):

let compare_int a b =
  match a, b with
  | (x, y) when x < y -> -1
  | (x, y) when x = y -> 0
  | _ -> 1

Notice how we match against the tuple (a, b) in different ways, using guards to distinguish the cases.

Partial Record Patterns

We can skip unused fields of a record in a pattern. Only the fields we care about need to be mentioned. This keeps patterns concise and means we do not have to update every pattern when we add a new field to a record type.

Or-Patterns

We can compress patterns by using | inside a single pattern to match multiple alternatives. This is different from having multiple pattern clauses---it lets us share a single right-hand side for several patterns:

type month =
  | Jan | Feb | Mar | Apr | May | Jun
  | Jul | Aug | Sep | Oct | Nov | Dec

type weekday = Mon | Tue | Wed | Thu | Fri | Sat | Sun

type calendar_date =
  { year : int; month : month; day : int; weekday : weekday }

let day =
  { year = 2012; month = Feb; day = 14; weekday = Wed }

let day_kind =
  match day with
  | { weekday = Sat | Sun; _ } -> "Weekend!"
  | _ -> "Work day"

The pattern Sat | Sun matches either Sat or Sun. This is much cleaner than writing two separate clauses with the same right-hand side.

Named Patterns with as

Sometimes we want to both destructure a value and keep a reference to the whole thing (or some intermediate part). We use (pattern as v) to name a nested pattern, binding the matched value to v:

match day with
  | {weekday = (Mon | Tue | Wed | Thu | Fri as wday); _}
      when not (day.month = Dec && day.day = 24) ->
    Some (work (get_plan wday))
  | _ -> None

This example demonstrates several features working together:

• An or-pattern matches any weekday from Monday to Friday
• The as wday clause binds the matched weekday to the variable wday
• A when guard checks that it is not Christmas Eve
• The bound variable wday is then used in the expression get_plan wday

This combination of features makes OCaml's pattern matching remarkably expressive.

2.5 Interpreting Algebraic Data Types as Polynomials

Now we come to one of the most delightful aspects of algebraic data types: they really are algebraic in a precise mathematical sense. Let us explore a curious analogy between types and polynomials that turns out to be surprisingly deep.

The translation from types to mathematical expressions works as follows:

• Replace | (variant choice) with $+$ (addition)
• Replace * (tuple product) with $\times$ (multiplication)
• Treat record types as tuple types (erasing field names and translating ; as $\times$)

We also need translations for some special types:

• The void type (a type with no constructors, hence no values):

  type void = |
  

  Since no values can be constructed, it represents emptiness---translate it as $0$.

• The unit type has exactly one value, so translate it as $1$. Since variants without arguments behave like variants of unit, translate them as $1$ as well.

• The bool type has exactly two values (true and false), so translate it as $2$.

• Types like int, string, float, and type parameters are treated as variables. We do not care about their exact number of values; we just give them symbolic names like $x$, $y$, etc.

• Defined types translate according to their definitions (substituting variables as necessary).

Give a name to the type being defined (representing a function of the introduced variables). Now interpret the result as an ordinary numeric polynomial! (Or a "rational function" if recursively defined.)

This might seem like a mere curiosity, but it leads to real insights. Let us have some fun with it!

Example: Date Type

type ymd = { year : int; month : int; day : int }

A simple “year-month-day” record is a product of three int fields. Translating to a polynomial (using $x$ for int):

$$D = x \times x \times x = x^3$$

The cube makes sense: this record is essentially a triple of integers.

Example: Option Type

The built-in option type is defined as:

type 'a option = None | Some of 'a

Translating (using $x$ for the type parameter 'a):

$$O = 1 + x$$

This reads as: an option is either nothing (1) or something of type $x$. The polynomial $1 + x$ is beautifully simple!

Example: List Type

type 'a my_list = Empty | Cons of 'a * 'a my_list

Translating (where $L$ represents the list type itself, and $x$ represents the element type):

$$L = 1 + x \cdot L$$

This is a recursive equation! A list is either empty ($1$) or an element times another list ($x \cdot L$). If you solve this equation algebraically, you get $L = \frac{1}{1-x} = 1 + x + x^2 + x^3 + \ldots$, which corresponds to: a list is either empty, or has one element, or has two elements, etc.

Example: Binary Tree Type

type btree = Tip | Node of int * btree * btree

Translating:

$$T = 1 + x \cdot T \cdot T = 1 + x \cdot T^2$$

A binary tree is either a tip ($1$) or a node containing a value and two subtrees ($x \cdot T^2$).

Type Isomorphisms

Here is the remarkable payoff: when translations of two types are equal according to the laws of high-school algebra, the types are isomorphic. This means there exist bijective (one-to-one and onto) functions between them---you can convert from one type to the other and back without losing any information.

Let us play with the binary tree polynomial and see where algebra takes us:

$$ \begin{aligned} T &= 1 + x \cdot T^2 \ &= 1 + x \cdot T + x^2 \cdot T^3 \ &= 1 + x + x^2 \cdot T^2 + x^2 \cdot T^3 \ &= 1 + x + x^2 \cdot T^2 \cdot (1 + T) \ &= 1 + x \cdot (1 + x \cdot T^2 \cdot (1 + T)) \end{aligned} $$

Each step uses standard algebraic manipulations: substituting $T = 1 + xT^2$, expanding, factoring, and rearranging. The result is a different but algebraically equivalent expression.

Now let us translate this resulting expression back to a type:

type repr =
  (int * (int * btree * btree * btree option) option) option

Reading the polynomial $1 + x \cdot (1 + x \cdot T^2 \cdot (1 + T))$ from outside in: we have an option (the outermost $1 + \ldots$), whose Some case contains an int times another option, and so on.

The challenge is to find isomorphism functions with signatures:

val iso1 : btree -> repr
val iso2 : repr -> btree

These functions should satisfy: for all trees t, iso2 (iso1 t) = t, and for all representations r, iso1 (iso2 r) = r. Can you write them?

My First (Failed) Attempt

Here is my first attempt, trying to guess the pattern directly:

# let iso1 (t : btree) : repr =
  match t with
    | Tip -> None
    | Node (x, Tip, Tip) -> Some (x, None)
    | Node (x, Node (y, t1, t2), Tip) ->
      Some (x, Some (y, t1, t2, None))
    | Node (x, Node (y, t1, t2), t3) ->
      Some (x, Some (y, t1, t2, Some t3));;

Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
Node (_, Tip, Node (_, _, _))

I forgot about one case! The case Node (_, Tip, Node (_, _, _))---a node with an empty left subtree and non-empty right subtree---was not covered. It seems difficult to guess the solution directly when trying to map the complex final form all at once.

Have you found it on your first try? If so, congratulations! Most people do not. This illustrates an important principle: complex transformations are easier to get right when broken into smaller steps.

Breaking Down the Problem

Let us divide the task into smaller steps corresponding to intermediate points in the polynomial transformation. Instead of jumping from $T = 1 + xT^2$ directly to the final form, we will introduce intermediate types for each algebraic step:

type ('a, 'b) choice = Left of 'a | Right of 'b

type interm1 =
  ((int * btree, int * int * btree * btree * btree) choice)
  option

type interm2 =
  ((int, int * int * btree * btree * btree option) choice)
  option

Now we can define each step:

let step1r (t : btree) : interm1 =
  match t with
    | Tip -> None
    | Node (x, t1, Tip) -> Some (Left (x, t1))
    | Node (x, t1, Node (y, t2, t3)) ->
      Some (Right (x, y, t1, t2, t3))

let step2r (r : interm1) : interm2 =
  match r with
    | None -> None
    | Some (Left (x, Tip)) -> Some (Left x)
    | Some (Left (x, Node (y, t1, t2))) ->
      Some (Right (x, y, t1, t2, None))
    | Some (Right (x, y, t1, t2, t3)) ->
      Some (Right (x, y, t1, t2, Some t3))

let step3r (r : interm2) : repr =
  match r with
    | None -> None
    | Some (Left x) -> Some (x, None)
    | Some (Right (x, y, t1, t2, t3opt)) ->
      Some (x, Some (y, t1, t2, t3opt))

let iso1 (t : btree) : repr =
  step3r (step2r (step1r t))

Each step function handles one small transformation, and the compiler verifies that our pattern matching is exhaustive. No more missed cases!

Exercise

Define step1l, step2l, step3l, and iso2.

Hint: Now it is straightforward---each step is simply the inverse of its corresponding forward step. The left-going functions undo what the right-going functions do.

Take-Home Lessons

This exploration of type isomorphisms teaches us two valuable principles:

1. Design for validity: Try to define data structures so that only meaningful information can be represented---as long as it does not overcomplicate the data structures. Avoid catch-all clauses when defining functions. The compiler will then tell you if you have forgotten about a case. The exhaustiveness checker is your friend.

2. Divide and conquer: Break solutions into small steps so that each step can be easily understood and verified. When I tried to write iso1 directly, I made a mistake. When I broke it into three simple steps, each step was obviously correct, and composing them gave the right answer.

2.6 Differentiating Algebraic Data Types

Of course, you might object that the pompous title is wrong---we will differentiate the translated polynomials, not the types themselves. Fair enough! But what sense does differentiating a type's polynomial make?

It turns out that taking the partial derivative of a polynomial (translated from a data type), when translated back, gives a type representing a "one-hole context"---a data structure with one piece missing. This missing piece corresponds to the variable with respect to which we differentiated. The derivative tells us: "Here are all the ways to point at one element of this type."

Example: Differentiating a Simple Record

Let us start with a simple record type:

type ymd = { year : int; month : int; day : int }

The translation and its derivative:

$$ \begin{aligned} D &= x \cdot x \cdot x = x^3 \ \frac{\partial D}{\partial x} &= 3x^2 = x \cdot x + x \cdot x + x \cdot x \end{aligned} $$

We could have left it as $3 \cdot x \cdot x$, but expanding it as a sum shows the structure more clearly. The derivative $3x^2$ says: there are three ways to "point at" an int in a ymd, and each way leaves two other ints behind.

Translating the expanded form back to a type:

type ymd_ctx =
  Year of int * int | Month of int * int | Day of int * int

Each variant represents a "hole" at a different position:

• Year (m, d) means the year field is the hole (and we have the month m and day d)
• Month (y, d) means the month field is the hole (and we have year y and day d)
• Day (y, m) means the day field is the hole.

Now we can define functions to introduce and eliminate this derivative type:

let ymd_deriv ({ year = y; month = m; day = d } : ymd) =
  [ Year (m, d); Month (y, d); Day (y, m) ]

let ymd_integr n = function
  | Year (m, d) -> { year = n; month = m; day = d }
  | Month (y, d) -> { year = y; month = n; day = d }
  | Day (y, m) -> { year = y; month = m; day = n }

let example =
  List.map (ymd_integr 7) (ymd_deriv { year = 2012; month = 2; day = 14 })

The ymd_deriv function produces all contexts (one for each field)---it "differentiates" a record into a list of one-hole contexts. The ymd_integr function fills in a hole with a new value---it "integrates" by putting a value back into the context. Notice how the naming follows the calculus analogy!

The example above takes the date February 14, 2012, produces three contexts (one for each field), and then fills each hole with the number 7, producing three modified dates.

Example: Differentiating Binary Trees

Now let us tackle the more challenging case of binary trees (using the same btree type as above):

type btree = Tip | Node of int * btree * btree

The translation and differentiation:

$$ \begin{aligned} T &= 1 + x \cdot T^2 \ \frac{\partial T}{\partial x} &= 0 + T^2 + 2 \cdot x \cdot T \cdot \frac{\partial T}{\partial x} = T \cdot T + 2 \cdot x \cdot T \cdot \frac{\partial T}{\partial x} \end{aligned} $$

Something interesting happened: the derivative is recursive! It refers to itself via $\frac{\partial T}{\partial x}$. This makes perfect sense when you think about it:

• $T \cdot T$ represents pointing at the root: the hole is at the current node, and we have the two subtrees.
• $2 \cdot x \cdot T \cdot \frac{\partial T}{\partial x}$ represents pointing deeper in the tree: we choose left or right (the factor of 2), remember the current node's value ($x$), keep the other subtree ($T$), and then have a context in the chosen subtree ($\frac{\partial T}{\partial x}$).

Instead of translating $2$ as bool, we introduce a more descriptive type to make the code clearer:

type btree_dir = LeftBranch | RightBranch

type btree_deriv =
  | Here of btree * btree
  | Below of btree_dir * int * btree * btree_deriv

The Here constructor means the hole is at the current position, and we have the left and right subtrees. The Below constructor means we go down one level, remembering which direction we went, the value at the node we passed, and the subtree we did not enter.

(You might someday hear about zippers---they are "inverted" relative to our type. In a zipper, the hole comes first, and the context trails behind. Both representations are useful in different situations.)

Exercise

Write a function that takes a number and a btree_deriv, and builds a btree by putting the number into the "hole" in btree_deriv.

let rec btree_integr n = function
  | Here (ltree, rtree) -> Node (n, ltree, rtree)
  | Below (LeftBranch, m, rtree, deriv) ->
    Node (m, btree_integr n deriv, rtree)
  | Below (RightBranch, m, ltree, deriv) ->
    Node (m, ltree, btree_integr n deriv)

2.7 Exercises

Exercise 1: Designing Valid Data Structures

Due to Yaron Minsky.

This exercise practices the principle of "making invalid states unrepresentable." Consider a datatype to store internet connection information. The time when_initiated marks the start of connecting and is not needed after the connection is established (it is only used to decide whether to give up trying to connect). The ping information is available for established connections but not straight away.

type connectionstate = Connecting | Connected | Disconnected

type connectioninfo = {
  state : connectionstate;
  server : Inetaddr.t;
  lastpingtime : Time.t option;
  lastpingid : int option;
  sessionid : string option;
  wheninitiated : Time.t option;
  whendisconnected : Time.t option;
}

(The types Time.t and Inetaddr.t come from the Core library. You can replace them with float and Unix.inet_addr. Load the Unix library in the interactive toplevel with #load "unix.cma";;.)

The problem with this design is that it allows many nonsensical combinations: a Connecting state with ping information, a Disconnected state with a session ID, etc. The optional fields (all those option types) make it unclear which fields are valid in which states.

Rewrite the type definitions so that the datatype will contain only reasonable combinations of information. Use separate record types for each connection state, with only the fields that make sense for that state.

Exercise 2: Labeled and Optional Arguments

In OCaml, functions can have labeled arguments and optional arguments (parameters with default values that can be omitted). This exercise explores these features.

Labels can differ from the names of argument values:

let f ~meaningfulname:n = n + 1
let _ = f ~meaningfulname:5  (* We do not need the result so we ignore it. *)

When the label and value names are the same, the syntax is shorter:

let g ~pos ~len =
  StringLabels.sub "0123456789abcdefghijklmnopqrstuvwxyz" ~pos ~len

let () =  (* A nicer way to mark computations that return unit. *)
  let pos = Random.int 26 in
  let len = Random.int 10 in
  print_string (g ~pos ~len)

When some function arguments are optional, the function must take non-optional arguments after the last optional argument. Optional parameters with default values:

let h ?(len=1) pos = g ~pos ~len
let () = print_string (h 10)

Optional arguments are implemented as parameters of an option type. This allows checking whether the argument was provided:

let foo ?bar n =
  match bar with
    | None -> "Argument = " ^ string_of_int n
    | Some m -> "Sum = " ^ string_of_int (m + n)

We can use it in various ways:

let _ = foo 5
let _ = foo ~bar:5 7

We can also provide the option value directly:

let test_foo () =
  let bar = if Random.int 10 < 5 then None else Some 7 in
  foo ?bar 7

1. Observe the types that functions with labeled and optional arguments have. Come up with coding style guidelines for when to use labeled arguments. When might they improve readability? When might they be overkill?

2. Write a rectangle-drawing procedure that takes three optional arguments: left-upper corner, right-lower corner, and a width-height pair. It should draw a correct rectangle whenever two of the three arguments are given (since any two determine the third), and raise an exception otherwise. Use the Bogue library.

3. Write a function that takes an optional argument of arbitrary type and a function argument, and passes the optional argument to the function without inspecting it. This tests your understanding of how optional arguments work at the type level.

Exercise 3: Type Inference Practice

From a past exam.

These exercises help you internalize how type inference works. Try to work them out by hand before checking with the OCaml toplevel.

1. Give the (most general) types of the following expressions, either by guessing or by inferring by hand:

   1. let double f y = f (f y) in fun g x -> double (g x)
   2. let rec tails l = match l with [] -> [] | x::xs -> xs::tails xs in fun l -> List.combine l (tails l)

2. Give example expressions that have the following types (without using type constraints). There are many possible answers for each:

   1. (int -> int) -> bool
   2. 'a option -> 'a list

Exercise 4: Types as Exponents

We have seen that algebraic data types can be related to analytic functions (the subset definable from polynomials via recursion)---by literally interpreting sum types (variant types) as sums and product types (tuple and record types) as products. We can extend this interpretation to function types by interpreting $a \rightarrow b$ as $b^a$ (i.e., $b$ to the power of $a$). Note that the $b^a$ notation is actually used to denote functions in set theory.

This interpretation makes sense: a function from a set with $a$ elements to a set with $b$ elements is choosing, for each of the $a$ inputs, one of $b$ outputs---giving $b^a$ possible functions.

1. Translate $a^{b + cd}$ and $a^b \cdot (a^c)^d$ into OCaml types, using any distinct types for $a, b, c, d$, and using type ('a,'b) choice = Left of 'a | Right of 'b for $+$. Write the bijection functions in both directions. Verify algebraically that $a^{b + cd} = a^b \cdot (a^c)^d$ using the laws of exponents.

2. Come up with a type 't exp that shares with the exponential function the following property: $\frac{\partial \exp(t)}{\partial t} = \exp(t)$, where we translate a derivative of a type as a context (i.e., the type with a "hole"), as in this chapter. In other words, the derivative of the type should be isomorphic to the type itself! Explain why your answer is correct. Hint: in computer science, our logarithms are mostly base 2.

Further reading: Algebraic Type Systems - Combinatorial Species

Exercise 5 (Homework): Finding Contexts

Write a function btree_deriv_at that takes a predicate over integers (i.e., a function f: int -> bool) and a btree, and builds a btree_deriv whose "hole" is in the first position for which the predicate returns true. It should return a btree_deriv option, with None if the predicate does not hold for any node.

This function lets you "search" a tree and get back a context pointing to the found element. Think about what order you want to search in (pre-order, in-order, or post-order) and what "first" means in that context.

Chapter 3: Computation

{.chapter-image}

Reduction semantics and operational reasoning

In this chapter, you will:

• Use function composition to build reusable “pipelines”
• Learn reduction semantics to reason about evaluation step by step
• Recognize and write tail-recursive programs (and understand what TCO buys you)
• Get a first working intuition for continuation-passing style (CPS)

References:

• "Using, Understanding and Unraveling the OCaml Language" by Didier Remy, Chapter 1
• "The OCaml system" manual, the tutorial part, Chapter 1

In this chapter, we explore how functional programs actually execute. We will learn how to reason about computation step by step using reduction semantics, and discover important optimization techniques like tail call optimization that make functional programming practical. Along the way, we will encounter our first taste of continuation passing style, a powerful programming technique that will reappear throughout this book.

3.1 Function Composition

Function composition is one of the most fundamental operations in functional programming. It allows us to build complex transformations by combining simpler functions. The usual way function composition is defined in mathematics is "backward"---the notation follows the convention of mathematical function application:

$$ (f \circ g)(x) = f(g(x)) $$

This means that when we write $f \circ g$, we first apply $g$ and then apply $f$ to the result. The function written on the left is applied last---hence the term "backward" composition. Here is how this is expressed in different functional programming languages:

This backward composition looks like function application but needs fewer parentheses. Do you recall the functions iso1 and iso2 from the previous chapter on type isomorphisms? Using backward composition, we could write:

let iso2 = step1l -| step2l -| step3l

While backward composition matches traditional mathematical notation, many programmers find a "forward" composition more intuitive. Forward composition follows the order in which computation actually proceeds---data flows from left to right, matching how we typically read code in most programming languages:

With forward composition, you can read a pipeline of transformations in the natural order:

let iso1 = step1r |- step2r |- step3r

Here, the data first passes through step1r, then the result goes to step2r, and finally to step3r. This "pipeline" style of programming is particularly popular in languages like F# and has influenced the design of many modern programming languages.

In the table above, the operator is written as \|- because Markdown tables use | to separate columns. In actual OCaml code, the operator name is (|-).

let (|-) f g x = g (f x)

Two related (but distinct) tools are also worth knowing:

• The standard library provides backward composition as Fun.compose, where Fun.compose f g x = f (g x).
• OCaml also provides the forward application operator (|>) (a pipeline): x |> f |> g means g (f x). Unlike (|-), this is not composition of functions but immediate application to a value.

Partial Application

Both composition examples above rely on partial application, a technique we introduced in the previous chapter. Recall that ((+) 1) is a function that adds 1 to its argument---we have provided only one of the two arguments that (+) requires. Partial application occurs whenever we supply fewer arguments than a function expects; the result is a new function that waits for the remaining arguments.

Consider the composition step1r |- step2r |- step3r. How exactly does partial application come into play here? The composition operator (|-) is defined as let (|-) f g x = g (f x), which means it takes three arguments: two functions f and g, and a value x. When we write step1r |- step2r, we are partially applying (|-) with just two arguments. The result is a function that still needs the final argument x.

Exercise: Think about the types involved. If step1r has type 'a -> 'b and step2r has type 'b -> 'c, what is the type of step1r |- step2r?

Check: step1r |- step2r has type 'a -> 'c. (Composition “cancels” the middle type 'b.)

Power Function

Now we define iterated function composition---applying a function to itself repeatedly. This is written mathematically as:

$$ f^n(x) := \underbrace{(f \circ \cdots \circ f)}_{n \text{ times}}(x) $$

In other words, $f^0$ is the identity function, $f^1 = f$, $f^2 = f \circ f$, and so on. In OCaml, we first define the backward composition operator, then use it to implement power:

let (-|) f g x = f (g x)

let rec power f n =
  if n <= 0 then (fun x -> x) else f -| power f (n-1)

When n <= 0, we return the identity function fun x -> x. Otherwise, we compose f with power f (n-1), which gives us one more application of f. Notice how elegantly this definition expresses the mathematical concept---we are literally composing f with itself n times.

This power function is surprisingly versatile. For example, we can use it to define addition in terms of the successor function:

let add n = power ((+) 1) n

Here add 5 7 would compute $7 + 1 + 1 + 1 + 1 + 1 = 12$. We could even define multiplication:

let mult k n = power ((+) k) n 0

This computes $0 + k + k + \ldots + k$ (adding $k$ a total of $n$ times), giving us $k \times n$. While not the most efficient implementation, these examples show how higher-order functions like power can express fundamental mathematical operations.

Numerical Derivative

A beautiful application of power is computing higher-order derivatives. First, let us define a numerical approximation of the derivative using the standard finite difference formula:

let derivative dx f = fun x -> (f (x +. dx) -. f x) /. dx

This definition computes $\frac{f(x + dx) - f(x)}{dx}$, which approximates $f'(x)$ when dx is small. Notice the explicit fun x -> ... syntax, which emphasizes that derivative dx f is itself a function---we are transforming a function f into its derivative function.

We can write the same definition more concisely using OCaml's curried function syntax:

let derivative dx f x = (f (x +. dx) -. f x) /. dx

Both definitions are equivalent, but the first makes the "function returning a function" structure more explicit, while the second is more compact.

A note on OCaml's numeric operators: OCaml uses different operators for floating-point arithmetic than for integers. The type of (+) is int -> int -> int, so we cannot use + with float values. Instead, operators followed by a dot work on float numbers: +., -., *., and /.. This might seem inconvenient at first, but it catches type errors at compile time and avoids the implicit conversions that cause subtle bugs in other languages.

Computing Higher-Order Derivatives

Now comes the payoff. With power and derivative, we can elegantly compute higher-order derivatives:

let pi = 4.0 *. atan 1.0
let sin''' = (power (derivative 1e-5) 3) sin
let _approx = sin''' pi

Here sin''' is the third derivative of sine. The expression (power (derivative 1e-5) 3) creates a function that applies the derivative operation three times---exactly what we need for the third derivative.

Mathematically, the third derivative of $\sin(x)$ is $-\cos(x)$, so sin''' pi should give us $-\cos(\pi) = 1$. The actual result will be close to 1, with some numerical error due to the finite difference approximation (the error compounds with each derivative we take).

This example demonstrates the power of treating functions as first-class values. We have built a general-purpose derivative operator and combined it with our power function to create an $n$th-derivative calculator---all in just a few lines of code.

3.2 Evaluation Rules (Reduction Semantics)

So far, we have written OCaml programs and observed their results, but we have not precisely described how those results are computed. To understand how OCaml programs execute, we need to formalize the evaluation process. This section presents reduction semantics (also called operational semantics), which describes computation as a series of rewriting steps that transform expressions until we reach a final value.

Understanding reduction semantics is valuable for several reasons. It helps us predict what our programs will do, reason about their efficiency, and understand subtle behaviors like infinite loops and non-termination. The ideas here also form the foundation for understanding more advanced topics like type systems and program verification.

Expressions

Programs consist of expressions. Here is the grammar of expressions for a simplified version of OCaml (we omit some features for clarity):

Arity means how many arguments something requires. For constructors, arity tells us how many components the constructor holds; for functions (primitives), it tells us how many arguments they need before they can compute a result. For tuple patterns, arity is simply the length of the tuple.

Meta-syntax note. In the grammar and rules below, we write constructors as if they were truly $n$-ary, e.g. $C^3(a_1,a_2,a_3)$. In actual OCaml syntax, constructors take exactly one argument; “multiple arguments” are represented by a tuple, e.g. Node (v1, v2, v3). The $n$-ary presentation is a convenient mathematical shorthand.

Evaluation-order note. The small-step rules below are intentionally simplified. In particular, the “context” rules allow reducing subexpressions in more than one place. Real OCaml is strict (call-by-value) and evaluates subexpressions in a deterministic order (in current OCaml implementations this is often right-to-left); the details matter when you have effects (exceptions, printing, mutation), but are usually irrelevant for purely functional code.

The fix Primitive

Our grammar above includes functions defined with fun, but what about recursive functions defined with let rec? To keep our semantics simple, we introduce a primitive fix that captures the essence of recursion:

$$ \texttt{let rec } f ; x = e_1 \texttt{ in } e_2 \equiv \texttt{let } f = \texttt{fix (fun } f ; x \texttt{ -> } e_1 \texttt{) in } e_2 $$

The fix primitive is a fixpoint combinator. It takes a function that expects to receive "itself" as its first argument and produces a function that, when called, behaves as if it has access to itself for recursive calls. This might seem mysterious now, but we will see exactly how it works when we examine its reduction rule below.

Values

Expressions evaluate (i.e., compute) to values. Values are expressions that cannot be reduced further---they are the "final answers" of computation:

$$ \begin{array}{lcll} v & := & \texttt{fun } x \texttt{ -> } a & \text{(defined) functions} \ & | & C^n(v_1, \ldots, v_n) & \text{constructed values} \ & | & f^n ; v_1 ; \cdots ; v_k & k < n \text{ (partially applied primitives)} \end{array} $$

Note that functions are values: fun x -> x + 1 is already fully evaluated---there is nothing more to compute until the function is applied to an argument. Similarly, constructed values like Some 42 or (1, 2, 3) are values when all their components are values.

Partially applied primitives like (+) 3 are also values. The expression (+) 3 has received one argument but needs another before it can compute a sum. Until that second argument arrives, there is nothing more to do, so (+) 3 is a value.

Substitution

The heart of evaluation is substitution. To substitute a value $v$ for a variable $x$ in expression $a$, we write $a[x := v]$. This notation means that every occurrence of $x$ in $a$ is replaced by $v$.

For example, if $a$ is the expression x + x * y and we substitute 3 for x, we get 3 + 3 * y. In our notation: (x + x * y)[x := 3] = 3 + 3 * y.

In the presence of binders like fun x -> ... (and pattern-bound variables), substitution must be capture-avoiding: we are allowed to rename bound variables so we do not accidentally change which occurrence refers to which binder.

Implementation note: Although we describe substitution as "replacing" variables with values, the actual implementation in OCaml does not duplicate the value $v$ in memory each time it appears. Instead, OCaml uses closures and sharing to ensure that values are stored once and referenced wherever needed. This is both more efficient and essential for handling recursive data structures.

Reduction Rules (Redexes)

Now we can describe how computation actually proceeds. Reduction works by finding reducible expressions called redexes (short for "reducible expressions") and applying reduction rules that rewrite them into simpler forms. We write $e_1 \rightsquigarrow e_2$ to mean "expression $e_1$ reduces to expression $e_2$ in one step."

Here are the fundamental reduction rules:

Function application (beta reduction): $$ (\texttt{fun } x \texttt{ -> } a) ; v \rightsquigarrow a[x := v] $$

This is the most important rule. When we apply a function fun x -> a to a value $v$, we substitute $v$ for the parameter $x$ throughout the function body $a$. This rule is traditionally called "beta reduction" in the lambda calculus literature.

For example: (fun x -> x + 1) 5 $\rightsquigarrow$ 5 + 1 $\rightsquigarrow$ 6.

Let binding: $$ \texttt{let } x = v \texttt{ in } a \rightsquigarrow a[x := v] $$

A let binding works similarly: once the bound expression has been evaluated to a value $v$, we substitute it into the body. Notice that let x = e in a is essentially equivalent to (fun x -> a) e---both bind $x$ to the result of evaluating $e$ within the expression $a$.

Primitive application: $$ f^n ; v_1 ; \cdots ; v_n \rightsquigarrow f(v_1, \ldots, v_n) $$

When a primitive (like + or *) receives all the arguments it needs (determined by its arity $n$), it computes the result. Here $f(v_1, \ldots, v_n)$ denotes the actual result of the primitive operation---for example, (+) 2 3 $\rightsquigarrow$ 5.

Pattern matching with a variable pattern: $$ \texttt{match } v \texttt{ with } x \texttt{ -> } a \texttt{ | } \cdots \rightsquigarrow a[x := v] $$

A variable pattern always matches, binding the entire value to the variable.

Pattern matching with a non-matching constructor: $$ \frac{C_1 \neq C_2}{\begin{array}{c}\texttt{match } C_1^n(v_1, \ldots, v_n) \texttt{ with } C_2^k(p_1, \ldots, p_k) \texttt{ -> } a \texttt{ | } pm \ \rightsquigarrow \texttt{match } C_1^n(v_1, \ldots, v_n) \texttt{ with } pm\end{array}} $$

If the constructor in the value ($C_1$) does not match the constructor in the pattern ($C_2$), we skip this branch and try the remaining patterns ($pm$). This is how OCaml searches through pattern match cases from top to bottom.

Pattern matching with a matching constructor: $$ \texttt{match } C_1^n(v_1, \ldots, v_n) \texttt{ with } C_1^n(x_1, \ldots, x_n) \texttt{ -> } a \texttt{ | } \cdots \rightsquigarrow a[x_1 := v_1; \ldots; x_n := v_n] $$

If the constructor matches, we substitute all the values from inside the constructor for the corresponding pattern variables. For example, match Some 42 with Some x -> x + 1 | None -> 0 reduces to 42 + 1 because Some matches Some and we substitute 42 for x.

If $n = 0$, then $C_1^n(v_1, \ldots, v_n)$ stands for simply $C_1^0$, a constructor with no arguments (like None or []). We omit the more complex cases of nested pattern matching for brevity.

Rule Variables

In these rules, we use metavariables---placeholders that can be replaced with actual expressions. Understanding them is key to applying the rules:

• $x$ matches any variable name (like foo, n, or result)
• $a, a_1, \ldots, a_n$ match any expression (not necessarily a value)
• $v, v_1, \ldots, v_n$ match any value (expressions that are fully evaluated)

To apply a rule, find substitutions for these metavariables that make the left-hand side of the rule match your expression. Then the right-hand side (with the same substitutions applied) gives you the reduced expression.

For example, to apply the beta reduction rule to (fun n -> n * 2) 5:

1. Match fun x -> a with fun n -> n * 2, giving us $x = \texttt{n}$ and $a = \texttt{n * 2}$
2. Match $v$ with 5
3. The right-hand side $a[x := v]$ becomes (n * 2)[n := 5] which equals 5 * 2

Evaluation Context Rules

The reduction rules above only apply when the arguments are already values. But what if we have (fun x -> x + 1) (2 + 3)? The argument 2 + 3 is not a value, so we cannot directly apply beta reduction. We need rules that tell us evaluation can proceed inside subexpressions.

If $a_i \rightsquigarrow a_i'$ (meaning $a_i$ can take a reduction step), then:

$$ \begin{array}{lcl} a_1 ; a_2 & \rightsquigarrow & a_1' ; a_2 \ a_1 ; a_2 & \rightsquigarrow & a_1 ; a_2' \ C^n(a_1, \ldots, a_i, \ldots, a_n) & \rightsquigarrow & C^n(a_1, \ldots, a_i', \ldots, a_n) \ \texttt{let } x = a_1 \texttt{ in } a_2 & \rightsquigarrow & \texttt{let } x = a_1' \texttt{ in } a_2 \ \texttt{match } a_1 \texttt{ with } pm & \rightsquigarrow & \texttt{match } a_1' \texttt{ with } pm \end{array} $$

These rules describe where reduction can happen:

• In a function application $a_1 ; a_2$, the rules allow reducing either the function ($a_1$) or the argument ($a_2$). This is a common simplification in textbook semantics; OCaml itself uses a fixed evaluation order.
• In a constructor application, any argument can be evaluated.
• In a let binding let x = a1 in a2, the bound expression $a_1$ must be evaluated to a value before we can proceed. Notice there is no rule for evaluating $a_2$ directly---the body is only evaluated after the substitution happens.
• In a match expression, the scrutinee (the expression being matched) must be evaluated before pattern matching can proceed.

The fix Rule

Finally, the rule for the fix primitive, which enables recursion:

$$ \texttt{fix}^2 ; v_1 ; v_2 \rightsquigarrow v_1 ; (\texttt{fix}^2 ; v_1) ; v_2 $$

This rule is subtle but powerful. Let us unpack it:

1. fix is a binary primitive (arity 2), meaning it needs two arguments before it computes.
2. When we apply fix to two values $v_1$ and $v_2$, it "unrolls" one level of recursion by calling $v_1$ with two arguments: (fix v1) (which represents "the recursive function itself") and $v_2$ (the actual argument to the recursive call).
3. Because fix has arity 2, the expression (fix v1) is a partially applied primitive---and partially applied primitives are values! This is crucial: it means (fix v1) will not be evaluated further until it is applied to another argument inside $v_1$.

This delayed evaluation is what prevents infinite loops. If (fix v1) were evaluated immediately, we would get an infinite chain of expansions. Instead, evaluation only continues when the recursive function actually makes a recursive call.

fix is not an OCaml primitive; it is a pedagogical device. If you did want to define it directly in OCaml, you could (ironically) do so using let rec:

let fix f =
  let rec self x = f self x in
  self

Practice

The best way to understand reduction semantics is to work through examples by hand. Trace the evaluation of these expressions step by step:

Exercise 1

Evaluate let double x = x + x in double 3

Exercise 2

Evaluate (fun f -> fun x -> f (f x)) (fun y -> y + 1) 0

Exercise 3

Define the factorial function using fix and trace the evaluation of factorial 3

3.3 Symbolic Derivation Example

Let us see the reduction rules in action with a more substantial example. We will build a small computer algebra system that can represent mathematical expressions symbolically, evaluate them, and even compute their derivatives symbolically.

Consider the symbolic expression type from Lec3.ml:

type expression =
  | Const of float
  | Var of string
  | Sum of expression * expression    (* e1 + e2 *)
  | Diff of expression * expression   (* e1 - e2 *)
  | Prod of expression * expression   (* e1 * e2 *)
  | Quot of expression * expression   (* e1 / e2 *)

exception Unbound_variable of string

let rec eval env exp =
  match exp with
  | Const c -> c
  | Var v ->
    (try List.assoc v env with Not_found -> raise (Unbound_variable v))
  | Sum(f, g) -> eval env f +. eval env g
  | Diff(f, g) -> eval env f -. eval env g
  | Prod(f, g) -> eval env f *. eval env g
  | Quot(f, g) -> eval env f /. eval env g

The expression type represents mathematical expressions as a tree structure. Each constructor corresponds to a different kind of expression: constants, variables, and the four basic arithmetic operations. The eval function takes an environment env (a list of variable-value pairs) and recursively evaluates an expression to a floating-point number.

We can also define symbolic differentiation---computing the derivative of an expression without evaluating it numerically:

let rec deriv exp dv =
  match exp with
  | Const _ -> Const 0.0
  | Var v -> if v = dv then Const 1.0 else Const 0.0
  | Sum(f, g) -> Sum(deriv f dv, deriv g dv)
  | Diff(f, g) -> Diff(deriv f dv, deriv g dv)
  | Prod(f, g) -> Sum(Prod(f, deriv g dv), Prod(deriv f dv, g))
  | Quot(f, g) -> Quot(Diff(Prod(deriv f dv, g), Prod(f, deriv g dv)),
                       Prod(g, g))

The deriv function implements the standard rules of calculus:

• The derivative of a constant is 0.
• The derivative of the variable we are differentiating with respect to is 1; any other variable is treated as a constant (derivative 0).
• The sum and difference rules: $(f + g)' = f' + g'$ and $(f - g)' = f' - g'$.
• The product rule: $(f \cdot g)' = f \cdot g' + f' \cdot g$.
• The quotient rule: $(f / g)' = (f' \cdot g - f \cdot g') / g^2$.

For convenience, let us define some operators and variables so we can write expressions more naturally:

let x = Var "x"
let y = Var "y"
let z = Var "z"
let (+:) f g = Sum (f, g)
let (-:) f g = Diff (f, g)
let ( *: ) f g = Prod (f, g)
let (/:) f g = Quot (f, g)
let (!:) i = Const i

These custom operators (ending in :) let us write symbolic expressions that look almost like regular mathematical notation.

Now let us evaluate the expression $3x + 2y + x^2 y$ at $x = 1, y = 2$:

let example = !:3.0 *: x +: !:2.0 *: y +: x *: x *: y
let env = ["x", 1.0; "y", 2.0]

For nicer output, it is helpful to define a pretty-printer that displays expressions in infix notation (this is adapted from Lec3.ml):

let print_expr ppf exp =
  let open_paren prec op_prec =
    if prec > op_prec then Format.fprintf ppf "(@["
    else Format.fprintf ppf "@[" in
  let close_paren prec op_prec =
    if prec > op_prec then Format.fprintf ppf "@])"
    else Format.fprintf ppf "@]" in
  let rec print prec exp =
    match exp with
    | Const c -> Format.fprintf ppf "%.2f" c
    | Var v -> Format.fprintf ppf "%s" v
    | Sum(f, g) ->
      open_paren prec 0;
      print 0 f; Format.fprintf ppf "@ +@ "; print 0 g;
      close_paren prec 0
    | Diff(f, g) ->
      open_paren prec 0;
      print 0 f; Format.fprintf ppf "@ -@ "; print 1 g;
      close_paren prec 0
    | Prod(f, g) ->
      open_paren prec 2;
      print 2 f; Format.fprintf ppf "@ *@ "; print 2 g;
      close_paren prec 2
    | Quot(f, g) ->
      open_paren prec 2;
      print 2 f; Format.fprintf ppf "@ /@ "; print 3 g;
      close_paren prec 2
  in
  print 0 exp

And for tracing, we define a specialized evaluator eval_1_2 with the environment baked in (so the trace focuses on the expression structure):

let rec eval_1_2 exp =
  match exp with
  | Const c -> c
  | Var v ->
    (try List.assoc v env with Not_found -> raise (Unbound_variable v))
  | Sum(f, g) -> eval_1_2 f +. eval_1_2 g
  | Diff(f, g) -> eval_1_2 f -. eval_1_2 g
  | Prod(f, g) -> eval_1_2 f *. eval_1_2 g
  | Quot(f, g) -> eval_1_2 f /. eval_1_2 g

In the toplevel, you can now install the printer and trace the evaluation:

# #install_printer print_expr;;
# #trace eval_1_2;;
# eval_1_2 example;;

The trace output makes the recursive structure of the computation very concrete:

eval_1_2 <-- 3.00 * x + 2.00 * y + x * x * y
  eval_1_2 <-- x * x * y
    eval_1_2 <-- y
    eval_1_2 --> 2.
    eval_1_2 <-- x * x
      eval_1_2 <-- x
      eval_1_2 --> 1.
      eval_1_2 <-- x
      eval_1_2 --> 1.
    eval_1_2 --> 1.
  eval_1_2 --> 2.
  eval_1_2 <-- 3.00 * x + 2.00 * y
    eval_1_2 <-- 2.00 * y
      eval_1_2 <-- y
      eval_1_2 --> 2.
      eval_1_2 <-- 2.00
      eval_1_2 --> 2.
    eval_1_2 --> 4.
    eval_1_2 <-- 3.00 * x
      eval_1_2 <-- x
      eval_1_2 --> 1.
      eval_1_2 <-- 3.00
      eval_1_2 --> 3.
    eval_1_2 --> 3.
  eval_1_2 --> 7.
eval_1_2 --> 9.
- : float = 9.

The arrows <-- and --> show function calls and returns, respectively. Each level of indentation represents a nested function call. These indentation levels correspond to stack frames---the runtime structures that store the state of each function call. Each time eval_1_2 is called recursively, a new stack frame is created to remember where to return and what computation remains.

The final result is $3 \cdot 1 + 2 \cdot 2 + 1 \cdot 1 \cdot 2 = 3 + 4 + 2 = 9$, as expected.

This trace visualization brings us to an important question: what happens when we have very deep recursion? This leads us to our next topic.

3.4 Tail Calls and Tail Recursion

The call stack is finite, and each recursive call typically adds a new frame to it. This means that deeply recursive functions can exhaust the stack and crash---a notorious problem known as "stack overflow." Fortunately, functional language implementations have a trick to avoid this problem in many cases.

Excuse me for not formally defining what a function call is... Computers normally evaluate programs by creating stack frames on the call stack for each function call. A stack frame stores the local variables, the return address (where to continue after the function returns), and other bookkeeping information. The trace in the previous section illustrates this: each level of indentation represents a new stack frame.

What is a Tail Call?

The key insight is that not all function calls require a new stack frame. A tail call is a function call that is performed as the very last action when computing a function---there is nothing more to do after the call returns except to return that value. For example:

let f x = g (x + 1)

The call to g is a tail call. Once g returns some value, f simply returns that same value---no further computation is needed.

In contrast:

let f x = 1 + g x

The call to g is not a tail call. After g returns, we still need to add 1 to the result before f can return. This means we need to remember to do the addition, which requires keeping the stack frame around.

Tail Call Optimization

Functional language compilers (including OCaml's) recognize tail calls and optimize them by performing tail call optimization (TCO). Instead of creating a new stack frame, the compiler generates code that reuses the current frame by performing a "jump" to the called function. This means tail calls use constant stack space, no matter how deep the call chain goes.

This optimization is not just a nice-to-have; it is essential for functional programming. Without TCO, many natural recursive algorithms would be impractical because they would overflow the stack on moderately large inputs.

Tail Recursive Functions

A function is tail recursive if all of its recursive calls (including calls to mutually recursive functions it depends on) are tail calls.

Writing tail recursive functions requires a shift in thinking. Instead of building up the result as recursive calls return, we build it up as we make the calls. This typically requires an extra accumulator argument that carries the partial result through the recursion.

The key insight is that with an accumulator, results are computed in "reverse order"---we do the work while climbing into the recursion (making calls) rather than while climbing out (returning from calls).

Example: Counting

Let us see this in action with a simple counting function. Compare these two versions:

let rec count n =
  if n <= 0 then 0 else 1 + (count (n-1))

This version is not tail recursive. Look at the recursive case: after count (n-1) returns, we still need to add 1 to the result. Each recursive call must remember to do this addition, consuming a stack frame.

Now compare with the tail recursive version:

let rec count_tcall acc n =
  if n <= 0 then acc else count_tcall (acc+1) (n-1)

Here, the recursive call count_tcall (acc+1) (n-1) is the very last thing the function does---its result becomes our result directly. The accumulator acc carries the running count: we add 1 to it before the recursive call rather than after it returns. To count to 1000000, we call count_tcall 0 1000000.

Example: Building Lists

The counting example does not really show the practical impact because the numbers are so small. Let us see a more dramatic example with lists:

let rec unfold n = if n <= 0 then [] else n :: unfold (n-1)

This function builds a list counting down from n to 1. It is not tail recursive because after the recursive call unfold (n-1) returns, we must cons n onto the front of the result.

# unfold 100000;;
- : int list = [100000; 99999; 99998; 99997; ...]

# unfold 1000000;;
Stack overflow during evaluation (looping recursion?).

With 100,000 elements, it works. But with a million elements, we run out of stack space and the program crashes! This is a serious problem for practical programming.

Now consider the tail-recursive version:

let rec unfold_tcall acc n =
  if n <= 0 then acc else unfold_tcall (n::acc) (n-1)

The accumulator acc collects the list as we go. We cons each element onto the accumulator before the recursive call. However, there is a catch: because we are building the list as we descend into the recursion (rather than as we return), the list comes out in reverse order:

# unfold_tcall [] 100000;;
- : int list = [1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; ...]

# unfold_tcall [] 1000000;;
- : int list = [1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; ...]

The tail-recursive version handles a million elements effortlessly. The trade-off is that we get [1; 2; 3; ...] instead of [1000000; 999999; ...]. If we need the original order, we could reverse the result at the end (which is an O(n) operation but uses only constant stack space).

A Challenge: Tree Depth

Not all recursive functions can be easily converted to tail recursive form. Consider this problem: can we find the depth of a binary tree using a tail-recursive function?

type btree = Tip | Node of int * btree * btree

Here is the natural recursive approach:

let rec depth tree = match tree with
  | Tip -> 0
  | Node(_, left, right) -> 1 + max (depth left) (depth right)

This is not tail recursive: after both recursive calls return, we still need to compute 1 + max .... The fundamental challenge is that we have two recursive calls that we need to make. A simple accumulator will not work---we cannot proceed with one subtree until we know the result of the other.

This seems like an impossible situation. How can we make a function tail recursive when it inherently needs to explore two branches? The answer involves a technique called continuation passing style, which we explore in the next section.

Note on Lazy Languages

The issue of tail recursion is more nuanced for lazy programming languages like Haskell. In a lazy language, expressions are only evaluated when their values are actually needed. The cons operation (:) does not immediately evaluate its arguments---it just builds a "promise" to compute them later.

This means that building a list with n : unfold (n-1) does not consume stack space in the same way as in OCaml. The unfold (n-1) is not evaluated immediately; it is just stored as an unevaluated expression (called a "thunk"). Stack space is only consumed later, when you actually traverse the list. This gives lazy languages different performance characteristics and trade-offs.

3.5 First Encounter of Continuation Passing Style

We can solve the tree depth problem using Continuation Passing Style (CPS). This is a powerful technique that transforms programs in a surprising way: instead of returning values, functions receive an extra argument---a continuation---that tells them what to do with their result.

The key idea is to postpone doing actual work until the very last moment by passing around a continuation---a function that represents "what to do next with this result."

let rec depth_cps tree k = match tree with
  | Tip -> k 0
  | Node(_, left, right) ->
    depth_cps left (fun dleft ->
      depth_cps right (fun dright ->
        k (1 + (max dleft dright))))

let depth tree = depth_cps tree (fun d -> d)

Let us understand how this works step by step:

1. The continuation parameter: The function takes an extra parameter k, called the continuation. Instead of returning a value directly, depth_cps will call k with its result. You can think of k as meaning "and then do this with the answer."

2. The base case (Tip): When we reach a leaf, the depth is 0. Instead of returning 0, we call k 0---"give 0 to whoever is waiting for our answer."

3. The recursive case (Node): This is where CPS shines. We need to compute depths of both subtrees and combine them. Here is how we do it:

   • First, recursively compute the depth of the left subtree. But instead of waiting for the result, we pass a continuation: fun dleft -> ...
   • This continuation says "when you have the left depth (call it dleft), then..."
   • ...compute the depth of the right subtree, passing another continuation: fun dright -> ...
   • This inner continuation says "when you have the right depth (call it dright), then..."
   • ...finally call the original continuation k with the combined result 1 + max dleft dright

4. The wrapper function: To use depth_cps, we need to provide an initial continuation. We pass the identity function fun d -> d, which just returns whatever it receives. This is the "final consumer" of the result.

The magic is that every recursive call is now a tail call! Look carefully: depth_cps left (...) is the last thing the function does in that branch---everything else is inside the continuation, which will be called later.

Where does the "pending work" go? Instead of being stored on the call stack, it is captured in the continuation closures. These closures are allocated on the heap. We have traded stack space for heap space.

Important caveat: This does not completely solve the stack overflow problem---we are just moving the problem from the stack to the heap. For very deep trees, the continuation closures can grow very large, potentially exhausting memory. True solutions for extreme cases involve techniques like trampolining (returning control to a loop) or using explicit data structures to represent the pending work. Nevertheless, CPS is often more space-efficient than direct recursion, and it is a fundamental technique that appears throughout functional programming.

We will encounter CPS again when studying monads and advanced control flow, where it provides the foundation for powerful abstractions.

3.6 Exercises

These exercises will help you practice the concepts from this chapter: function composition, reduction semantics, tail recursion, and continuation passing style.

Exercise 1: Tree Traversals

By "traverse a tree" below we mean: write a function that takes a tree and returns a list of values in the nodes of the tree. Use the btree type defined earlier.

1. Write a function (of type btree -> int list) that traverses a binary tree in prefix order (also called preorder)---first the value stored in a node, then values in all nodes to the left, then values in all nodes to the right.

2. Write a traversal in infix order (also called inorder)---first values in all nodes to the left, then the value stored in the node, then values in all nodes to the right. For a binary search tree, this would give you the elements in sorted order.

3. Write a traversal in breadth-first order (also called level order)---visit all nodes at depth 0, then all nodes at depth 1, and so on. Hint: you will need an auxiliary data structure (a queue) to keep track of nodes to visit.

Exercise 2: CPS Transformation

Turn the function from Exercise 1 (prefix or infix traversal) into continuation passing style. Compare the structure of your CPS version to the original. What are the trade-offs?

Exercise 3: Tree Derivatives Revisited

Do the homework from the end of Chapter 2: write btree_deriv_at that takes a predicate over integers and a btree, and builds a btree_deriv whose "hole" is in the first position (using your chosen traversal order) for which the predicate returns true.

Exercise 4: Expression Simplification

Write a function simplify: expression -> expression that simplifies symbolic expressions, so that for example the result of simplify (deriv exp dv) looks more like what a human would get computing the derivative of exp with respect to dv.

Some simplifications to consider:

• $0 + x = x$ and $x + 0 = x$
• $0 \cdot x = 0$ and $x \cdot 0 = 0$
• $1 \cdot x = x$ and $x \cdot 1 = x$
• $x - 0 = x$
• $x / 1 = x$

Approach this in two steps:

1. Write a simplify_once function that performs a single "pass" of simplification over the expression tree.
2. Wrap it using a general fixpoint function that performs an operation until a fixed point is reached: given $f$ and $x$, it computes $f^n(x)$ such that $f^n(x) = f^{n+1}(x)$ (i.e., applying $f$ one more time does not change the result).

Why do we need iteration to a fixed point rather than a single pass?

Exercise 5: Sorting Algorithms

Write two sorting algorithms working on lists: merge sort and quicksort.

1. Merge sort splits the list roughly in half, sorts the parts recursively, and merges the sorted parts into the sorted result. You will need a helper function to merge two sorted lists.

2. Quicksort splits the list into elements smaller than and greater-than-or-equal-to the first element (the "pivot"), sorts the parts recursively, and concatenates them.

Which of these algorithms can be implemented in a tail-recursive manner? What about the helper functions (merge, partition)?

Chapter 4: Functions

{.chapter-image}

Programming in untyped lambda-calculus

In this chapter, you will:

• Rehearse reduction-by-hand on a non-trivial recursive program
• Learn the syntax and $\beta$-reduction rules of the untyped lambda-calculus
• Encode booleans, pairs, naturals, lists, and trees using functions alone
• Understand recursion via fixpoint combinators (and how evaluation order matters)

This chapter explores the theoretical foundations of functional programming through the untyped lambda-calculus. We embark on a fascinating journey that reveals a surprising truth: every computation can be expressed using nothing but functions. No numbers, no booleans, no data structures---just functions all the way down.

We begin with a review of computation by hand using our reduction semantics, then introduce the lambda-calculus notation and show how to encode fundamental data types---booleans, pairs, and natural numbers---using only functions. The chapter concludes with an examination of recursion through fixpoint combinators and practical considerations for avoiding infinite loops in eager evaluation.

References:

• "Introduction to Lambda Calculus" by Henk Barendregt and Erik Barendsen
• "Lecture Notes on the Lambda Calculus" by Peter Selinger

4.1 Review: Computation by Hand

Before diving into the lambda-calculus, let us work through a complete example of evaluation using the reduction rules from Chapter 3. Computing a larger, recursive program by hand will solidify our understanding of how computation proceeds step by step and prepare us for the more abstract setting of lambda-calculus.

Recall that we use fix instead of let rec to simplify our rules for recursion. Also remember our syntactic conventions: fun x y -> e stands for fun x -> (fun y -> e), and so forth.

Consider the following recursive length function applied to a two-element list:

let rec fix f x = f (fix f) x

type int_list = Nil | Cons of int * int_list

let length =
  fix (fun f l ->
    match l with
    | Nil -> 0
    | Cons (_x, xs) -> 1 + f xs)
in
length (Cons (1, (Cons (2, Nil))))

Let us trace through this computation step by step. First, we eliminate the let ... in ... binding for length:

$$\texttt{let } x = v \texttt{ in } a \rightsquigarrow a[x := v]$$

This gives us:

fix (fun f l ->
    match l with
      | Nil -> 0
      | Cons (x, xs) -> 1 + f xs) (Cons (1, (Cons (2, Nil))))

Next, we apply the fix rule:

$$\texttt{fix}^2 ; v_1 ; v_2 \rightsquigarrow v_1 ; (\texttt{fix}^2 ; v_1) ; v_2$$

This unfolds to:

(fun f l ->
    match l with
      | Nil -> 0
      | Cons (x, xs) -> 1 + f xs)
    (fix (fun f l ->
      match l with
        | Nil -> 0
        | Cons (x, xs) -> 1 + f xs))
    (Cons (1, (Cons (2, Nil))))

Function application reduces according to:

$$(\texttt{fun } x \texttt{ -> } a) ; v \rightsquigarrow a[x := v]$$

After substituting both f and l, we get:

(match Cons (1, (Cons (2, Nil))) with
    | Nil -> 0
    | Cons (x, xs) -> 1 + (fix (fun f l ->
      match l with
        | Nil -> 0
        | Cons (x, xs) -> 1 + f xs)) xs)

Pattern matching against a non-matching constructor moves to the next branch:

$$ \begin{aligned} & \texttt{match } C_1^n(v_1, \ldots, v_n) \texttt{ with} \ & C_2^n(p_1, \ldots, p_k) \texttt{ -> } a \texttt{ | } pm \rightsquigarrow \texttt{match } C_1^n(v_1, \ldots, v_n) \texttt{ with } pm \end{aligned} $$

Pattern matching against a matching constructor performs substitution:

$$ \begin{aligned} & \texttt{match } C_1^n(v_1, \ldots, v_n) \texttt{ with} \ & C_1^n(x_1, \ldots, x_n) \texttt{ -> } a \texttt{ | } \ldots \rightsquigarrow a[x_1 := v_1; \ldots; x_n := v_n] \end{aligned} $$

After matching and substitution:

1 + (fix (fun f l ->
      match l with
        | Nil -> 0
        | Cons (x, xs) -> 1 + f xs)) (Cons (2, Nil))

Continuing the evaluation, we apply fix again and work through the pattern match for Cons (2, Nil), eventually reaching:

1 + (1 + (fix (fun f l ->
             match l with
               | Nil -> 0
               | Cons (x, xs) -> 1 + f xs)) Nil)

One more unfolding and pattern match against Nil gives:

1 + (1 + 0)

Finally, applying the built-in addition:

$$f^n ; v_1 ; \ldots ; v_n \rightsquigarrow f(v_1, \ldots, v_n)$$

We obtain the result: 2.

4.2 Language and Rules of the Untyped Lambda-Calculus

The lambda-calculus, introduced by Alonzo Church in the 1930s, is a minimal formal system for expressing computation. It may seem surprising that such a stripped-down language can be computationally complete, but that is precisely what we will demonstrate in this chapter. To work with lambda-calculus, we first simplify our language in several ways:

1. Forget about types. In pure lambda-calculus, there is no type system constraining which terms can be combined. Any function can be applied to any argument---including itself!

2. Introduce notation. We write $\lambda x.a$ for fun x -> a, and $\lambda xy.a$ for fun x y -> a, and so forth. This notation is more compact and traditional in the literature.

3. Reduce to essentials. We keep only functions (lambda abstractions) and variables---no constructors, no built-in primitives. Everything else will be encoded using functions.

The core reduction rule of lambda-calculus is called $\beta$-reduction:

$$(\texttt{fun } x \texttt{ -> } a_1) ; a_2 \rightsquigarrow a_1[x := a_2]$$

Note that this rule is more general than the one we use for OCaml evaluation. In our OCaml semantics, we require the argument to be a value: $(\texttt{fun } x \texttt{ -> } a) ; v \rightsquigarrow a[x := v]$. The general $\beta$-reduction rule allows substituting any expression, not just values.

Lambda-calculus also uses $\alpha$-conversion (bound variable renaming), or equivalent techniques, to avoid variable capture---the unintended binding of free variables during substitution. We will explore the implications of $\beta$-reduction more deeply in the chapter on laziness.

Why is $\beta$-reduction more general than our evaluation rule? Consider the expression $(\lambda x. x) ; ((\lambda y. y) ; z)$. With $\beta$-reduction, we could reduce the outer application first, obtaining $((\lambda y. y) ; z)$. Our evaluation rule would require first reducing the argument to a value---but here z is a free variable, not a value, so we would be stuck!

This example is intentionally an open term (it has a free variable z): in lambda-calculus we often reason about open terms up to $\beta$-equivalence, while programming-language evaluation is usually defined for closed programs.

4.3 Booleans

Alonzo Church originally introduced lambda-calculus as a foundation for logic, seeking to encode logical reasoning in a purely computational form. There are multiple ways to encode various sorts of data in lambda-calculus, though not all of them work well in a typed setting---the straightforward encode/decode functions may not type-check for some encodings.

The key insight behind the Church encoding of booleans is to represent truth values as selector functions. Think about what a boolean fundamentally does: it chooses between two alternatives. So we define:

• True selects the first argument: c_true $= \lambda xy.x$
• False selects the second argument: c_false $= \lambda xy.y$

In OCaml syntax:

let c_true = fun x y -> x   (* "True" is projection on the first argument *)
let c_false = fun x y -> y  (* And "false" on the second argument *)

Once we have booleans as selectors, logical operations become elegant. Logical conjunction can be defined as:

$$\texttt{c_and} = \lambda xy. x ; y ; \texttt{c_false}$$

The logic behind this definition is beautifully simple: we apply x (which is a selector) to two arguments. If x is true, it selects its first argument, which is y---so the result is true only if both x and y are true. If x is false, it selects its second argument, c_false, and returns false immediately without even looking at y.

let c_and = fun x y -> x y c_false  (* If one is false, then return false *)

Let us verify this works. For c_and c_true c_true:

$$(\lambda xy. x ; y ; \texttt{c_false}) ; (\lambda xy.x) ; (\lambda xy.x)$$

reduces to:

$$(\lambda xy.x) ; (\lambda xy.x) ; \texttt{c_false}$$

which gives us $\lambda xy.x$ = c_true. You can verify that for any other combination involving c_false, the result is c_false.

To verify our encodings in OCaml, we need encode and decode functions. The decoder works by applying our Church boolean to the actual OCaml values true and false:

let encode_bool b = if b then c_true else c_false
let decode_bool c = (Obj.magic c) true false  (* Don't enforce type on c *)

Exercise: Church Boolean Combinators

Define c_or and c_not yourself! Hint: think about what c_or should return when the first argument is true, and when it is false. For c_not, consider that a boolean is a function that selects between two arguments.

4.4 If-then-else and Pairs

From now on, we will use OCaml syntax for our lambda-calculus programs. This makes it easier to experiment with our encodings in the toplevel.

An important observation is that our encoded booleans already implement conditional selection:

let if_then_else b t e = b t e  (* Booleans select the branch! *)

Wait---is if_then_else “just” the identity function? Up to $\eta$-equivalence, yes: fun b -> b and fun b t e -> b t e are the same function. Since c_true returns its first argument and c_false returns its second, if_then_else b t e simply applies b to the two branches. The boolean is the conditional.

Remember to play with these functions in the toplevel to build intuition. Try expressions like if_then_else c_true "yes" "no" and see what happens.

Pairs

Pairs (ordered tuples of two elements) can be encoded using a similar idea. The key insight is that a pair needs to "remember" two values and provide them when asked. We can achieve this by creating a function that holds onto both values and waits for a selector to choose between them:

let c_pair m n = fun x -> x m n  (* We couple things *)
let c_first = fun p -> p c_true  (* by passing them together *)
let c_second = fun p -> p c_false  (* Check that it works! *)

A pair is a function that, when given a selector, applies that selector to both components. To extract the first component, we pass c_true (which selects the first argument); to extract the second, we pass c_false. Verify for yourself that c_first (c_pair a b) reduces to a!

For verification:

let encode_pair enc_fst enc_snd (a, b) =
  c_pair (enc_fst a) (enc_snd b)
let decode_pair de_fst de_snd c = c (fun x y -> de_fst x, de_snd y)
let decode_bool_pair c = decode_pair decode_bool decode_bool c

We can define larger tuples in the same manner: let c_triple l m n = fun x -> x l m n

4.5 Pair-Encoded Natural Numbers

Now we come to encoding numbers---a crucial test of whether functions alone can represent all data. Our first encoding of natural numbers uses nested pairs. The representation is based on the depth of nested pairs whose rightmost leaf is the identity function $\lambda x.x$ and whose left elements are c_false.

let pn0 = fun x -> x           (* Start with the identity function *)
let pn_succ n = c_pair c_false n  (* Stack another pair *)

let pn_pred = fun x -> x c_false  (* Extract the nested number *)
let pn_is_zero = fun x -> x c_true  (* Check if it's the base case *)

The number 0 is represented as the identity function. The number 1 is c_pair c_false pn0, the number 2 is c_pair c_false (c_pair c_false pn0), and so on. Think of it as a stack of pairs, where the height of the stack represents the number.

How do pn_pred and pn_is_zero work? Let us think through this carefully:

• The identity function pn0, when applied to any argument, returns that argument.
• A successor c_pair c_false n is a function waiting for a selector; applying it to c_false selects the second component (the predecessor), while applying it to c_true selects the first component (c_false).

So pn_is_zero applies the number to c_true:

• For pn0, we get c_true back (since pn0 is the identity)---the number is zero!
• For any successor, we get c_false back (the first component of the pair)---the number is not zero!

We program in untyped lambda-calculus as an exercise, and we need encoding/decoding to verify our work. Since these encodings do not type-check cleanly in OCaml, using Obj.magic to bypass the type system for encoding/decoding is "fair game":

let rec encode_pnat n =                (* We use Obj.magic to forget types *)
  if n <= 0 then Obj.magic pn0
  else pn_succ (Obj.magic (encode_pnat (n-1)))  (* Disregarding types, *)
let rec decode_pnat pn =               (* these functions are straightforward! *)
  if decode_bool (pn_is_zero pn) then 0
  else 1 + decode_pnat (pn_pred (Obj.magic pn))

Needless to say, Obj.magic is unsafe and should not be used in real code; here it is only a convenient bridge from untyped lambda-terms to OCaml so we can test our encodings.

4.6 Church Numerals

Do you remember our function power f n from Chapter 3 that composed a function with itself n times? We will use a similar idea for a different, and historically important, representation of numbers.

Church numerals represent a natural number $n$ as a function that applies its first argument $n$ times to its second argument:

let cn0 = fun f x -> x        (* The same as c_false *)
let cn1 = fun f x -> f x      (* Behaves like identity when f = id *)
let cn2 = fun f x -> f (f x)
let cn3 = fun f x -> f (f (f x))

This is the original Alonzo Church encoding, and it is remarkably elegant. The number $n$ is represented as $\lambda fx. f^n(x)$, where $f^n$ denotes $n$-fold composition. A number literally is the act of doing something $n$ times!

Notice that cn0 is the same as c_false---zero applications of f just returns x.

The successor function adds one more application of f:

let cn_succ = fun n f x -> f (n f x)

Exercise: Church Numeral Arithmetic

Define addition, multiplication, and comparing to zero for Church numerals. Also try to define the predecessor function "-1".

It turns out even Alonzo Church could not define predecessor right away! The story goes that his student Stephen Kleene figured it out while at the dentist. Try to make some progress on addition and multiplication first (they are not too hard), and then attempt predecessor before looking at the solution below.

let (-|) f g x = f (g x)  (* Backward composition operator *)

let rec encode_cnat n f =
  if n <= 0 then (fun x -> x) else f -| encode_cnat (n-1) f
let decode_cnat n = n ((+) 1) 0
let cn7 f x = encode_cnat 7 f x   (* We need to eta-expand these definitions *)
let cn13 f x = encode_cnat 13 f x  (* for type-system reasons *)
                                   (* (because OCaml allows side-effects) *)
let cn_add = fun n m f x -> n f (m f x)  (* Put n of f in front *)
let cn_mult = fun n m f -> n (m f)       (* Repeat n times *)
                                          (* putting m of f in front *)
let cn_prev n =
  fun f x ->
    (* A Church numeral is an n-step iterator. Predecessor is tricky because
       we cannot “subtract an iteration”; instead we build a small state
       transformer that delays the use of [f] and then skips the first step. *)
    n
      (fun g h -> h (g f))
      (fun _z -> x)
      (fun z -> z)

Addition is intuitive: to add $n$ and $m$, we first apply f $m$ times (giving us m f x), then apply f $n$ more times. Multiplication is even more clever: we apply the operation "apply f $m$ times" $n$ times, which computes $m \times n$ applications of f.

The predecessor function is ingenious and worth studying carefully. The challenge is that Church numerals only know how to apply f more times, not fewer. Kleene's insight was to build up a chain of functions that, when "started" with the identity, yields $n-1$ applications of f. The key is to delay the actual application of f and skip the first one.

cn_is_zero is left as an exercise. Hint: what happens when you apply zero to a function that always returns c_false and start with c_true?

Tracing cn_prev cn3

The predecessor function is tricky enough that it is worth tracing through a complete example. Let us trace through decode_cnat (cn_prev cn3) to see how it computes 2 from 3:

$$\rightsquigarrow^*$$

(cn_prev cn3) ((+) 1) 0

$$\rightsquigarrow^*$$

(fun f x ->
    cn3
      (fun g h -> h (g f))
      (fun _z -> x)
      (fun z -> z)) ((+) 1) 0

$$\rightsquigarrow^*$$

((fun f x -> f (f (f x)))
      (fun g h -> h (g ((+) 1)))
      (fun z -> 0)
      (fun z -> z))

$$\rightsquigarrow^*$$

((fun g h -> h (g ((+) 1)))
  ((fun g h -> h (g ((+) 1)))
    ((fun g h -> h (g ((+) 1)))
      (fun z -> 0))))
  (fun z -> z))

$$\rightsquigarrow^*$$

((fun z -> z)
  (((fun g h -> h (g ((+) 1)))
    ((fun g h -> h (g ((+) 1)))
      (fun z -> 0)))) ((+) 1)))

$$\rightsquigarrow^*$$

(fun g h -> h (g ((+) 1)))
  ((fun g h -> h (g ((+) 1)))
    (fun z -> 0)) ((+) 1)

$$\rightsquigarrow^*$$

((+) 1) ((fun g h -> h (g ((+) 1)))
          (fun z -> 0) ((+) 1))

$$\rightsquigarrow^*$$

((+) 1) (((+) 1) ((fun z -> 0) ((+) 1)))

$$\rightsquigarrow^*$$

((+) 1) (((+) 1) (0))

$$\rightsquigarrow^*$$

((+) 1) 1

$\rightsquigarrow^*$ 2

4.7 Recursion: Fixpoint Combinators

We have seen how to encode data in lambda-calculus, but how do we encode computation, especially recursive computation? In lambda-calculus, there is no let rec or any built-in notion of a function referring to itself. Instead, recursion is achieved through fixpoint combinators---remarkable lambda terms that compute fixed points of functions.

Turing's Fixpoint Combinator

$$\Theta = (\lambda xy. y ; (x ; x ; y)) ; (\lambda xy. y ; (x ; x ; y))$$

Let us verify it computes fixed points. Define $N = \Theta F$:

$$ \begin{aligned} N &= \Theta F \ &= (\lambda xy. y ; (x ; x ; y)) ; (\lambda xy. y ; (x ; x ; y)) ; F \ &=_{\rightarrow\rightarrow} F ; ((\lambda xy. y ; (x ; x ; y)) ; (\lambda xy. y ; (x ; x ; y)) ; F) \ &= F ; (\Theta F) = F ; N \end{aligned} $$

So $N = F ; N$, meaning $N$ is a fixed point of $F$.

Curry's Fixpoint Combinator (Y Combinator)

$$\mathbf{Y} = \lambda f. (\lambda x. f ; (x ; x)) ; (\lambda x. f ; (x ; x))$$

$$ \begin{aligned} N &= \mathbf{Y} F \ &= (\lambda f. (\lambda x. f ; (x ; x)) ; (\lambda x. f ; (x ; x))) ; F \ &={\rightarrow} (\lambda x. F ; (x ; x)) ; (\lambda x. F ; (x ; x)) \ &={\rightarrow} F ; ((\lambda x. F ; (x ; x)) ; (\lambda x. F ; (x ; x))) \ &=_{\leftarrow} F ; ((\lambda f. (\lambda x. f ; (x ; x)) ; (\lambda x. f ; (x ; x))) ; F) \ &= F ; (\mathbf{Y} F) = F ; N \end{aligned} $$

Call-by-Value Fixpoint Combinator

$$\texttt{fix} = \lambda f'. (\lambda fx. f' ; (f ; f) ; x) ; (\lambda fx. f' ; (f ; f) ; x)$$

$$ \begin{aligned} N &= \texttt{fix} ; F \ &= (\lambda f'. (\lambda fx. f' ; (f ; f) ; x) ; (\lambda fx. f' ; (f ; f) ; x)) ; F \ &={\rightarrow} (\lambda fx. F ; (f ; f) ; x) ; (\lambda fx. F ; (f ; f) ; x) \ &={\rightarrow} \lambda x. F ; ((\lambda fx. F ; (f ; f) ; x) ; (\lambda fx. F ; (f ; f) ; x)) ; x \ &={\leftarrow} \lambda x. F ; ((\lambda f'. (\lambda fx. f' ; (f ; f) ; x) ; (\lambda fx. f' ; (f ; f) ; x)) ; F) ; x \ &= \lambda x. F ; (\texttt{fix} ; F) ; x = \lambda x. F ; N ; x \ &={\eta} F ; N \end{aligned} $$

The lambda-terms we have seen above are fixpoint combinators---the means within lambda-calculus to perform recursion without any special recursive binding constructs.

The Problem with the First Two Combinators

What is the problem with Turing's and Curry's combinators in a practical programming language? Consider what happens when we try to evaluate $\Theta F$:

$$ \begin{aligned} \Theta F &\rightsquigarrow\rightsquigarrow F ; ((\lambda xy. y ; (x ; x ; y)) ; (\lambda xy. y ; (x ; x ; y)) ; F) \ &\rightsquigarrow\rightsquigarrow F ; (F ; ((\lambda xy. y ; (x ; x ; y)) ; (\lambda xy. y ; (x ; x ; y)) ; F)) \ &\rightsquigarrow\rightsquigarrow F ; (F ; (F ; ((\lambda xy. y ; (x ; x ; y)) ; (\lambda xy. y ; (x ; x ; y)) ; F))) \ &\rightsquigarrow\rightsquigarrow \ldots \end{aligned} $$

Recall the distinction between expressions and values from Chapter 3 on Computation. The reduction rule for lambda-calculus is meant to determine which expressions are considered "equal"---it is highly non-deterministic, while on a computer, computation needs to go one way or another.

Using the general reduction rule of lambda-calculus, for a recursive definition, it is always possible to find an infinite reduction sequence. Why? Because we can always choose to reduce the recursive call first, which generates another recursive call, and so on forever. This means a naive lambda-calculus compiler could legitimately generate infinite loops for all recursive definitions---which would not be very useful!

Therefore, we need more specific rules. Most languages use call-by-value (also called eager evaluation):

$$(\texttt{fun } x \texttt{ -> } a) ; v \rightsquigarrow a[x := v]$$

The program eagerly computes arguments before starting to compute the function body. This is exactly the rule we introduced in the Computation chapter.

Call-by-Value Fixpoint Combinator in Action

What happens with the call-by-value fixpoint combinator?

$$ \begin{aligned} \texttt{fix} ; F &\rightsquigarrow (\lambda fx. F ; (f ; f) ; x) ; (\lambda fx. F ; (f ; f) ; x) \ &\rightsquigarrow \lambda x. F ; ((\lambda fx. F ; (f ; f) ; x) ; (\lambda fx. F ; (f ; f) ; x)) ; x \end{aligned} $$

The computation stops because we use the rule $(\texttt{fun } x \texttt{ -> } a) ; v \rightsquigarrow a[x := v]$ rather than $(\texttt{fun } x \texttt{ -> } a_1) ; a_2 \rightsquigarrow a_1[x := a_2]$. The expression inside the lambda is not evaluated until the function is applied.

Let us compute the function on some input:

$$ \begin{aligned} \texttt{fix} ; F ; v &\rightsquigarrow (\lambda fx. F ; (f ; f) ; x) ; (\lambda fx. F ; (f ; f) ; x) ; v \ &\rightsquigarrow (\lambda x. F ; ((\lambda fx. F ; (f ; f) ; x) ; (\lambda fx. F ; (f ; f) ; x)) ; x) ; v \ &\rightsquigarrow F ; ((\lambda fx. F ; (f ; f) ; x) ; (\lambda fx. F ; (f ; f) ; x)) ; v \ &\rightsquigarrow F ; (\lambda x. F ; ((\lambda fx. F ; (f ; f) ; x) ; (\lambda fx. F ; (f ; f) ; x)) ; x) ; v \ &\rightsquigarrow \text{depends on } F \end{aligned} $$

Why "Fixpoint"?

If you examine our derivations, you will see they establish $x = f(x)$. Such values $x$ are called fixpoints of $f$. An arithmetic function can have several fixpoints---for example, $f(x) = x^2$ has fixpoints 0 and 1 (since $0^2 = 0$ and $1^2 = 1$)---or no fixpoints, such as $f(x) = x + 1$ (since $x + 1 \neq x$ for all $x$).

When you define a function (or another object) by recursion, it has a similar meaning: the name appears on both sides of the equality. For example, fact n = if n = 0 then 1 else n * fact (n-1) has fact on both sides. In lambda-calculus, functions like $\Theta$ and $\mathbf{Y}$ take any function as an argument and return its fixpoint.

We turn a specification of a recursive object into a definition by solving it with respect to the recurring name: deriving $x = f(x)$ where $x$ is the recurring name. We then have $x = \texttt{fix}(f)$.

Deriving Factorial

Let us walk through this process step by step for the factorial function. This will show how to transform a recursive specification into a proper definition using fix. We omit the prefix cn_ (could be pn_ if using pair-encoded numbers) and shorten if_then_else to if_t_e:

$$ \begin{aligned} \texttt{fact} ; n &= \texttt{if_t_e} ; (\texttt{is_zero} ; n) ; \texttt{cn1} ; (\texttt{mult} ; n ; (\texttt{fact} ; (\texttt{pred} ; n))) \ \texttt{fact} &= \lambda n. \texttt{if_t_e} ; (\texttt{is_zero} ; n) ; \texttt{cn1} ; (\texttt{mult} ; n ; (\texttt{fact} ; (\texttt{pred} ; n))) \ \texttt{fact} &= (\lambda fn. \texttt{if_t_e} ; (\texttt{is_zero} ; n) ; \texttt{cn1} ; (\texttt{mult} ; n ; (f ; (\texttt{pred} ; n)))) ; \texttt{fact} \ \texttt{fact} &= \texttt{fix} ; (\lambda fn. \texttt{if_t_e} ; (\texttt{is_zero} ; n) ; \texttt{cn1} ; (\texttt{mult} ; n ; (f ; (\texttt{pred} ; n)))) \end{aligned} $$

The last line is a valid definition: we simply give a name to a ground (also called closed) expression---one with no free variables. We have already seen how fix works in the reduction semantics.

Exercise: Hand-Reduce fact cn2

Compute fact cn2 by hand, tracing through the reduction steps.

Exercise: Fixed Point of Successor

What does fix (fun x -> cn_succ x) mean? What happens if you try to evaluate it? Think about whether there is any value x such that x = cn_succ x.

4.8 Encoding Lists and Trees

Now that we have numbers and recursion, we can encode more complex data structures. The pattern we have seen with booleans and pairs extends naturally to algebraic data types like lists and trees.

A list is either empty (often called Empty or Nil) or consists of an element followed by another list (the "tail"), called Cons. Since lists have two variants, we encode them with two-argument selector functions:

• nil $= \lambda xy.y$ (select the second argument, like c_false)
• cons $H ; T = \lambda xy. x ; H ; T$ (apply the first argument to head and tail)

With these definitions, we can write a function to add all numbers stored inside a list:

$$\texttt{addlist} ; l = l ; (\lambda h t. \texttt{cn_add} ; h ; (\texttt{addlist} ; t)) ; \texttt{cn0}$$

To make a proper definition, we apply $\texttt{fix}$ to the solution of the above equation:

$$\texttt{addlist} = \texttt{fix} ; (\lambda f l. l ; (\lambda h t. \texttt{cn_add} ; h ; (f ; t)) ; \texttt{cn0})$$

For trees, let us use a different form of binary trees than we have seen before: instead of keeping elements in inner nodes, we will keep elements in leaves. This is sometimes called an "external" tree structure.

Again, we have two variants, so we use two-argument selector functions:

• leaf $n = \lambda xy. x ; n$ (apply first argument to the element)
• node $L ; R = \lambda xy. y ; L ; R$ (apply second argument to left and right subtrees)

To add numbers stored inside a tree:

$$\texttt{addtree} ; t = t ; (\lambda n.n) ; (\lambda l r. \texttt{cn_add} ; (\texttt{addtree} ; l) ; (\texttt{addtree} ; r))$$

And in solved form:

$$\texttt{addtree} = \texttt{fix} ; (\lambda f t. t ; (\lambda n.n) ; (\lambda l r. \texttt{cn_add} ; (f ; l) ; (f ; r)))$$

let rec fix f x = f (fix f) x
let nil = fun x y -> y
let cons h t = fun x y -> x h t
let addlist l =
  fix (fun f l -> l (fun h t -> cn_add h (f t)) cn0) l
;;
decode_cnat
  (addlist (cons cn1 (cons cn2 (cons cn7 nil))));;
let leaf n = fun x y -> x n
let node l r = fun x y -> y l r
let addtree t =
  fix (fun f t ->
    t (fun n -> n) (fun l r -> cn_add (f l) (f r))
  ) t
;;
decode_cnat
  (addtree (node (node (leaf cn3) (leaf cn7))
              (leaf cn1)));;

The General Pattern

If you look back at our encodings, you will observe a consistent pattern: when we encode a variant type with $n$ variants, for each variant we define a function that takes $n$ arguments.

If the $k$th variant $C_k$ has $m_k$ parameters, then the function $c_k$ that encodes it has the form:

$$C_k(v_1, \ldots, v_{m_k}) \sim c_k ; v_1 ; \ldots ; v_{m_k} = \lambda x_1 \ldots x_n. x_k ; v_1 ; \ldots ; v_{m_k}$$

The encoded variants serve as shallow pattern matching with guaranteed exhaustiveness: the $k$th argument corresponds to the $k$th branch of pattern matching. This is exactly how match works in OCaml, but encoded purely with functions!

4.9 Looping Recursion

We have been coding in untyped lambda-calculus and verifying our code works in OCaml. But there is a subtle trap we must be aware of when combining lambda-calculus encodings with OCaml's eager evaluation.

Let us return to pair-encoded numbers and define addition:

let pn_add m n =
  fix (fun f m n ->
    if_then_else (pn_is_zero m)
      n (pn_succ (f (pn_pred m) n))
  ) m n;;
decode_pnat (pn_add pn3 pn3);;

Oops... OCaml says: Stack overflow during evaluation (looping recursion?).

What went wrong? Nothing as far as lambda-calculus is concerned---the definition is mathematically correct. But OCaml (and F#) always compute arguments before calling a function. This is the eager evaluation strategy we discussed earlier. By definition of fix, f corresponds to recursively calling pn_add. Therefore, (pn_succ (f (pn_pred m) n)) will be evaluated regardless of what (pn_is_zero m) returns!

In other words, even when m is zero and we should return n, OCaml first tries to compute the "else" branch, which makes a recursive call, which computes its "else" branch, and so on forever.

Why do addlist and addtree work? Look at them carefully: their recursive calls are "guarded" by corresponding fun. The expression (fun h t -> cn_add h (f t)) does not immediately call f---it creates a function that will call f only when that function is applied to arguments. What is inside of fun is not computed immediately---only when the function is applied to argument(s).

To avoid looping recursion, you need to guard all recursive calls. Besides putting them inside fun, in OCaml or F# you can also put them in branches of a match clause, as long as one of the branches does not have unguarded recursive calls.

The trick for functions like if_then_else is to guard their arguments with fun x ->, where x is not used, and apply the result of if_then_else to some dummy value. This delays the evaluation of both branches until the boolean has selected one of them:

let id x = x
let rec fix f x = f (fix f) x
let pn1 x = pn_succ pn0 x
let pn2 x = pn_succ pn1 x
let pn3 x = pn_succ pn2 x
let pn7 x = encode_pnat 7 x
let pn_add m n =
  fix (fun f m n ->
    (if_then_else (pn_is_zero m)
       (fun x -> n) (fun x -> pn_succ (f (pn_pred m) n)))
      id
  ) m n;;
decode_pnat (pn_add pn3 pn3);;
decode_pnat (pn_add pn3 pn7);;

Now the recursive call is wrapped in fun x ->, so it is not evaluated until if_then_else selects the second branch and applies it to id. When m is zero, the first branch (fun x -> n) is selected and applied to id, giving us n without ever touching the recursive call.

In OCaml or F# we would typically guard by fun () -> and then apply to (), but we do not have datatypes like unit in pure lambda-calculus, so we use id as our dummy value.

4.10 Exercises

The following exercises will help solidify your understanding of lambda-calculus encodings. For each exercise involving lambda-calculus, test your implementation by encoding some inputs, applying your function, and decoding the result.

Exercise 1: Core Lambda Encodings

Define (implement) and test on a couple of examples functions corresponding to or computing:

1. c_or and c_not;
2. exponentiation for Church numerals;
3. is-zero predicate for Church numerals;
4. even-number predicate for Church numerals;
5. multiplication for pair-encoded natural numbers;
6. factorial $n!$ for pair-encoded natural numbers;
7. the length of a list (in Church numerals);
8. cn_max -- maximum of two Church numerals;
9. the depth of a tree (in Church numerals).

Exercise 2: Numeral-like Lambda Terms

Construct lambda-terms $m_0, m_1, \ldots$ such that for all $n$ one has:

$$ \begin{aligned} m_0 &= x \ m_{n+1} &= m_{n+2} ; m_n \end{aligned} $$

(where equality is after performing $\beta$-reductions).

Exercise 3: State-Passing Imperative Constructs

Representing side-effects as an explicitly "passed around" state value, write (higher-order) functions that represent the imperative constructs:

1. for...to...
2. for...downto...
3. while...do...
4. do...while...
5. repeat...until...

Rather than writing a lambda-term using the encodings that we have learnt, just implement the functions in OCaml / F#, using built-in int and bool types. You can use let rec instead of fix.

• For example, in exercise (a), write a function let rec for_to f beg_i end_i s = ... where f takes arguments i ranging from beg_i to end_i, state s at given step, and returns state s at next step; the for_to function returns the state after the last step.
• And in exercise (c), write a function let rec while_do p f s = ... where both p and f take state s at given step, and if p s returns true, then f s is computed to obtain state at next step; the while_do function returns the state after the last step.

Do not use the imperative features of OCaml and F#! This exercise demonstrates that imperative control flow can be encoded purely functionally by threading state through function calls.

Although we will not cover imperative features in this course, it is instructive to see the implementation using them, to better understand what is actually required of a solution to Exercise 3:

(* (a) *)
let for_to f beg_i end_i s =
  let s = ref s in
  for i = beg_i to end_i do
    s := f i !s
  done;
  !s

(* (b) *)
let for_downto f beg_i end_i s =
  let s = ref s in
  for i = beg_i downto end_i do
    s := f i !s
  done;
  !s

(* (c) *)
let while_do p f s =
  let s = ref s in
  while p !s do
    s := f !s
  done;
  !s

(* (d) *)
let do_while p f s =
  let s = ref (f s) in
  while p !s do
    s := f !s
  done;
  !s

(* (e) *)
let repeat_until p f s =
  let s = ref (f s) in
  while not (p !s) do
    s := f !s
  done;
  !s

Chapter 5: Polymorphism and Abstract Data Types

{.chapter-image}

In this chapter, you will:

• Understand “unknowns vs parameters” in OCaml’s inferred types (and why the value restriction exists)
• Connect type inference to solving constraint systems (unification intuition)
• Use parametric types to design reusable, type-safe data structures
• Specify ADTs algebraically and implement maps with increasing efficiency (lists → BSTs → red-black trees)

This chapter explores how OCaml's type system supports generic programming through parametric polymorphism, and how abstract data types provide clean interfaces for data structures. We begin by examining how type inference actually works -- the process by which OCaml determines types for your code. Then we explore parametric types and show how they enable polymorphic functions to work with data of any shape. The second half of the chapter introduces algebraic specifications, the mathematical foundation for describing data structures, and applies these concepts to build progressively more sophisticated implementations of the map (dictionary) data structure, culminating in the elegant red-black tree.

Reader feedback welcome: if you spot an error or unclear passage, please report it.

5.1 Type Inference

We have seen the rules that govern the assignment of types to expressions, but how does OCaml actually guess what types to use? And how does it know when no correct types exist? The answer lies in a beautiful algorithm: OCaml solves equations. When you write code, the type checker generates a set of equations that must hold for the program to be well-typed, and then it solves those equations to discover the types.

Variables: Unknowns and Parameters

Variables in type inference play two distinct roles, and understanding this distinction is crucial for mastering OCaml's type system. A type variable can be either an unknown (standing for a specific but not-yet-determined type) or a parameter (standing for any type whatsoever).

Consider this example:

# let f = List.hd;;
val f : 'a list -> 'a = <fun>

Here 'a is a parameter: it can become any type. When you use f with a list of integers, 'a becomes int; when you use it with a list of strings, 'a becomes string. Mathematically we write: $f : \forall \alpha . \alpha \ \text{list} \rightarrow \alpha$ -- the quantified type is called a type scheme. The $\forall$ symbol indicates that this type works "for all" choices of $\alpha$.

In contrast, consider this example:

# let x = ref [];;
val x : '_weak1 list ref = {contents = []}

Here '_a (displayed as '_weak1 in recent OCaml versions) is an unknown. Unlike a parameter, it stands for a particular type -- perhaps float or int -> int -- but OCaml simply doesn't know which type yet. The underscore prefix signals this distinction. OCaml reports unknowns like '_a in inferred types for reasons related to mutable state (the "value restriction"), which are not relevant to purely functional programming.

More precisely: the value restriction prevents unsoundness that would otherwise arise from generalizing type variables in effectful (mutable) expressions. When you see '_weak..., treat it as “this will become one specific type later”.

When unknowns appear in inferred types against our expectations, $\eta$-expansion may help. This technique involves writing let f x = expr x instead of let f = expr, essentially adding an extra parameter that gets immediately applied. For example:

# let f = List.append [];;
val f : '_weak2 list -> '_weak2 list = <fun>
# let f l = List.append [] l;;
val f : 'a list -> 'a list = <fun>

In the second definition, the eta-expanded form let f l = List.append [] l allows full generalization, giving us a truly polymorphic function that can work with lists of any type.

Type Environments

Before diving into the equation-solving process, we need to understand how the type checker keeps track of what names are available. A type environment specifies what names (corresponding to parameters and definitions) are available for an expression because they were introduced above it, and it specifies their types. Think of it as a dictionary that maps variable names to their types at any given point in your program.

Solving Type Equations

Type inference works by solving equations over unknowns. The central question the algorithm asks is: "What has to hold so that $e : \tau$ in type environment $\Gamma$?" The answer takes the form of equations that constrain the possible types.

Let us walk through how the algorithm handles different expression forms:

• If, for example, $f : \forall \alpha . \alpha \ \text{list} \rightarrow \alpha \in \Gamma$, then for $f : \tau$ we introduce $\gamma \ \text{list} \rightarrow \gamma = \tau$ for some fresh unknown $\gamma$.

• For function application $e_1 \ e_2 : \tau$, we introduce $\beta = \tau$ and ask for $e_1 : \gamma \rightarrow \beta$ and $e_2 : \gamma$, for some fresh unknowns $\beta, \gamma$.

• For a function $\text{fun} \ x \rightarrow e : \tau$, we introduce $\beta \rightarrow \gamma = \tau$ and ask for $e : \gamma$ in environment ${x : \beta} \cup \Gamma$, for some fresh unknowns $\beta, \gamma$.

• The case $\text{let} \ x = e_1 \ \text{in} \ e_2 : \tau$ is different. One approach is to first solve the equations that we get by asking for $e_1 : \beta$, for some fresh unknown $\beta$. Let us say a solution $\beta = \tau_\beta$ has been found, $\alpha_1 \ldots \alpha_n \beta_1 \ldots \beta_m$ are the remaining unknowns in $\tau_\beta$, and $\alpha_1 \ldots \alpha_n$ are all that do not appear in $\Gamma$. Then we ask for $e_2 : \tau$ in environment ${x : \forall \alpha_1 \ldots \alpha_n . \tau_\beta} \cup \Gamma$.

• Remember that whenever we establish a solution $\beta = \tau_\beta$ to an unknown $\beta$, it takes effect everywhere! The substitution propagates through all the equations, potentially triggering further unifications.

• To find a type for $e$ (in environment $\Gamma$), we pick a fresh unknown $\beta$ and ask for $e : \beta$ (in $\Gamma$). The algorithm then generates and solves equations until either a solution is found or a contradiction reveals a type error.

Polymorphism

The "top-level" definitions for which the system infers types with variables are called polymorphic, which informally means "working with different shapes of data." A polymorphic function like List.hd can operate on lists containing any type of element -- the function itself doesn't care what the elements are, only that it's working with a list.

This kind of polymorphism is called parametric polymorphism, since the types have parameters. The term "parametric" emphasizes that the same code works uniformly for all type instantiations. A different kind of polymorphism is provided by object-oriented programming languages (sometimes called subtype polymorphism or ad-hoc polymorphism), where different code may execute depending on the runtime type of objects.

5.2 Parametric Types

Polymorphic functions truly shine when used with polymorphic data types. The combination of the two is what makes ML-family languages so expressive. Consider this definition of our own list type:

type 'a my_list = Empty | Cons of 'a * 'a my_list

We define lists that can store elements of any type 'a. The type parameter 'a acts as a placeholder that gets filled in when we create actual lists. Now we can write functions that work on these lists:

# let tail l =
    match l with
    | Empty -> invalid_arg "tail"
    | Cons (_, tl) -> tl;;
val tail : 'a my_list -> 'a my_list = <fun>

This is a polymorphic function: it works for lists with elements of any type. Whether we have a list of integers, strings, or even lists of lists, the same tail function handles them all.

A crucial point to understand: a parametric type like 'a my_list is not itself a data type but rather a family of data types. The types bool my_list, int my_list, etc. are different types -- you cannot mix elements of different types in a single list. We say that the type int my_list instantiates the parametric type 'a my_list.

Multiple Type Parameters

Types can have multiple type parameters. In OCaml, the syntax might seem a bit unusual at first: type parameters precede the type name, enclosed in parentheses. For example:

type ('a, 'b) choice = Left of 'a | Right of 'b

This type has two parameters and represents a value that is either something of type 'a (wrapped in Left) or something of type 'b (wrapped in Right). Mathematically we would write $\text{choice}(\alpha, \beta)$.

Not all functions that use parametric types need to be polymorphic. A function may constrain the type parameters to specific types:

# let get_int c =
    match c with
    | Left i -> i
    | Right b -> if b then 1 else 0;;
val get_int : (int, bool) choice -> int = <fun>

Here, the pattern matching on Left i and Right b with arithmetic operations constrains the type to (int, bool) choice.

Syntax in Other Languages

Different functional languages have different syntactic conventions for type parameters. In F#, we provide parameters (when more than one) after the type name, using angle brackets:

type choice<'a,'b> = Left of 'a | Right of 'b

In Haskell, the syntax is arguably the cleanest -- we provide type parameters similarly to function arguments, separated by spaces:

data Choice a b = Left a | Right b

Despite the syntactic differences, the underlying concept of parametric polymorphism is the same across all these languages.

5.3 Type Inference, Formally

Now we present a more formal treatment of type inference. A statement that an expression has a type in an environment is called a type judgement. For environment $\Gamma = {x : \forall \alpha_1 \ldots \alpha_n . \tau_x ; \ldots}$, expression $e$ and type $\tau$ we write:

$$\Gamma \vdash e : \tau$$

This notation reads: "In environment $\Gamma$, expression $e$ has type $\tau$." The turnstile symbol $\vdash$ can be thought of as "entails" or "proves."

We will derive all the constraint equations in one go using the notation $[![ \cdot ]!]$, to be solved later by unification. Besides equations we will need to manage introduced variables, using existential quantification to express that "there exists some type variable satisfying these constraints."

For local definitions we require remembering what constraints should hold when the definition is used. Therefore we extend type schemes in the environment to: $\Gamma = {x : \forall \beta_1 \ldots \beta_m [\exists \alpha_1 \ldots \alpha_n . D] . \tau_x ; \ldots}$ where $D$ are equations -- keeping the variables $\alpha_1 \ldots \alpha_n$ introduced while deriving $D$ in front. A simpler form would be sufficient: $\Gamma = {x : \forall \beta [\exists \alpha_1 \ldots \alpha_n . D] . \beta ; \ldots}$

The formal constraint generation rules are:

$$[![ \Gamma \vdash x : \tau ]!] = \exists \overline{\beta'} \overline{\alpha'} . (D[\overline{\beta} \overline{\alpha} := \overline{\beta'} \overline{\alpha'}] \wedge \tau_x[\overline{\beta} \overline{\alpha} := \overline{\beta'} \overline{\alpha'}] \doteq \tau)$$

where $\Gamma(x) = \forall \overline{\beta} [\exists \overline{\alpha} . D] . \tau_x$, $\overline{\beta'} \overline{\alpha'} # \text{FV}(\Gamma, \tau)$

$$[![ \Gamma \vdash \mathbf{fun} \ x \texttt{->} e : \tau ]!] = \exists \alpha_1 \alpha_2 . ([![ \Gamma {x : \alpha_1} \vdash e : \alpha_2 ]!] \wedge \alpha_1 \rightarrow \alpha_2 \doteq \tau)$$

where $\alpha_1 \alpha_2 # \text{FV}(\Gamma, \tau)$

$$[![ \Gamma \vdash e_1 \ e_2 : \tau ]!] = \exists \alpha . ([![ \Gamma \vdash e_1 : \alpha \rightarrow \tau ]!] \wedge [![ \Gamma \vdash e_2 : \alpha ]!]), \alpha # \text{FV}(\Gamma, \tau)$$

$$[![ \Gamma \vdash K \ e_1 \ldots e_n : \tau ]!] = \exists \overline{\alpha'} . (\bigwedge_i [![ \Gamma \vdash e_i : \tau_i[\overline{\alpha} := \overline{\alpha'}] ]!] \wedge \varepsilon(\overline{\alpha'}) \doteq \tau)$$

where $K : \forall \overline{\alpha} . \tau_1 \times \ldots \times \tau_n \rightarrow \varepsilon(\overline{\alpha})$, $\overline{\alpha'} # \text{FV}(\Gamma, \tau)$

For let-expressions:

$$[![ \Gamma \vdash \mathbf{let} \ x = e_1 \ \mathbf{in} \ e_2 : \tau ]!] = (\exists \beta . C) \wedge [![ \Gamma {x : \forall \beta [C] . \beta} \vdash e_2 : \tau ]!]$$

where $C = [![ \Gamma \vdash e_1 : \beta ]!]$

For recursive let-expressions:

$$[![ \Gamma \vdash \mathbf{letrec} \ x = e_1 \ \mathbf{in} \ e_2 : \tau ]!] = (\exists \beta . C) \wedge [![ \Gamma {x : \forall \beta [C] . \beta} \vdash e_2 : \tau ]!]$$

where $C = [![ \Gamma {x : \beta} \vdash e_1 : \beta ]!]$

For match expressions:

$$[![ \Gamma \vdash \mathbf{match} \ e_v \ \mathbf{with} \ \overline{c} : \tau ]!] = \exists \alpha_v . [![ \Gamma \vdash e_v : \alpha_v ]!] \bigwedge_i [![ \Gamma \vdash p_i . e_i : \alpha_v \rightarrow \tau ]!]$$

where $\overline{c} = p_1 . e_1 | \ldots | p_n . e_n$, $\alpha_v # \text{FV}(\Gamma, \tau)$

For pattern clauses:

$$[![ \Gamma, \Sigma \vdash p.e : \tau_1 \rightarrow \tau_2 ]!] = [![ \Sigma \vdash p \downarrow \tau_1 ]!] \wedge \forall \overline{\beta} . [![ \Gamma \Gamma' \vdash e : \tau_2 ]!]$$

where $\exists \overline{\beta} \Gamma'$ is $[![ \Sigma \vdash p \uparrow \tau_1 ]!]$, $\overline{\beta} # \text{FV}(\Gamma, \tau_2)$

The notation $[![ \Sigma \vdash p \downarrow \tau_1 ]!]$ derives constraints on the type of the matched value, while $[![ \Sigma \vdash p \uparrow \tau_1 ]!]$ derives the environment for pattern variables.

By $\overline{\alpha}$ or $\overline{\alpha_i}$ we denote a sequence of some length: $\alpha_1 \ldots \alpha_n$. By $\bigwedge_i \varphi_i$ we denote a conjunction of $\overline{\varphi_i}$: $\varphi_1 \wedge \ldots \wedge \varphi_n$.

Polymorphic Recursion

There is an interesting limitation in standard type inference for recursive functions. Note the limited polymorphism of let rec f = ... -- we cannot use f polymorphically within its own definition. Why? Because when type-checking the body of a recursive definition, we don't yet know the final type of f, so we must treat it as having a single, unknown type.

In modern OCaml we can bypass this limitation if we provide the type of f upfront:

let rec f : 'a. 'a -> 'a list = ...

where 'a. 'a -> 'a list stands for $\forall \alpha . \alpha \rightarrow \alpha \ \text{list}$.

Using the recursively defined function with different types in its definition is called polymorphic recursion. It is most useful together with irregular recursive datatypes -- data structures where the recursive use has different type arguments than the actual parameters. These "nested" or "non-uniform" datatypes enable some remarkably elegant data structures.

Example: A List Alternating Between Two Types of Elements

Here is a fascinating example: a list that alternates between two different types of elements. Notice how the recursive occurrence swaps the type parameters:

type ('x, 'o) alternating =
  | Stop
  | One of 'x * ('o, 'x) alternating

let rec to_list :
    'x 'o 'a. ('x -> 'a) -> ('o -> 'a) ->
              ('x, 'o) alternating -> 'a list =
  fun x2a o2a ->
    function
    | Stop -> []
    | One (x, rest) -> x2a x :: to_list o2a x2a rest

let to_choice_list alt =
  to_list (fun x -> Left x) (fun o -> Right o) alt

let it = to_choice_list
  (One (1, One ("o", One (2, One ("oo", Stop)))))

Notice how the recursive call to to_list swaps o2a and x2a -- this is necessary because the alternating structure swaps the type parameters at each level. The polymorphic recursion annotation 'x 'o 'a. tells OCaml that we need to use to_list at different type instantiations within its own definition.

Example: Data-Structural Bootstrapping

Here is another powerful example of polymorphic recursion: a sequence data structure that stores elements in exponentially increasing chunks. This technique, known as data-structural bootstrapping, achieves logarithmic-time random access -- much faster than standard lists which require linear time.

type 'a seq =
  | Nil
  | Zero of ('a * 'a) seq
  | One of 'a * ('a * 'a) seq

The key insight is that this type is non-uniform: the recursive occurrences use ('a * 'a) seq rather than 'a seq. This means that as we go deeper into the structure, elements get paired together, effectively doubling the "width" at each level. We store a list of elements in exponentially increasing chunks:

let example =
  One (0, One ((1,2), Zero (One ((((3,4),(5,6)), ((7,8),(9,10))), Nil))))

The cons operation adds an element to the front. Remarkably, appending an element to this data structure works exactly like adding one to a binary number:

let rec cons : 'a. 'a -> 'a seq -> 'a seq =
  fun x -> function
  | Nil -> One (x, Nil)                       (* 1+0=1 *)
  | Zero ps -> One (x, ps)                    (* 1+...0=...1 *)
  | One (y, ps) -> Zero (cons (x,y) ps)       (* 1+...1=[...+1]0 *)

let rec lookup : 'a. int -> 'a seq -> 'a =
  fun i s -> match i, s with
  | _, Nil -> raise Not_found              (* Rather than returning None : 'a option *)
  | 0, One (x, _) -> x                     (* we raise exception, for convenience. *)
  | i, One (_, ps) -> lookup (i-1) (Zero ps)
  | i, Zero ps ->                          (* Random-access lookup works *)
      let x, y = lookup (i / 2) ps in      (* in logarithmic time -- much faster *)
      if i mod 2 = 0 then x else y         (* than in standard lists. *)

The Zero and One constructors correspond to binary digits. A Zero means "no singleton element at this level," while One carries a singleton (or pair, or quad, etc.) before recursing. The lookup function exploits this structure: when looking up index i in a Zero ps, it divides by 2 and looks in the paired structure, then extracts the appropriate half of the pair.

5.4 Algebraic Specification

Now we turn to a fundamental question in computer science: how do we formally describe what a data structure is and what it should do? The mathematical answer is algebraic specification.

The way we introduce a data structure, like complex numbers or strings, in mathematics is by specifying an algebraic structure. This approach gives us a precise language for describing data structures independent of any particular implementation.

Algebraic structures consist of a set (or several sets, for so-called multisorted algebras) and a bunch of functions (also known as operations) over this set (or sets). Think of integers with addition and multiplication, or strings with concatenation and character access.

A signature is a rough description of an algebraic structure: it provides sorts -- names for the sets (in the multisorted case) -- and names of the functions-operations together with their arity (and what sorts of arguments they take). A signature tells us what operations exist, but not how they behave.

We select a class of algebraic structures by providing axioms that have to hold. We will call such classes algebraic specifications. In mathematics, a rusty name for some algebraic specifications is a variety; a more modern name is algebraic category.

Here is the key connection to programming: algebraic structures correspond to "implementations" and signatures to "interfaces" in programming languages. We will say that an algebraic structure implements an algebraic specification when all axioms of the specification hold in the structure. An important point: all algebraic specifications are implemented by multiple structures! This is precisely what we want -- it gives us the freedom to choose different implementations with different performance characteristics while maintaining the same interface.

We say that an algebraic structure does not have junk when all its elements (i.e., elements in the sets corresponding to sorts) can be built using operations in its signature. Junk-free structures are "minimal" in some sense -- they contain only the values that can be constructed using the provided operations.

We allow parametric types as sorts. In that case, strictly speaking, we define a family of algebraic specifications (a different specification for each instantiation of the parametric type).

Algebraic Specifications: Examples

Let us look at some concrete examples to make these abstract ideas tangible. An algebraic specification can also use an earlier specification, building up complexity layer by layer. In "impure" languages like OCaml and F# we allow that the result of any operation be an $\text{error}$. In Haskell we would use Maybe to explicitly model potential failure.

Specification $\text{nat}_p$ (bounded natural numbers):

This specification describes natural numbers that wrap around at some bound $p$ (like machine integers):

The axioms define how addition and multiplication work recursively, and the last two axioms capture the bounded nature: applying $\text{succ}$ less than $p$ times never gives zero, but exactly $p$ times wraps around to zero.

Specification $\text{string}_p$ (bounded strings):

This specification describes strings with a maximum length $p$:

The axioms specify that concatenation is associative, that the empty string is an identity for concatenation, that exceeding the length limit produces an error, and that indexing works by stripping characters from the front.

5.5 Homomorphisms

When do two implementations of the same specification "behave the same"? The mathematical answer involves homomorphisms -- structure-preserving mappings between algebraic structures.

Homomorphisms are mappings between algebraic structures with the same signature that preserve operations. Intuitively, if you apply an operation and then map, you get the same result as mapping first and then applying the corresponding operation.

A homomorphism from algebraic structure $(A, {f^A, g^A, \ldots})$ to $(B, {f^B, g^B, \ldots})$ is a function $h : A \rightarrow B$ such that:

• $h(f^A(a_1, \ldots, a_{n_f})) = f^B(h(a_1), \ldots, h(a_{n_f}))$ for all $(a_1, \ldots, a_{n_f})$
• $h(g^A(a_1, \ldots, a_{n_g})) = g^B(h(a_1), \ldots, h(a_{n_g}))$ for all $(a_1, \ldots, a_{n_g})$
• and so on for all operations.

Two algebraic structures are isomorphic if there are homomorphisms $h_1 : A \rightarrow B$, $h_2 : B \rightarrow A$ from one to the other and back, that when composed in any order form identity: $\forall (b \in B) \ h_1(h_2(b)) = b$ and $\forall (a \in A) \ h_2(h_1(a)) = a$.

An algebraic specification whose all implementations without junk are isomorphic is called "monomorphic". This means the specification pins down the structure so precisely that there's essentially only one way to implement it (up to isomorphism).

We usually only add axioms that really matter to us to the specification, so that the implementations have room for optimization. For this reason, the resulting specifications will often not be monomorphic in the above sense -- and that's intentional! A non-monomorphic specification allows for multiple genuinely different implementations, which may have different performance characteristics.

5.6 Example: Maps

Now let us look at a practical example that will guide the rest of this chapter. A map (also called dictionary or associative array) associates keys with values. This is one of the most fundamental data structures in programming -- think of Python's dictionaries, Java's HashMap, or OCaml's Map module.

Here is an algebraic specification that captures the essential behavior of maps:

The axioms capture the intuitive behavior: adding a key-value pair makes that key findable, removing a key makes it unfindable, and operations on different keys don't interfere with each other. Notice how the specification says nothing about how the map is implemented -- only about what behavior it must exhibit.

5.7 Modules and Interfaces (Signatures): Syntax

How do we express algebraic specifications in OCaml? The answer is the module system. In the ML family of languages, structures are given names by module bindings, and signatures are types of modules. From outside of a structure or signature, we refer to the values or types it provides with a dot notation: Module.value.

Module (and module type) names have to start with a capital letter (in ML languages). Since modules and module types have names, there is a convention to name the central type of a signature (the one that is "specified" by the signature), for brevity, t. Module types are often named with "all-caps" (all letters upper case).

Here is how we translate our map specification into an OCaml module signature:

module type MAP = sig
  type ('a, 'b) t
  val empty : ('a, 'b) t
  val member : 'a -> ('a, 'b) t -> bool
  val add : 'a -> 'b -> ('a, 'b) t -> ('a, 'b) t
  val remove : 'a -> ('a, 'b) t -> ('a, 'b) t
  val find : 'a -> ('a, 'b) t -> 'b
end

module ListMap : MAP = struct
  type ('a, 'b) t = ('a * 'b) list
  let empty = []
  let member = List.mem_assoc
  let add k v m = (k, v)::m
  let remove = List.remove_assoc
  let find = List.assoc
end

The ListMap module implements MAP using OCaml's built-in list functions for association lists. The type annotation : MAP after the module name tells OCaml to check that the implementation provides everything the signature requires, and hides any additional details.

5.8 Implementing Maps: Association Lists

Let us now build an implementation of maps from the ground up, exploring different approaches and their trade-offs. The most straightforward implementation... might not be what you expected:

module TrivialMap : MAP = struct
  type ('a, 'b) t =
    | Empty
    | Add of 'a * 'b * ('a, 'b) t
    | Remove of 'a * ('a, 'b) t

  let empty = Empty

  let rec member k m =
    match m with
    | Empty -> false
    | Add (k2, _, _) when k = k2 -> true
    | Remove (k2, _) when k = k2 -> false
    | Add (_, _, m2) -> member k m2
    | Remove (_, m2) -> member k m2

  let add k v m = Add (k, v, m)
  let remove k m = Remove (k, m)

  let rec find k m =
    match m with
    | Empty -> raise Not_found
    | Add (k2, v, _) when k = k2 -> v
    | Remove (k2, _) when k = k2 -> raise Not_found
    | Add (_, _, m2) -> find k m2
    | Remove (_, m2) -> find k m2
end

This "trivial" implementation is quite clever in its own way: it simply records all operations as a log! The data structure itself is a history of everything that has been done to it. The add and remove operations are $O(1)$ -- they just prepend a new node. However, member and find must traverse the entire history to determine the current state, giving them $O(n)$ complexity where $n$ is the number of operations performed.

This implementation illustrates an important point: there are many ways to satisfy the same specification, with very different performance characteristics.

Here is a more conventional implementation based on association lists, i.e., on lists of key-value pairs without the Remove constructor:

module MyListMap : MAP = struct
  type ('a, 'b) t = Empty | Add of 'a * 'b * ('a, 'b) t

  let empty = Empty

  let rec member k m =
    match m with
    | Empty -> false
    | Add (k2, _, _) when k = k2 -> true
    | Add (_, _, m2) -> member k m2

  let rec add k v m =
    match m with
    | Empty -> Add (k, v, Empty)
    | Add (k2, _, m) when k = k2 -> Add (k, v, m)
    | Add (k2, v2, m) -> Add (k2, v2, add k v m)

  let rec remove k m =
    match m with
    | Empty -> Empty
    | Add (k2, _, m) when k = k2 -> m
    | Add (k2, v, m) -> Add (k2, v, remove k m)

  let rec find k m =
    match m with
    | Empty -> raise Not_found
    | Add (k2, v, _) when k = k2 -> v
    | Add (_, _, m2) -> find k m2
end

This implementation maintains the invariant that each key appears at most once in the structure. The add function replaces an existing key's value rather than creating a duplicate, and remove actually removes the key-value pair. All operations are still $O(n)$ in the worst case, but the structure stays cleaner.

5.9 Implementing Maps: Binary Search Trees

Can we do better than linear time? Yes, by using a smarter data structure. Binary search trees are binary trees with elements stored at the interior nodes, such that elements to the left of a node are smaller than, and elements to the right bigger than, elements within a node. This ordering property is what makes them efficient.

For maps, we store key-value pairs as elements in binary search trees, and compare the elements by keys alone. The tree structure allows us to use "divide-and-conquer" to search for the value associated with a key.

On average, binary search trees are fast -- $O(\log n)$ complexity for all operations. At each node, we can eliminate half the remaining elements from consideration. However, in the worst case (when keys are inserted in sorted order), the tree degenerates into a linked list and operations become $O(n)$.

A note on our design: the simple polymorphic signature for maps is only possible because OCaml provides polymorphic comparison (and equality) operators that work on elements of most types (but not on functions). These operators may not behave as you expect for all types! Our signature for polymorphic maps is not the standard approach because of this limitation; it is just to keep things simple for pedagogical purposes.

module BTreeMap : MAP = struct
  type ('a, 'b) t = Empty | T of ('a, 'b) t * 'a * 'b * ('a, 'b) t

  let empty = Empty

  let rec member k m =              (* "Divide and conquer" search through the tree. *)
    match m with
    | Empty -> false
    | T (_, k2, _, _) when k = k2 -> true
    | T (m1, k2, _, _) when k < k2 -> member k m1
    | T (_, _, _, m2) -> member k m2

  let rec add k v m =               (* Searches the tree in the same way as member *)
    match m with                    (* but copies every node along the way. *)
    | Empty -> T (Empty, k, v, Empty)
    | T (m1, k2, _, m2) when k = k2 -> T (m1, k, v, m2)
    | T (m1, k2, v2, m2) when k < k2 -> T (add k v m1, k2, v2, m2)
    | T (m1, k2, v2, m2) -> T (m1, k2, v2, add k v m2)

  let rec split_rightmost m =       (* A helper function, it does not belong *)
    match m with                    (* to the "exported" signature. *)
    | Empty -> raise Not_found
    | T (Empty, k, v, Empty) -> k, v, Empty   (* We remove one element, *)
    | T (m1, k, v, m2) ->           (* the one that is on the bottom right. *)
        let rk, rv, rm = split_rightmost m2 in
        rk, rv, T (m1, k, v, rm)

  let rec remove k m =
    match m with
    | Empty -> Empty
    | T (m1, k2, _, Empty) when k = k2 -> m1
    | T (Empty, k2, _, m2) when k = k2 -> m2
    | T (m1, k2, _, m2) when k = k2 ->
        let rk, rv, rm = split_rightmost m1 in
        T (rm, rk, rv, m2)
    | T (m1, k2, v, m2) when k < k2 -> T (remove k m1, k2, v, m2)
    | T (m1, k2, v, m2) -> T (m1, k2, v, remove k m2)

  let rec find k m =
    match m with
    | Empty -> raise Not_found
    | T (_, k2, v, _) when k = k2 -> v
    | T (m1, k2, _, _) when k < k2 -> find k m1
    | T (_, _, _, m2) -> find k m2
end

The member and find functions use the "divide-and-conquer" strategy: compare the target key with the key at the current node, and recursively search in the appropriate subtree. The add function searches the tree in the same way but copies every node along the path to create the new tree (since we're using immutable data structures).

The remove function is trickier. When removing a node with two children, we need to replace it with another value that maintains the ordering property. The split_rightmost helper function finds and removes the rightmost (largest) element from a subtree -- this element is guaranteed to be smaller than everything in the right subtree and larger than everything remaining in the left subtree, making it the perfect replacement.

5.10 Implementing Maps: Red-Black Trees

The fatal weakness of ordinary binary search trees is that they can become unbalanced. If keys arrive in sorted order, each insertion adds a node at the bottom of a long chain, and we lose the logarithmic performance guarantee. How can we maintain balance automatically?

This section is based on Wikipedia's Red-black tree article, Chris Okasaki's "Purely Functional Data Structures" and Matt Might's excellent blog post on red-black tree deletion.

Binary search trees are good when we encounter keys in random order, because the cost of operations is limited by the depth of the tree which is small relative to the number of nodes... unless the tree grows unbalanced achieving large depth (which means there are sibling subtrees of vastly different sizes on some path).

To remedy this, we rebalance the tree while building it -- i.e., while adding elements. The key insight is to detect when the tree is becoming unbalanced and perform local rotations to restore balance.

In red-black trees we achieve balance by:

1. Remembering one of two colors (red or black) with each node
2. Keeping the same number of black nodes on every path from the root to a leaf
3. Not allowing a red node to have a red child

These invariants together guarantee that the tree cannot become too unbalanced: the depth is at most twice the depth of a perfectly balanced tree with the same number of nodes. Why? The "black height" (number of black nodes on any root-to-leaf path) is the same everywhere, and red nodes can only appear between black nodes, so the longest path can have at most twice as many nodes as the shortest.

B-trees of Order 4 (2-3-4 Trees)

To understand where red-black trees come from, it helps to first understand 2-3-4 trees (also known as B-trees of order 4).

How can we have perfectly balanced trees without worrying about having exactly $2^k - 1$ elements? The answer is to allow variable-width nodes. 2-3-4 trees can store from 1 to 3 elements in each node and have 2 to 4 subtrees correspondingly. This flexibility lets us maintain perfect balance!

• A 2-node contains one element and has two children
• A 3-node contains two elements and has three children
• A 4-node contains three elements and has four children

To insert into a 2-3-4 tree, we descend toward the appropriate leaf position. But if we encounter a full node (4-node) along the way, we "split" it: move the middle element up to the parent and split the remaining two elements into separate 2-nodes. This maintains perfect balance at all times -- all leaves are at the same depth.

The remarkable fact is that red-black trees are just a clever way to represent 2-3-4 trees as binary trees! To represent a 2-3-4 tree as a binary tree with one element per node, we color the "primary" element of each node black (the middle element of a 4-node, or the first element of a 2-/3-node) and make it the parent of its neighbor elements colored red. The red elements then become parents of the original subtrees. This correspondence provides the deep intuition behind red-black trees: the colors encode the structure of the underlying 2-3-4 tree.

Red-Black Trees, Without Deletion

Now let us implement red-black trees in OCaml. Red-black trees maintain two invariants:

Invariant 1. No red node has a red child. (No two consecutive red nodes on any path.)

Invariant 2. Every path from the root to an empty node contains the same number of black nodes. (The "black height" is uniform.)

For simplicity, we first implement red-black tree based sets (not maps) without deletion. The implementation proceeds almost exactly like for unbalanced binary search trees; we only need to add code to restore the invariants after each insertion.

The beautiful insight of Okasaki's approach is that by keeping balance at each step of constructing a node, it is enough to check locally (around the root of the subtree) whether a violation has occurred. We never need to examine the entire tree. For an understandable implementation of deletion, we need to introduce more colors -- see Matt Might's post for details.

type color = R | B
type 'a t = E | T of color * 'a t * 'a * 'a t

let empty = E

let rec member x m =                     (* Like in unbalanced binary search tree. *)
  match m with
  | E -> false
  | T (_, _, y, _) when x = y -> true
  | T (_, a, y, _) when x < y -> member x a
  | T (_, _, _, b) -> member x b

let balance = function                   (* Restoring the invariants. *)
  | B, T (R, T (R,a,x,b), y, c), z, d    (* On next figure: left, *)
  | B, T (R, a, x, T (R,b,y,c)), z, d    (* top, *)
  | B, a, x, T (R, T (R,b,y,c), z, d)    (* bottom, *)
  | B, a, x, T (R, b, y, T (R,c,z,d))    (* right, *)
      -> T (R, T (B,a,x,b), y, T (B,c,z,d))    (* center tree. *)
  | color, a, x, b -> T (color, a, x, b)   (* We allow red-red violation for now. *)

let insert x s =
  let rec ins = function                 (* Like in unbalanced binary search tree, *)
    | E -> T (R, E, x, E)                (* but fix violation above created node. *)
    | T (color, a, y, b) as s ->
        if x < y then balance (color, ins a, y, b)
        else if x > y then balance (color, a, y, ins b)
        else s
  in
  match ins s with                       (* We could still have red-red violation *)
  | T (_, a, y, b) -> T (B, a, y, b)     (* at root, fixed by coloring it black. *)
  | E -> failwith "insert: impossible"

The balance function is the heart of the algorithm. It handles four cases where a red-red violation occurs (a red node with a red child). The four cases correspond to different positions of the violation:

• A red left child with a red left grandchild
• A red left child with a red right grandchild
• A red right child with a red left grandchild
• A red right child with a red right grandchild

In each case, we perform a "rotation" that restructures the tree to eliminate the violation while maintaining the binary search tree property. Remarkably, all four cases produce the same balanced result: a red root with two black children, with the subtrees a, b, c, d properly distributed.

The insert function works like insertion into an ordinary binary search tree, but calls balance after each recursive step to fix any violations that may have been introduced. New nodes are always created red (which might create a red-red violation that balance will fix). At the very end, we color the root black -- this can never create a violation and ensures the root is always black.

Exercises

Exercise 1: Type Equation Solving

Derive the equations and solve them to find the type for:

let cadr l = List.hd (List.tl l) in cadr (1::2::[]), cadr (true::false::[])

in environment $\Gamma = { \text{List.hd} : \forall \alpha . \alpha \ \text{list} \rightarrow \alpha ; \text{List.tl} : \forall \alpha . \alpha \ \text{list} \rightarrow \alpha \ \text{list} }$. You can take "shortcuts" if it is too many equations to write down.

Exercise 2: Unification Practice

Terms $t_1, t_2, \ldots \in T(\Sigma, X)$ are built out of variables $x, y, \ldots \in X$ and function symbols $f, g, \ldots \in \Sigma$ the way you build values out of functions:

• $X \subset T(\Sigma, X)$ -- variables are terms; usually an infinite set,
• for terms $t_1, \ldots, t_n \in T(\Sigma, X)$ and a function symbol $f \in \Sigma_n$ of arity $n$, $f(t_1, \ldots, t_n) \in T(\Sigma, X)$ -- bigger terms arise from applying function symbols to smaller terms; $\Sigma = \dot{\cup}_n \Sigma_n$ is called a signature.

In OCaml, we can define terms as: type term = V of string | T of string * term list, where for example V("x") is a variable $x$ and T("f", [V("x"); V("y")]) is the term $f(x, y)$.

By substitutions $\sigma, \rho, \ldots$ we mean finite sets of variable-term pairs which we can write as ${x_1 \mapsto t_1, \ldots, x_k \mapsto t_k}$ or $[x_1 := t_1; \ldots; x_k := t_k]$, but also functions from terms to terms $\sigma : T(\Sigma, X) \rightarrow T(\Sigma, X)$ related to the pairs as follows: if $\sigma = {x_1 \mapsto t_1, \ldots, x_k \mapsto t_k}$, then

• $\sigma(x_i) = t_i$ for $x_i \in {x_1, \ldots, x_k}$,
• $\sigma(x) = x$ for $x \in X \setminus {x_1, \ldots, x_k}$,
• $\sigma(f(t_1, \ldots, t_n)) = f(\sigma(t_1), \ldots, \sigma(t_n))$.

In OCaml, we can define substitutions $\sigma$ as: type subst = (string * term) list, together with a function apply : subst -> term -> term which computes $\sigma(\cdot)$.

We say that a substitution $\sigma$ is more general than all substitutions $\rho \circ \sigma$, where $(\rho \circ \sigma)(x) = \rho(\sigma(x))$. In type inference, we are interested in most general solutions.

A unification problem is a finite set of equations $S = {s_1 =^? t_1, \ldots, s_n =^? t_n}$. A solution, or unifier of $S$, is a substitution $\sigma$ such that $\sigma(s_i) = \sigma(t_i)$ for $i = 1, \ldots, n$. A most general unifier, or MGU, is a most general such substitution.

1. Implement an algorithm that, given a set of equations represented as a list of pairs of terms, computes an idempotent most general unifier of the equations.

2. (Ex. 4.22 in Franz Baader and Tobias Nipkow "Term Rewriting and All That", p. 82.) Modify the implementation of unification to achieve linear space complexity by working with what could be called iterated substitutions.

Exercise 3: Algebraic Specs and Junk

1. What does it mean that an implementation has junk (as an algebraic structure for a given signature)? Is it bad?
2. Define a monomorphic algebraic specification (other than, but similar to, $\text{nat}_p$ or $\text{string}_p$, some useful data type).
3. Discuss an example of a (monomorphic) algebraic specification where it would be useful to drop some axioms (giving up monomorphicity) to allow more efficient implementations.

Exercise 4: Map Specification Audit

1. Does the example ListMap meet the requirements of the algebraic specification for maps? Hint: here is the definition of List.remove_assoc; compare a x equals 0 if and only if a = x.

   let rec remove_assoc x = function
     | [] -> []
     | (a, b as pair) :: l ->
         if compare a x = 0 then l else pair :: remove_assoc x l
   

2. Trick question: what is the computational complexity of ListMap or TrivialMap?

3. (*) The implementation MyListMap is inefficient: it performs a lot of copying and is not tail-recursive. Optimize it (without changing the type definition).

4. Add (and specify) $\text{isEmpty} : (\alpha, \beta) \ \text{map} \rightarrow \text{bool}$ to the example algebraic specification of maps without increasing the burden on its implementations. Hint: equational reasoning might be not enough; consider an equivalence relation $\approx$ meaning "have the same keys".

Exercise 5: Queue ADT Design

Design an algebraic specification and write a signature for first-in-first-out queues. Provide two implementations: one straightforward using a list, and another one using two lists: one for freshly added elements providing efficient queueing of new elements, and "reversed" one for efficient popping of old elements.

Exercise 6: Set ADT Design

Design an algebraic specification and write a signature for sets. Provide two implementations: one straightforward using a list, and another one using a map into the unit type.

Exercise 7: Efficient Set Operations

1. (Ex. 2.2 in Chris Okasaki "Purely Functional Data Structures") In the worst case, member performs approximately $2d$ comparisons, where $d$ is the depth of the tree. Rewrite member to take no more than $d + 1$ comparisons by keeping track of a candidate element that might be equal to the query element (say, the last element for which $<$ returned false) and checking for equality only when you hit the bottom of the tree.

2. (Ex. 3.10 in Chris Okasaki "Purely Functional Data Structures") The balance function currently performs several unnecessary tests: when e.g. ins recurses on the left child, there are no violations on the right child.

   • Split balance into lbalance and rbalance that test for violations of left resp. right child only. Replace calls to balance appropriately.
   • One of the remaining tests on grandchildren is also unnecessary. Rewrite ins so that it never tests the color of nodes not on the search path.

Exercise 8: AVL Map Implementation

(*) Implement maps (i.e. write a module for the map signature) based on AVL trees. See http://en.wikipedia.org/wiki/AVL_tree.

Chapter 6: Folding and Backtracking

{.chapter-image}

In this chapter, you will:

• Identify common recursion patterns and refactor them into map/fold abstractions
• Make folds tail-recursive using accumulators (and understand the trade-offs)
• Generalize map/fold beyond lists to trees and expression grammars
• Use backtracking (via lists) to solve search problems and puzzles

This chapter explores two fundamental programming paradigms in functional programming: folding (also known as reduction) and backtracking. We begin with the classic map and fold higher-order functions, examine how they generalize to trees and other data structures, then move on to solving puzzles using backtracking with lists.

The material in this chapter draws from Martin Odersky's "Functional Programming Fundamentals," Ralf Laemmel's "Going Bananas," Graham Hutton's "Programming in Haskell" (Chapter 11 on the Countdown Problem), and Tomasz Wierzbicki's Honey Islands Puzzle Solver.

6.1 Basic Generic List Operations

Functional programming emphasizes identifying common patterns and abstracting them into reusable higher-order functions. Rather than writing similar code repeatedly, we extract the common structure into a single generic function. Let us see how this principle works in practice through two motivating examples.

The map Function

How do we print a comma-separated list of integers? The String module provides a function that joins strings with a separator:

val concat : string -> string list -> string

But String.concat works on strings, not integers. So first, we need to convert numbers into strings:

let rec strings_of_ints = function
  | [] -> []
  | hd::tl -> string_of_int hd :: strings_of_ints tl

let comma_sep_ints = String.concat ", " -| strings_of_ints

Here is another common task: how do we sort strings from shortest to longest? We can pair each string with its length and then sort by the first component. First, let us compute the lengths:

let rec strings_lengths = function
  | [] -> []
  | hd::tl -> (String.length hd, hd) :: strings_lengths tl

let by_size = List.sort compare -| strings_lengths

Now, look carefully at strings_of_ints and strings_lengths. Do you notice the common structure? Both functions traverse a list and transform each element independently -- one applies string_of_int, the other applies a function that pairs a string with its length. The recursive structure is identical; only the transformation differs.

This is our cue to extract the common pattern into a generic higher-order function. We call it map:

let rec list_map f = function
  | [] -> []
  | hd::tl -> f hd :: list_map f tl

Now we can rewrite our functions more concisely:

let comma_sep_ints =
  String.concat ", " -| list_map string_of_int

let by_size =
  List.sort compare -| list_map (fun s -> String.length s, s)

The fold Function

Now let us consider a different kind of pattern. How do we sum all the elements of a list?

let rec balance = function
  | [] -> 0
  | hd::tl -> hd + balance tl

And how do we multiply all the elements together (perhaps to compute a cumulative ratio)?

let rec total_ratio = function
  | [] -> 1.
  | hd::tl -> hd *. total_ratio tl

Again, the recursive structure is the same. In both cases, we combine each element with the result of processing the rest of the list. The differences are: (1) what we return for the empty list (the "base case" or "identity element"), and (2) how we combine the head with the recursive result. This pattern is called folding:

let rec list_fold f base = function
  | [] -> base
  | hd::tl -> f hd (list_fold f base tl)

Important: Note that list_fold f base l equals List.fold_right f l base. The OCaml standard library uses a different argument order, so be careful when using List.fold_right.

The key insight is understanding the fundamental difference between map and fold:

• map alters the contents of a data structure without changing its shape. The output list has the same length as the input; we merely transform each element.
• fold collapses a data structure down to a single value, using the structure itself as scaffolding for the computation.

Visually, consider what happens to the list [a; b; c; d]:

• map f transforms: [a; b; c; d] becomes [f a; f b; f c; f d] -- same structure, different contents
• fold f accu collapses: [a; b; c; d] becomes f a (f b (f c (f d accu))) -- structure disappears, single value remains

6.2 Making Fold Tail-Recursive

Our list_fold function above is not tail-recursive: it builds up a chain of deferred f applications on the call stack. For very long lists, this can cause stack overflow. Can we make folding tail-recursive?

Let us investigate some tail-recursive list functions to find a pattern. Consider reversing a list:

let rec list_rev acc = function
  | [] -> acc
  | hd::tl -> list_rev (hd::acc) tl

The key technique here is the accumulator parameter acc. Instead of building up work to do after the recursive call returns, we do the work before the recursive call and pass the intermediate result along.

Here is another example -- computing an average by tracking both the running sum and the count:

let rec average (sum, tot) = function
  | [] when tot = 0. -> 0.
  | [] -> sum /. tot
  | hd::tl -> average (hd +. sum, 1. +. tot) tl

Notice how these functions process elements from left to right, threading an accumulator through the computation. This is the pattern of fold_left:

let rec fold_left f accu = function
  | [] -> accu
  | a::l -> fold_left f (f accu a) l

With fold_left, expressing our earlier functions becomes straightforward -- we hide the accumulator inside the initial value:

let list_rev l =
  fold_left (fun t h -> h::t) [] l

let average =
  fold_left (fun (sum, tot) e -> sum +. e, 1. +. tot) (0., 0.)

Note that the average example is slightly trickier than list_rev because we need to track two values (sum and count) rather than one.

Why the names fold_right and fold_left? The names reflect the associativity of the combining operation:

• fold_right f makes f right associative, like the list constructor ::: List.fold_right f [a1; ...; an] b is f a1 (f a2 (... (f an b) ...))

• fold_left f makes f left associative, like function application: List.fold_left f a [b1; ...; bn] is f (... (f (f a b1) b2) ...) bn

This "backward" structure of fold_left can be visualized by comparing the shape of the input list with the shape of the computation tree. The input list has a right-leaning spine (because :: associates to the right), while fold_left produces a computation tree with a left-leaning spine:

::: {.figure}

    Input list              Result computation

        ::                         f
       /  \                       / \
      a    ::                    f   d
          /  \                  / \
         b    ::               f   c
             /  \             / \
            c    ::          f   b
                /  \        / \
               d    []  accu   a

Figure: List spine vs. fold_left computation tree :::

This reversal of structure is why fold_left naturally reverses lists when the combining operation is cons.

Useful Derived Functions

Many common list operations can be expressed elegantly using folds. List filtering selects elements satisfying a predicate -- naturally expressed using fold_right to preserve order:

let list_filter p l =
  List.fold_right (fun h t -> if p h then h::t else t) l []

When we need a tail-recursive map and can tolerate reversed output, fold_left gives us rev_map:

let list_rev_map f l =
  List.fold_left (fun t h -> f h :: t) [] l

6.3 Map and Fold for Trees and Other Structures

The map and fold patterns are not limited to lists. They apply to any recursive data structure. The key insight is that map preserves structure while transforming contents, and fold collapses structure into a single value.

Binary Trees

Mapping binary trees is straightforward:

type 'a btree = Empty | Node of 'a * 'a btree * 'a btree

let rec bt_map f = function
  | Empty -> Empty
  | Node (e, l, r) -> Node (f e, bt_map f l, bt_map f r)

let test = Node
  (3, Node (5, Empty, Empty), Node (7, Empty, Empty))
let _ = bt_map ((+) 1) test

A note on terminology: The map and fold functions we define here preserve and respect the structure of data. They are different from the map and fold operations you might find in abstract data type container libraries, which often behave more like List.rev_map and List.fold_left over container elements in arbitrary order. Here we are generalizing List.map and List.fold_right to other structures.

For binary trees, the most general form of fold processes each element together with the partial results already computed for its subtrees:

let rec bt_fold f base = function
  | Empty -> base
  | Node (e, l, r) ->
    f e (bt_fold f base l) (bt_fold f base r)

Here are two examples showing how bt_fold can compute different properties of a tree:

let sum_els = bt_fold (fun i l r -> i + l + r) 0
let depth t = bt_fold (fun _ l r -> 1 + max l r) 1 t

The first computes the sum of all elements (the combining function adds the current element to the sums of both subtrees). The second computes the depth -- we ignore the element value and take the maximum depth of the subtrees, adding 1 for the current level.

More Complex Structures: Expressions

Real-world data types often have more than two cases. To demonstrate map and fold for more complex structures, let us recall the expression type from Chapter 3:

type expression =
    Const of float
  | Var of string
  | Sum of expression * expression    (* e1 + e2 *)
  | Diff of expression * expression   (* e1 - e2 *)
  | Prod of expression * expression   (* e1 * e2 *)
  | Quot of expression * expression   (* e1 / e2 *)

The multitude of cases makes this datatype harder to work with than binary trees. Fortunately, OCaml's or-patterns help us handle multiple similar cases together:

let rec vars = function
  | Const _ -> []
  | Var x -> [x]
  | Sum (a,b) | Diff (a,b) | Prod (a,b) | Quot (a,b) ->
    vars a @ vars b

For a generic map and fold over expressions, we need to specify behavior for each case. Since there are many cases, we pack all the behaviors into records. This way, we can define default behaviors and then override just the cases we care about:

type expression_map = {
  map_const : float -> expression;
  map_var : string -> expression;
  map_sum : expression -> expression -> expression;
  map_diff : expression -> expression -> expression;
  map_prod : expression -> expression -> expression;
  map_quot : expression -> expression -> expression;
}

(*
   Note: In expression_fold, we use 'a instead of expression because
   fold produces values of arbitrary type, not necessarily expressions.
*)
type 'a expression_fold = {
  fold_const : float -> 'a;
  fold_var : string -> 'a;
  fold_sum : 'a -> 'a -> 'a;
  fold_diff : 'a -> 'a -> 'a;
  fold_prod : 'a -> 'a -> 'a;
  fold_quot : 'a -> 'a -> 'a;
}

Now we define standard "default" behaviors. The identity_map reconstructs the same expression (useful as a starting point when we only want to change one case), and make_fold creates a fold where all binary operators behave the same:

let identity_map = {
  map_const = (fun c -> Const c);
  map_var = (fun x -> Var x);
  map_sum = (fun a b -> Sum (a, b));
  map_diff = (fun a b -> Diff (a, b));
  map_prod = (fun a b -> Prod (a, b));
  map_quot = (fun a b -> Quot (a, b));
}

let make_fold op base = {
  fold_const = (fun _ -> base);
  fold_var = (fun _ -> base);
  fold_sum