Purity

PFCL language reference · composure.systems

1.Scope

This document specifies the purity guarantee that applies to every function in a PFCL catalog. It defines what purity means in PFCL, states the guarantee formally, and enumerates the exclusions.

1. A function is a PFCL expression of type T₁ × ... × Tₙ → T, closed under the free variables of its signature.
2. An evaluation is the reduction of a function application under the language's operational semantics to a normal form.
3. A function is pure if for every well-typed tuple of inputs, its evaluation depends only on those inputs, produces only the resulting value, and observes no ambient state.

2.Statement

Let f be a function in a PFCL catalog and let x be a well-typed input for f. Then:

1. Evaluation of f(x) proceeds by reduction of f's body with x substituted for f's parameters, using only the language's operational semantics.
2. The evaluation depends on x and on the definitions of the functions f calls. It does not depend on time, on the state of any external resource, or on any observation of the host environment.
3. The evaluation produces a value in f's declared output type, and produces nothing else. It performs no side effect.
4. Two evaluations of f(x) and f(x') with x = x' produce equal output values.

3.Consequences

Three properties follow directly.

1. Referential transparency. A call to a function with a given input may be replaced by that function's output value without changing the observable behaviour of any program that contains the call.
2. Compositionality. A function composed of pure functions is pure. The property closes under composition, over the entire catalog.
3. Independence from evaluation strategy. The value produced by an evaluation is a property of the function and its input, not of the order or timing of reduction steps. Any strategy that reaches a normal form reaches the same normal form.

4.Effect-describing functions

Some functions need to describe an effect — writing to standard output, reading a file, making a network call, changing a persisted value. In PFCL, such a function does not perform the effect. It returns a value — a command record, or a list of them — that describes the effect. A host program reads the value and performs the action.

The function is pure. Its output is determined entirely by its input. The effect happens when the host reads the returned value; the function's own evaluation performs nothing. The mechanism by which this is arranged, and the properties it yields, are described at /effects-as-data.

The purity guarantee stated in section 2 covers effect-describing functions in the same way it covers any other function. Their return type is different — it contains command records rather than only data — but the property of their evaluation is unchanged.

5.Exclusions

The guarantee does not cover the following.

1. Primitives. A composed function calling a primitive is pure if the primitive is pure. The purity of primitives is established by external audit of their implementation and is declared in metadata. A composed function calling a primitive that violates the primitive's declared purity contract is outside the guarantee.
2. Hosts. The purity guarantee applies to the function's evaluation, not to what a host does with the function's returned value. A host reading a command record and performing an effect is doing what the function described; the effect is a property of the host's execution, not of the function.
3. Non-termination. The guarantee that a function's evaluation produces a value assumes the evaluation terminates. Termination is a separate property, specified at /totality.

6.Relation to totality

Purity and totality together yield the property that a function's return value is fully determined by its inputs and is produced in bounded time. A function that is pure but not total may fail to produce a value on some inputs. A function that is total but not pure may produce different values on repeat calls with the same input. Neither alone is sufficient for the reasoning properties one wants from a function; the combination is.

Totality is specified at /totality. The two properties are stated independently and enforced independently. A PFCL catalog holds both guarantees for every function it admits.