7
$\begingroup$

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.

$\endgroup$
8
  • $\begingroup$ In Haskell, all impure functions are encapsulated in the IO monad. You can do that. Or are you asking for, given an IO action, a way to verify whether it's pure? $\endgroup$ Commented May 23, 2023 at 22:06
  • $\begingroup$ @DannyuNDos I don't follow your comment. Haskell is not an imperative language, and the goal is not to require all functions to be pure or to change the way that impure functions should be written. The idea is to allow the programmer to label functions as pure when they are pure, and the goal is to have the compiler check that they are. $\endgroup$
    – kaya3
    Commented May 23, 2023 at 22:10
  • 1
    $\begingroup$ Haskell is an imperative language: it can express programs with side effects. Unlike most imperative language, Haskell's type system can identify pure programs: they're expressions that don't need to be placed in a stateful monad. (@DannyuNDos not all impure function are in IO, there are also monads for internal side effects like ST.) That's one way to achieve exactly what you're asking for. $\endgroup$ Commented May 23, 2023 at 22:28
  • 2
    $\begingroup$ Haskell can express programs with side-effects by representing side-effects as data so that they can be returned by pure functions. This is not how side-effects work in the imperative paradigm; in imperative languages, you just write a statement which expresses some side-effect, and when the statement is executed, the side-effect occurs. The goal here is to verify pure functions, not change the way impure functions have to be written in order to make them pure. That said, if you think Haskells way of doing things could be applied in the imperative paradigm, feel free to write an answer. $\endgroup$
    – kaya3
    Commented May 23, 2023 at 22:32
  • $\begingroup$ By the way, given your questions, I think that you haven't read ATTAPL, and you should (at least the chapters that interest you, and then look at the “further reading” sections). For this question, “linear type” and “effect types” are relevant — unfortunately that book doesn't have a unified chapter on the general topic. $\endgroup$ Commented May 23, 2023 at 22:38

3 Answers 3

8
$\begingroup$

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.

$\endgroup$
1
4
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ This works but it's overly conservative ─ it means pure functions aren't allowed to mutate objects even if those mutations will never be externally visible. $\endgroup$
    – kaya3
    Commented May 23, 2023 at 22:08
  • $\begingroup$ @kaya3 It's worth to mention the State monad. It emulates mutation while still being pure by its own. $\endgroup$ Commented May 23, 2023 at 22:10
-1
$\begingroup$

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.

New contributor
skreutzer is a new contributor to this site. Take care in asking for clarification, commenting, and answering. Check out our Code of Conduct.
$\endgroup$
7
  • $\begingroup$ There is no apparent relationship between "a function's implementation never accesses some outside variable" and "Don't read external data from a file/stream or network.". IO operations are often done without accessing external variables. So your second paragraph demonstrates that your test is not sufficient. On the other hand, functions which access outside variables can be pure, e.g. in JavaScript function() { let a = 1; a += 2; return () => a; } returns a pure function despite that it accesses a non-local mutable variable. So your test has both false positives and true negatives. $\endgroup$
    – kaya3
    Commented 2 days ago
  • $\begingroup$ Side-effects make a function non-pure, no? Because based on these, for the same call/parameters, you get a different result. External state causing such a side-effect can be accessing outside variables, or the different and changing state of an external data source (files, network). Might not be apparent to you, but isn't this the case nonetheless? For your JavaScript function, isn't a a local variable not accessing external state, so the result is always 3 (not considering captures/closures, but it'll reliably always produce a new a value reference or whatever)? $\endgroup$
    – skreutzer
    Commented 2 days ago
  • $\begingroup$ Side-effects make a function impure. However, you propose as a sufficient condition that "a function's implementation never accesses some outside variable". Since a function can have side-effects despite satisfying your condition, that shows that your condition is not sufficient. In my JavaScript example, a is a non-local mutable variable captured by the closure () => a, showing that your condition is also not a necessary condition. $\endgroup$
    – kaya3
    Commented 2 days ago
  • $\begingroup$ You're probably referencing this langdev.stackexchange.com/a/1340/5447 which is, if the function implementation itself is not pure by being a data source (for example, by generating different output by using some construct that does that). Indeed my "test" does not help with "emitting" what can become a side effect to something else. I guess in my mind, the "purity" attribute/property has the two components of external input for the function implementer vs. output to external for the caller. "Pure" likely refers to both, while output to external is someone else's/caller's problem. $\endgroup$
    – skreutzer
    Commented 2 days ago
  • 1
    $\begingroup$ I'm not referencing that, the problem is much simpler than referential transparency. In C, for example, void foo() { printf("Hello, world!\n"); } is a function which "never accesses some outside variable". (Note that in C, named functions are not variables.) Or in Python, def foo(p): p("Hello, world!") is impure when called like foo(print). Likewise, the Python function "never accesses some outside variable". These counterexamples show that your proposed condition is not sufficient for a function to be pure. $\endgroup$
    – kaya3
    Commented 2 days ago

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .