Referential Transparency and the Substitution Test

Two calls to the same function with the same arguments may produce different results, or the same result while leaving the machine in different states. When either happens, an expression can no longer be swapped for its value without changing what the program does, and every optimization that performs such a swap becomes unsound. Referential transparency is the name for the property that makes the swap safe, and the useful way to define it is as an equation between a program fragment and its meaning.

The substitution property, stated precisely

Write e ⇓ v for the judgement that expression e evaluates to value v. An expression is referentially transparent when, for every context C (a program with one hole), C[e] and C[v] have the same observable behaviour. Observable behaviour is deliberately coarse: the value produced, whether evaluation terminates, and the sequence of interactions with the outside world. Two programs that differ only in how long they take or how much memory they consume are considered equal under this relation.

Read operationally, the definition says a pure expression denotes one value forever. Read denotationally, it says the expression is a name for an element of a semantic domain, and composition is function application on those elements. The two readings agree often enough that the phrase “purity” is used for both, but they come apart on divergence and on exceptions, which are values in some domains and failures of the judgement in others.

The equation has a second half that is easy to miss. It is not enough that e always produces the same v; the context must also be unable to distinguish v from a copy of v. Languages that expose object identity violate this half without violating the first.

Where the property breaks

Four families of feature break substitutivity, and each one breaks it for a different reason.

Mutable store. A read of a reference cell depends on the history of writes to that cell, not on the cell expression itself. If r holds 0, then !r denotes 0 now and 1 after an assignment, so no single value can replace the expression. The same argument applies to global variables, to mutable record fields, and to arrays.

Identity. Physical equality tests whether two references point at the same object. Two calls to a function that allocates a fresh empty list return structurally equal but physically distinct values, so replacing the second call with the first changes the result of ==. Hash codes derived from addresses have the same defect. This is why languages that offer both structural and physical equality require the programmer to choose, and why the physical variant cannot be given a substitutive semantics.

Non-determinism. A function of the clock, the random generator, the process environment, or the amount of free memory maps the same argument to different results at different times. The equation e ⇓ v fails outright.

Divergence and exceptions. Replacing a non-terminating expression by a value turns a program that never halts into one that does, which is observable. Exceptions behave the same way when they escape: a context that catches the exception sees a different result than a context that receives a value. Both show that the substitution property is a statement about total expressions, and that partiality has to be modelled rather than ignored.

A language can also break substitutivity in a way that is invisible in the type. The C standard leaves the order of evaluation of the operands of most operators unspecified, so in f() + g() the two calls may run in either order, and a program whose result depends on that order has no fixed meaning at all. Java specifies left-to-right evaluation of operands and still allows a thread to observe writes from another thread without a happens-before edge between them. C has mutable state and unspecified order; Java has mutable state and a defined intra-thread order but a memory model that licenses reordering across threads. In both cases an expression is not always a name for a value, and the reason is the one the four families above already gave.

Bottoms, exceptions, and what types do not promise

In a typed language every expression has a type, and it is tempting to conclude that an expression of type Int denotes an integer. It does not.

undefined :: a                      -- inhabits every type

let x = undefined in 1              -- 1: the binding is never demanded
seq undefined 1                     -- undefined: the demand is what differs

undefined inhabits every type, so the type checker accepts both expressions, and they disagree about the value because one demands the ⊥ and the other does not. Totality is not part of the type.

The consequence is that “pure” cannot mean “total”. A pure function may fail to terminate, and the standard treatment is to add a least element, written ⊥, to every type, so that the denotation of undefined is ⊥ and the substitution property is stated over a domain rather than a set. Strict functions map ⊥ to ⊥; lazy ones may not. const 1 undefined is 1, because const never demands its second argument, and seq undefined 1 is undefined, because seq demands its first. That is the whole content of the distinction between the two, and it is why seq can be seen in a program’s meaning even though it performs no effect.

This is also where a language can cheat. A function declared with a pure type but implemented by reading a global counter satisfies the type and violates the property. Haskell’s escape hatch is unsafePerformIO, whose type is IO a -> a; the name is honest about the fact that the resulting expression cannot be reasoned about as a value. Any optimization that duplicates, reorders, or eliminates the call may change behaviour, and the language gives no guarantee about which of those will happen.

