Very quickly: a substitution is "referentially transparent" if "substituting like leads to like" and a function is "pure" if all of its effects are contained in its return value. Both of those can be made precise, but it's vital to note that they are not identical nor even does one imply the other.
Now let's talk about closures.
Boring (mostly pure) "closures"
Closures occur because as we evaluate a lambda term we interpret (bound) variables as environment lookups. Thus, when we return a lambda term as the result of an evaluation the variables inside it will have "closed over" the values they took when it was defined.
In plain lambda calculus this is sort of trivial and the whole notion just vanishes. To demonstrate that, here's a relatively lightweight lambda calculus interpreter:
-- untyped lambda calculus values are functions
data Value = FunVal (Value -> Value)
-- we write expressions where variables take string-based names, but we'll
-- also just assume that nobody ever shadows names to avoid having to do
-- capture-avoiding substitutions
type Name = String
data Expr
= Var Name
| App Expr Expr
| Abs Name Expr
-- We model the environment as function from strings to values,
-- notably ignoring any kind of smooth lookup failures
type Env = Name -> Value
-- The empty environment
env0 :: Env
env0 _ = error "Nope!"
-- Augmenting the environment with a value, "closing over" it!
addEnv :: Name -> Value -> Env -> Env
addEnv nm v e nm' | nm' == nm = v
| otherwise = e nm
-- And finally the interpreter itself
interp :: Env -> Expr -> Value
interp e (Var name) = e name -- variable lookup in the env
interp e (App ef ex) =
let FunVal f = interp e ef
x = interp e ex
in f x -- application to lambda terms
interp e (Abs name expr) =
-- augmentation of a local (lexical) environment
FunVal (\value -> interp (addEnv name value e) expr)
The important part to notice is in addEnv
when we augment the environment with a new name. This function gets called only "inside" of the interpreted Abs
traction term (lambda term). The environment gets "looked up" whenever we evaluate a Var
term and so those Var
s resolve to whatever the Name
referred to in the Env
which got captured by the Abs
traction containing the Var
.
Now, again, in plain LC terms this is boring. It means that bound variables are just constants as far as anyone cares. They get evaluated directly and immediately as the values they denote in the environment as lexically scoped up to that point.
This is also (almost) pure. The only meaning of any term in our lambda calculus is determined by its return value. The only exception is the side-effect of non-termination which is embodied by the Omega term:
-- in simple LC syntax:
--
-- (\x -> (x x)) (\x -> (x x))
omega :: Expr
omega = App (Abs "x" (App (Var "x")
(Var "x")))
(Abs "x" (App (Var "x")
(Var "x")))
Interesting (impure) closures
Now to certain backgrounds the closures described in plain LC above are boring because there's no notion of being able to interact with the variables we've closed over. In particular, the word "closure" tends to invoke code like the following Javascript
> function mk_counter() {
var n = 0;
return function incr() {
return n += 1;
}
}
undefined
> var c = mk_counter()
undefined
> c()
1
> c()
2
> c()
3
This demonstrates that we've closed over the n
variable in the inner function incr
and calling incr
meaningfully interacts with that variable. mk_counter
is pure, but incr
is decidedly impure (and not referentially transparent either).
What differs between these two instances?
Notions of "variable"
If we look at what substitution and abstraction mean in the plain LC sense we notice that they are decidedly plain. Variables are literally nothing more than immediate environment lookups. Lambda abstraction is literally nothing more than creating an augmented environment to evaluate the inner expression. There is no room in this model for the kind of behavior we saw with mk_counter
/incr
because there's no variation allowed.
To many this is the heart of what "variable" means—variation. However, semanticists like to distinguish between the kind of variable used in LC and the kind of "variable" used in Javascript. To do so, they tend to call the latter a "mutable cell" or "slot".
This nomenclature follows the long historical usage of "variable" in mathematics where it meant something more like "unknown": the (mathematical) expression "x + x" does not allow for x
to vary over time, it instead is meant to have meaning regardless of the (single, constant) value x
takes.
Thus, we say "slot" to emphasize the ability to put values into a slot and to take them out.
To add further to the confusion, in Javascript these "slots" look the same as variables: we write
var x;
to create one and then when we write
x;
it indicates us looking up the value currently stored in that slot. To make this more clear, pure languages tend to think of slots as taking names as (mathematical, lambda calculus) names. In this case we must explicitly label when we get or put from a slot. Such notation tends to look like
-- create a fresh, empty slot and name it `x` in the context of the
-- expression E
let x = newSlot in E
-- look up the value stored in the named slot named `x`, return that value
get x
-- store a new value, `v`, in the slot named `x`, return the slot
put x v
The advantage of this notation is that we now have a firm distinction between mathematical variables and mutable slots. Variables may take slots as their values, but the particular slot named by a variable is constant throughout its scope.
Using this notation we can rewrite the mk_counter
example (this time in a Haskell-like syntax, though decidedly un-Haskell-like semantics):
mkCounter =
let x = newSlot
in (\() -> let old = get x
in get (put x (old + 1)))
In this case we're using procedures which manipulate this mutable slot. In order to implement it we'd need to close over not only a constant environment of names like x
but also a mutable environment containing all of the needed slots. This is closer to the common notion of "closure" people love so much.
Again, mkCounter
is very impure. It's also very referentially opaque. But notice that the side-effects do not arise from the name capture or closure but instead the capture of the mutable cell and the side-effecting operations on it like get
and put
.
Ultimately, I think this is the final answer to your question: purity is not affected by (mathematical) variable capture but instead by side-effecting operations performed on mutable slots named by captured variables.
It's only that in languages which do not attempt to be close to LC or do not attempt to maintain purity that these two concepts are so often conflated leading to confusion.
y
can't change, so the output off(3)
will always be the same.y
is part of the definition off
even though it's not explicitly marked as an input tof
— it's still the case thatf
is defined in terms ofy
(we could denote the function f_y, to make the dependence ony
explicit), and therefore changingy
gives a different function. The particular functionf_y
defined for a particulary
is very much pure. (For example, the two functionsf: x -> x + 3
andf: x -> x + 5
are different functions, and both pure, even though we happened to use the same letter to denote them.)