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$ 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
    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$ 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
    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$ May 23, 2023 at 22:38

2 Answers 2

7
$\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
    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$ May 23, 2023 at 22:10

You must log in to answer this question.

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