Contents
Chapter 43

Confidence

Introductions to functional programming usually call it “programming with functions,” and functions really are a central part of the practice. But after (slowly) studying it for over ten years, I have started to wonder whether it’s more about “functionality.” One definition of science is “what works.” Science has theories that fit the data, are predictive, and are falsifiable. If “computer science” is to live up to its name, some of its ideas and practices should fit that definition, and perhaps some should even be mathematically provable. This seems to me to be the broader challenge that functional programming takes on, and what this chapter explores.

The preceding chapters built the machinery. Foundations established pure functions and immutable values, Toolkits supplied the standard library’s support, and Error Handling made failure an ordinary value. This chapter asks what that machinery lets you claim about your code, and how far those claims can go.

Referential Transparency

An expression is referentially transparent when you can replace it with its value without changing the program’s behavior. Pure functions have this property, and that is the reason purity matters:

# referential_transparency.py
def add(a: int, b: int) -> int:
    return a + b

# The call add(2, 3) always equals 5, so the call and the
# value 5 are interchangeable everywhere in the program.
x = add(2, 3) + add(2, 3)
y = 5 + 5
print(x, y, x == y)
#: 10 10 True

Because add(2, 3) and 5 are interchangeable, an implementation may cache the call, run the two calls in either order, or skip the second. The language has no way to mark add() as pure, so CPython applies none of the three and leaves them to you. You can also reason about the code by substitution, the same move you make in algebra. Referential transparency lets you check parts of a program, and sometimes prove them correct.

Substitution stops working the moment a function reads or writes outside itself. withdraw() from Foundations does both, reading and writing the module-level balance:

# not_transparent.py
balance = 100

def withdraw(amount: int) -> int:
    global balance
    balance -= amount
    return balance

print(withdraw(30) + withdraw(30))
#: 110
balance = 100
print(70 + withdraw(30))
#: 140

The first withdraw(30) evaluates to 70, so substituting 70 for it ought to change nothing. It changes 110 into 140. withdraw() is not referentially transparent, and any expression containing it inherits the problem, so substitution reasoning stops at the first impure call.

global is not the only way to break substitution. A function that mutates an argument breaks it too, with no global in sight:

# mutates_argument.py
def add_item(cart: list[str], item: str) -> list[str]:
    cart.append(item)
    return cart

cart: list[str] = ["milk"]
add_item(cart, "eggs")
add_item(cart, "eggs")
print(cart)
#: ['milk', 'eggs', 'eggs']

Each call to add_item() returns the same list the caller passed in, so replacing the call with that list looks safe. It is not. The call also appends to cart, a change substitution cannot see, so calling it twice leaves cart different from calling it once.

Referential transparency also makes lru_cache safe. A memoizer can hand back a stored result because the call is interchangeable with its value. Every optimization that skips or reuses work, from a cache to a database query planner, benefits from referential transparency. The more your program is referentially transparent, the more of it a machine, or a proof, can verify. Caching an impure function breaks silently instead of raising an exception. withdraw() is not referentially transparent, so decorating it with lru_cache corrupts its own bookkeeping:

# cached_withdraw.py
from functools import lru_cache

balance = 100

@lru_cache
def withdraw(amount: int) -> int:
    global balance
    balance -= amount
    return balance

print(withdraw(30), withdraw(30))
#: 70 70
print(f"balance: {balance}")
#: balance: 70

Two withdrawals of 30 should leave balance at 40. The second call is a cache hit, so withdraw() never runs a second time and never subtracts the second 30, with no error to report the loss. lru_cache trusts every call it wraps to be referentially transparent, and nothing in the language checks that trust.

Automatic Parallelism

A pure function is automatically parallelizable. Each call depends only on its arguments, so no call can affect another. The calls can run in any order, on any schedule, on any number of cores, and the answers do not change.

Impure code has no such freedom. Two parallel withdraw() calls could both read balance before either writes it back, and one withdrawal vanishes. A lock makes that safe, and the lock serializes the work you wanted to overlap. Purity removes the problem instead of managing it: with nothing shared, a lock has nothing to guard.

count_primes() is pure, and each call does enough work to spread across cores:

# parallel_pure.py
import time
from concurrent.futures import ProcessPoolExecutor
from benchmark import report

def count_primes(limit: int) -> int:
    count = 0
    for n in range(2, limit):
        if all(n % d for d in range(2, int(n**0.5) + 1)):
            count += 1
    return count

if __name__ == "__main__":
    limits = [200_000, 400_000, 600_000, 800_000]
    start = time.perf_counter()
    serial = list(map(count_primes, limits))
    serial_time = time.perf_counter() - start
    start = time.perf_counter()
    with ProcessPoolExecutor() as pool:
        parallel = list(pool.map(count_primes, limits))
    parallel_time = time.perf_counter() - start
    assert parallel == serial
    report(serial=serial_time, parallel=parallel_time)
    print(parallel)
    # Sample run: [17984, 33860, 49098, 63951]
    faster = serial_time > 1.3 * parallel_time
    print(f"serial at least 1.3x parallel time: {faster}")
    # Sample run: serial at least 1.3x parallel time: True