What the property buys

The value of the substitution property is that it licenses transformations. A compiler can replace let x = e in (x, x) with a single evaluation of e, because both occurrences denote the same value; that transformation is common-subexpression elimination, and it is unsound for any expression whose evaluation has an effect. The same argument justifies inlining, dead-code elimination of unused bindings, hoisting loop-invariant computations, and reordering independent work across threads.

The second payoff is reasoning. If every expression is a value, then a function definition is an equation, and proving a property of a program is proving a property of a function on its domain. Hughes makes the case that this is what makes functional languages modular: a function can be replaced by any extensionally equal function without touching its callers, and composition of programs is composition of mathematical functions.

The third payoff is parametricity. Wadler’s free theorems follow from the fact that a polymorphic function must behave uniformly for all instantiations. The type forall a. a -> a admits only the identity function and ⊥; the type forall a. [a] -> [a] admits only functions that rearrange, drop, or duplicate elements, because the element type is unknown and the function cannot inspect it. These results require purity: a function that printed its argument would be distinguishable at different types by its output, and the theorem would fail.

A fourth payoff is memoization. If a function is pure, its result for an argument can be cached and reused, which is only sound because the result cannot change. The same property allows a thunk to stand in for an unevaluated expression and be forced later, which is the mechanism described in call-by-need evaluation.

The costs, stated on the same axis

Purity is not free, and the cost is easiest to see in data structures. Updating one field of a balanced tree while preserving the old version requires copying the path from the root to the changed node, which costs O(log n) allocations where a mutable update costs one store. An array cannot be updated in place at all without either a copy of the whole array or a type system that tracks uniqueness. Languages that want both purity and in-place update therefore add a second mechanism: the ST monad in Haskell, uniqueness types in Clean, or linear types in a language that can prove a value has exactly one reference.

The trade is measurable. A strict, mutable array update writes 4 or 8 bytes. A purely functional update of a persistent structure allocates a path of O(log n) nodes, and each node in a typical implementation is a header plus several fields, so tens of bytes per node. The persistent version buys the ability to keep the old version alive, which is worth the allocation when versions are needed and wasted when they are not.

There is a second cost in optimization: purity makes transformations legal, but the compiler still has to find them, and the analyses that do so are not free. A language with effects must track where they occur; a language without effects does not need the analysis but also cannot express the programs that need it, which is why every serious functional language eventually grows an effect system or an escape hatch.

Purity as a property of expressions, not of languages

The final point is that no language is referentially transparent as a whole. The property is attached to expressions, and the useful question about a given expression is whether replacing it by its value preserves behaviour in the contexts where it appears.

Haskell’s IO is the clearest illustration. getLine has type IO String and is a value: a description of an action, constructed without reading anything. Two occurrences of the same description denote the same action, and substitution is sound. What is not substitutive is the execution of the action, which happens when the description is sequenced into main. Writing let x = getLine in x >> x duplicates the description and therefore reads twice, whereas x <- getLine; print x; print x reads once; both are pure programs, and the difference is in how many copies of the action were built. The let form duplicates because x names a value of type IO String and >> takes two of them; the do form does not, because >>= passes the single result of one action to a function, and a function’s body is instantiated per call rather than duplicated as text. This distinction between an action and its value is what makes the monadic encoding work, and it is the subject of monadic sequencing.

The same distinction explains why a pure language still needs a way to say “this argument is evaluated now”. seq and strict fields are not effects; they are annotations that change which value an expression denotes, by moving ⊥ into a position where it is observable. A language that offered neither could not express a strict fold, and one that offered them everywhere would lose the ability to define infinite structures.

Referential transparency is therefore a discipline rather than a guarantee. It holds when the programmer avoids the four breaking features, and it is preserved by composition: an expression built from transparent parts with transparent operators is itself transparent. The rest of this cluster is about what can be built on that foundation, from folds as universal consumers up to recursion schemes that generalize the same idea to any datatype.