How to verify function purity in an imperative language?

Question

A pure function in an imperative language means one with no observable side-effects, which when called multiple times with identical arguments will always return identical results, and which doesn't read any global or non-local mutable variables or other context from outside of the function and its arguments.

Pure functions give the compiler more leeway to optimise code by lazy evaluation, re-ordering computations, or memoisation. However, the compiler cannot apply these optimisations unless it can check that the functions are indeed pure. This is not trivial ─ an imperative function can be pure despite containing statements with side-effects (i.e. re-assigning local variables, mutating objects), if those side-effects are not externally visible.

For example, the following Python function is pure, despite mutating a list in two ways, because these mutations cannot be observed by the caller:

def ordered_running_totals(a: List[int]) -> List[int]:
    a = a.copy()
    a.sort()
    for i in range(1, len(a)):
        a[i] += a[i - 1]
    return a

Suppose a statically-typed imperative language has a pure modifier which can be applied to function declarations, to indicate that the function is pure. How can a static analyser verify that the modifier is used correctly? It's OK for the checker to be conservative (i.e. reject some valid functions, if they aren't written in a way the checker can recognise as pure), so long as it doesn't have any false positives.

Answer 1

What you're asking for is a type system for expressions that classify not only the value of the expression, but also how it's calculated — in particular, you want to have a class of expressions that is guaranteed not to have side effects when evaluated. The general framework for that is an effect system. There are two other popular ways to model purity: monads as in Haskell and linear types as in Clean. I think both can be modeled as effect systems, although not in a very convenient way. In this answer, I'll focus on effect systems, which are easiest to retrofit to an existing language.

If the following presentation seems a bit dry to you, I invite you to read a much longer answer I wrote on a similar topic.

The general idea of an effect system is that for each expression, we want the type checker to keep track of its possible side effects, in the same way that the type checker keeps track of the possible values through the expression's type (in the classical sense). To a first approximation, a value type designates a set of potential values, and an effect type designates a set of potential side effects. For example, read_int(f) + 1 is an expression that returns an integer and whose effect is to read from the file f. print_int(f, read_int(f) + 1) is an expression that returns nothing and whose effect is to read and write to the file f.

Classically, the type of a function indicates the type of its parameters and the type of its return value. With an effect system, the type of a function indicates the possible side effects when the function is evaluated. That is, if $f : A \to_{e} B$ ($f$ takes a parameter of type $A$, returns a value of type $B$, and has the effect $e$ when applied), then $f(x) :_{e} B$ (the expression $f(x)$ has the type $B$ and the effect $e$, assuming that $x$ has the type $A$). In this manner, the effect type system becomes embedded in the value type system.

Just like with data types, effect types can be more or less precise. For example, you can have a data type system that keeps track of every single potential value that an expression can have, but that very quickly becomes undecidable, so typical programming languages have a type integer but not a type ${0, 1, 2, 4, 8}$. Likewise, in an effect system, you're going to need to make a compromise between precision and decidability, and this compromise is going to depend on how much you expect programmers to annotate their program.

A very simple effect system is to have just two effect types: pure or impure. Any side effect makes an expression impure, and almost anything built from an impure expression is impure. A notable exception to that last statement is that a function abstraction is pure: $(\lambda x. M)$ itself is a pure expression, the effects of $M$ are “hidden” until the function is applied. An example of this in a mainstream language is constexpr in C++, which is an annotation indicating that a piece of code is pure. constexpr on a function means that the function's body is pure.

Another example of an effect system in a mainstream language is the annotations on Java methods that indicate which expressions the method's body can throw. A catch on an exception removes that exception from the expression's potential effects.

If you want to be able to do things like modify a local variable in a function, but have the function still be considered pure, you're going to need a fancier effect system. For an assignment $v := E$, you need to keep track of which variable $v$ is modified, so that the effect “access the mutable variable $v$” can be limited to the scope of $v$. This can get hairy really quickly, since you need to keep track of aliasing, indirect references, etc. The Haskell approach that forces the programmer to explicitly use a monad for any state, even internal state, makes this tracking considerably easier.

Answer 2

Define impure methods and extrapolate from that

This could be done by defining what operations are impure. Things like sockets and streams fall into this category. Then, when you look at a normal function, you can see whether it uses those methods marked impure. If it does, it is impure. Also, if it uses a user-defined function marked impure, then the function also is impure.

Variable accesses must also be checked. If it uses a non-constant non-local variable, it should be considered impure too.

Answer 3

It might be entirely sufficient if a function's implementation never accesses some outside variable :-)

For example, just don't have or don't use global variables within the function's body. Don't read external data from a file/stream or network.

You could test/verify that by simply moving the function into an otherwise empty program environment (empty main which contains nothing but the call of the function, passing in some arguments and returning the result). May modify the arguments (is that another function's problem?), may write/output some data (is that another function's problem?) - as other code/functions would not be pure if they in their implementation read/receive such data, if it's not passed into these as a parameter argument.

Obviously, this way, some optimizations can be performed with functions that are pure. Memoization of the computed/known result for the same parameter arguments (here of course leaking-out/manipulating state elsewhere might be a problem) or parallel or distributed computation of the result are some options, as such would not rely on other state that's external to the function.

It's easier to "verify" function purity by enforcing it, per, for example, a pure programming language not having global variables and not allowing input, reading external state, in function implementations. As this may limit what the language can do (or cause inconvenience), often the attempt is to limit input/reading to a few "dirty" functions, and the state they source/manage is then just passed into various pure functions as arguments for their parameters.