list(map(...)) runs the four calls one at a time, on one core. pool.map() sends the same calls to worker processes, which the operating system places on separate cores. The assert passes on every run, because a pure call returns the same answer no matter which process ran it, or when. The limits above are large enough for the difference to show: on the machine that built this book, the serial run took a few seconds and the parallel run about half that, comfortably clearing the 1.3x margin the last line checks. Smaller limits finish before spawning the worker processes pays for itself, so a reader who shrinks the limits back down will watch parallel lose. Purity makes parallel safe. It says nothing about whether parallel is worth it at a given size. No locks, no queues, no shared state: a pure function is ready to run in parallel, unchanged.

Purity makes the calls safe to run together. It does not make them easy to move. Each argument and each result pickles to cross the process boundary, and the function travels by name, so count_primes() must live at the top level of a module a worker can import. A lambda or a closure fails with a PicklingError, and that rules out two shapes these chapters favor. A functools.partial survives, because it pickles as its wrapped function plus its bound arguments. The if __name__ == "__main__" guard exists for the same reason: each worker imports this module to find count_primes(), and without the guard every worker would build a pool of its own. Concurrency covers the pickling boundary and the guard, along with the reasons Python parallelism uses processes rather than threads.

A Confidence Spectrum

The chapter opened by asking whether programming can make the kind of provable claims a science makes. Functional programming’s answer is not one guarantee but a spectrum. Purity, immutability, and referential transparency, the properties these chapters built, provide confidence at every level.

Style contributes before the first rung. Declarative code states the result you want, while imperative code spells out each step to produce it. A comprehension names the result, “the squares of the even numbers” (see Comprehensions), and match names the shapes you expect (see Pattern Matching), the way Error Handling took a Result apart with one branch per kind of failure. A description of the result is easier to check than a sequence of steps, because less of it can be wrong. It also leaves the runtime free to choose the steps, which is why a SQL query, a NumPy expression, or a dataframe operation can run on an optimized or parallel engine you never see.

You decide how far up the spectrum to go.

  1. The cheapest rung is local reasoning. Pure functions and immutable values let you understand one piece at a time, with no hidden state to carry in your head. Most code needs no more.
  2. Next are tests over chosen examples, the subject of Testing. Each one pins a single input to a single answer, so what you learn is no wider than the examples you invent.
  3. Next is type checking. A type signature is a small theorem, and the function body is its proof. This is the Curry-Howard correspondence. Python’s version of it is partial. An Any, a cast(), or data arriving from outside the program leaves a gap no type checker can close, so the theorem holds only as far as the annotations do. Running ty over the examples in this book still rules out a useful class of mistakes, and that is most of what this rung offers.
  4. Above that is property-based testing. You state a law the code must obey, then check it against many generated inputs. It searches for a counterexample instead of proving the law, and that search is the falsifiability the opening required of a science. The climb from rung 3 is in expressiveness, not certainty. A type states only what shape a value has. A property can state a fact about its behavior, at the cost of checking a sample of inputs instead of every one.
  5. At the top is formal proof. In a dependently-typed language such as Lean, Idris, or Rocq (formerly Coq), you prove a program correct for every possible input, and a machine checks the proof. This is real, but rare outside specialized work.

Property-Based Testing

You can write a property check by hand, looping over random inputs and asserting the law. A tool like Hypothesis does the same thing with sharper inputs, and shrinks any failure to a minimal counterexample:

# property_check.py
import random

def encode(text: str) -> str:
    # Reversible, and not its own inverse:
    return text.encode().hex()

def decode(text: str) -> str:
    return bytes.fromhex(text).decode()

random.seed(42)  # A failing search must be reproducible
alphabet = "abcde"
for _ in range(1000):
    size = random.randint(0, 8)
    sample = "".join(random.choice(alphabet)
                     for _ in range(size))
    assert decode(encode(sample)) == sample
print("1000 random cases passed")
#: 1000 random cases passed

The law is “decoding an encoding returns the original,” and it holds for every input the loop tries. A property test states what must always be true. The machine searches for a counterexample. A bare assert like this one reports only AssertionError if the law fails. Python prints the assert’s source code, not the value that broke it, so finding the failing input means adding a print() and rerunning by hand.

Hypothesis turns the hand-written loop into a declaration. You describe the inputs with a Strategy and state the law once, as a normal test_ function. The framework supplies the cases, drawing on every character UTF-8 can encode rather than property_check.py’s five-letter alphabet, so it reaches inputs the loop cannot produce, such as unusual Unicode:

# test_property.py
from hypothesis import given, strategies

def encode(text: str) -> str:
    return text.encode().hex()

def decode(text: str) -> str:
    return bytes.fromhex(text).decode()

@given(strategies.text())
def test_roundtrip(sample: str) -> None:
    assert decode(encode(sample)) == sample

The listing repeats the two functions rather than importing them, because importing property_check.py would run its thousand-iteration loop inside the test run.

