Effects

In this third unit of the course, we’ll look at extensions to the λ-calculus, called effects, that make the language less “pure” but more like most programming languages you’ve used (including Scheme and ML). Some examples of effects include being able to modify the value of a memory cell, or to raise an exception.

We’ve seen plenty of examples of extensions of the λ-calculus that are macro-expressible [1], meaning that they can be defined with definitions like

zro ≡ λs. λz. z                     (1)

This definition says that wherever we write zro, we really mean λs. λz. z. One property of such extensions is that they don’t change any basic guarantees of the language. For example, in pure λ-calculus, for any t1 and t2, if z does not occur free in t2, then it’s always the case that

(let z = t1 in t2) = t2             (2)

because it evaluates t1, discards its value, then evaluates t2. Adding definitions like (1) can’t break this guarantee.

But imagine that t1 could do something like change the value of a variable, or exit the program. Things like that would indeed break guarantee (2). As a consequence, they are not macro-expressible in the pure lambda calculus.

This final unit of the course is about these “impure” extensions, called effects. For each effect, we’ll show how to extend the language to include the effect, following TAPL. We’ll also show how to translate programs that use the effect into programs that don’t. However, as we will see, these translations aren’t like the translation of zro above; they are more complicated whole-program transformations.