@given(strategies.text()) feeds test_roundtrip() a stream of generated strings. By default Hypothesis generates a hundred of them, a tenth of the hand-written loop’s thousand, and they still cover more ground, because Hypothesis aims at boundaries and oddities instead of sampling evenly. When a law fails, Hypothesis reports the failing input, the first improvement over the bare assert above. It also shrinks that input to the smallest example that still fails, a second improvement, so the bug surfaces as the clearest case rather than a random one. The framework automates falsification.

The two listings above both pass, so nothing has shrunk yet. The next codec has a bug, and it is the Unicode gap promised earlier:

# shrinking.py
from hypothesis import given, settings, strategies

def encode(text: str) -> str:
    return text.encode().hex()

def decode(text: str) -> str:
    return bytes.fromhex(text).decode("latin-1")

@settings(derandomize=True, database=None)
@given(strategies.text())
def roundtrip(sample: str) -> None:
    assert decode(encode(sample)) == sample

try:
    roundtrip()
except AssertionError as e:
    print(e.__notes__[0])
#: Failing test case: roundtrip(
#:     sample='\x80',
#: )

encode() still turns text into UTF-8 bytes, but decode() now reads those bytes back as Latin-1 instead of UTF-8. The two agree on the 128 ASCII code points, so property_check.py’s five-letter alphabet, built only from those, can run all thousand cases and never reach the mismatch. Hypothesis draws from the full range a Python string holds, and shrinks its failure down to the smallest code point outside that agreement, '\x80', the first character UTF-8 needs more than one byte to encode. Decoding those two bytes as Latin-1 returns two characters where one went in, so the round trip breaks. This is the unusual Unicode the hand loop’s alphabet could never draw, found because Hypothesis draws from a wider alphabet, not because it guessed the bug. derandomize=True fixes the search so this book gets the same answer every run, the job random.seed(42) does in the hand-written loop. database=None keeps it from replaying a case an earlier run saved. A real test needs neither. This function exists to fail, and a failing test_ function would fail the build, so its name drops the test_ prefix and the listing calls it directly inside a try.

The roundtrip law is one member of a small family of reusable property shapes, and knowing the family is most of the skill. An invariant states a fact about every output: sorting produces an ordered list. Idempotence states that repeating changes nothing: sorting a sorted list leaves it alone. An oracle states that two implementations agree: the simple version you can check by reading matches the fast one. parallel_pure.py’s assert parallel == serial makes that claim about map() and pool.map(). The trap to avoid is a property that restates the implementation. Asserting encode(text) == text.encode().hex() tests nothing, because the test and the code share any bug. A good law, like the roundtrip, constrains the function’s behavior without repeating its body. All of these lean on purity. Hypothesis can rerun and shrink freely because each call is independent of every other.

Affordable Proof

Two caveats keep the chapter’s argument from overreaching. First, proof works on imperative code too: Hoare logic and tools like Dafny verify it. What purity changes is the cost. With no mutable state to track, each step of the reasoning is shorter. Functional programming does not make correctness provable so much as it makes the proof affordable. Second, most functional code stops well below the top rung. Haskell programmers rarely prove a program correct. They lean on types and on reasoning by substitution, and save full proof for the few places that earn it.

The thread running through these chapters is not that functions are special. It is that purity, immutability, and referential transparency shrink the distance between “I believe this is correct” and “I can show why.” Proof is the far end of that distance. The everyday win is everything below it: code you can read, check, and test as statements about what is true. That, more than the presence of functions, is the “functionality” the introduction set out to find.

Part V takes the same discipline one step further and asks the type checker to enforce it: Effect Management puts a function’s effects in its signature, and the chapters after it build a checked system on that idea.

Exercises

  1. Change count_primes() to return (count, os.getpid()) and print the distinct process IDs alongside the counts. Narrow assert parallel == serial to compare only the counts, since the serial run now carries the parent’s ID and the parallel one carries the workers’. Compare the number of distinct IDs to os.process_cpu_count(), and run it three times before deciding what it means.
  2. Replace ProcessPoolExecutor with ThreadPoolExecutor in the previous exercise and explain the IDs you see instead.
  3. Write Hypothesis properties for sorted() using two shapes from the family above: an invariant (every adjacent pair of the output is in order) and idempotence (sorting a sorted list changes nothing). Then add the oracle property that sorted(xs) agrees with a hand-written insertion sort on short lists.
  4. State a law that is false and watch Hypothesis falsify it: @given(strategies.text()) with assert s.upper().lower() == s.lower(). Report the counterexample Hypothesis shrinks to, run it a few times to see which characters it settles on, and explain what they reveal about Unicode case mapping.
  5. Write a property test for group_rounds() from Toolkits: for any roster and any group size, every student appears in exactly one group per round. Use a strategy that generates rosters of distinct names. Then break group_rounds() on purpose, run the test twice, and confirm the same counterexample arrives both times: Hypothesis records a failing case under .hypothesis/ and replays it first on the next run.
  6. Write two functions that are not referentially transparent without using global: one that reads datetime.now(), and one that reads an environment variable. For each, name the substitution that would change the program’s behavior, then rewrite it so the value arrives as an argument.
  7. Take the describe() function from Error Handling and rewrite its match as isinstance() tests. Count the lines, then run ty on both and compare what each one knows about the value inside the Ok.