Muy rápidamente: una sustitución es "referencialmente transparente" si "sustituir lo similar conduce a lo similar" y una función es "pura" si todos sus efectos están contenidos en su valor de retorno. Ambos pueden hacerse precisos, pero es vital tener en cuenta que no son idénticos ni siquiera uno implica al otro.
Ahora hablemos de los cierres.
"Cierres" aburridos (en su mayoría puros)
Los cierres ocurren porque cuando evaluamos un término lambda interpretamos las variables (enlazadas) como búsquedas de entorno. Por lo tanto, cuando devolvemos un término lambda como resultado de una evaluación, las variables dentro de él habrán "cerrado" los valores que tomaron cuando se definió.
En el simple cálculo lambda esto es algo trivial y toda la noción simplemente desaparece. Para demostrar eso, aquí hay un intérprete de cálculo lambda relativamente liviano:
-- 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)
La parte importante a tener en cuenta es addEnv
cuando aumentamos el entorno con un nuevo nombre. Esta función se llama solo "dentro" del Abs
término de tracción interpretado (término lambda). El entorno se "busca" cada vez que evaluamos un Var
término y, por lo tanto, se Var
resuelve lo que sea que se Name
mencionó en el Env
que fue capturado por la Abs
tracción que contiene el Var
.
Ahora, nuevamente, en términos simples de LC esto es aburrido. Significa que las variables enlazadas son solo constantes en lo que a nadie le importa. Se evalúan de forma directa e inmediata como los valores que denotan en el entorno como alcances léxicos hasta ese punto.
Esto también es (casi) puro. El único significado de cualquier término en nuestro cálculo lambda está determinado por su valor de retorno. La única excepción es el efecto secundario de la no terminación que se incorpora en el término Omega:
-- 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")))
Cierres (impuros) interesantes
Ahora, para ciertos entornos, los cierres descritos en el LC simple anterior son aburridos porque no existe la noción de poder interactuar con las variables que hemos cerrado. En particular, la palabra "cierre" tiende a invocar código como el siguiente 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
Esto demuestra que hemos cerrado la n
variable en la función interna incr
y que la llamada incr
interactúa significativamente con esa variable. mk_counter
es puro, pero incr
es decididamente impuro (y tampoco es referencialmente transparente).
¿Qué difiere entre estas dos instancias?
Nociones de "variable"
Si observamos qué significan sustitución y abstracción en el sentido claro de LC, notamos que son decididamente simples. Las variables son literalmente nada más que búsquedas de entorno inmediatas. Lambda abstracción es, literalmente, nada más que la creación de un entorno aumentada para evaluar la expresión interior. No hay espacio en este modelo para el tipo de comportamiento que vimos con mk_counter
/ incr
porque no hay variación permitida.
Para muchos, este es el corazón de lo que significa "variable": variación. Sin embargo, a los semánticos les gusta distinguir entre el tipo de variable utilizada en LC y el tipo de "variable" utilizada en Javascript. Para hacerlo, tienden a llamar a este último una "celda mutable" o "ranura".
Esta nomenclatura sigue el largo uso histórico de "variable" en matemáticas donde significaba algo más como "desconocido": la expresión (matemática) "x + x" no permite x
variar con el tiempo, sino que tiene un significado independientemente del valor (único, constante) x
toma.
Por lo tanto, decimos "ranura" para enfatizar la capacidad de poner valores en una ranura y eliminarlos.
Para agregar más a la confusión, en Javascript estas "ranuras" se ven igual que las variables: escribimos
var x;
para crear uno y luego cuando escribimos
x;
nos indica buscando el valor actualmente almacenado en ese espacio. Para hacer esto más claro, los lenguajes puros tienden a pensar en las tragamonedas como nombres de nombres (matemáticos, cálculo lambda). En este caso, debemos etiquetar explícitamente cuándo obtenemos o colocamos desde una ranura. Tal notación tiende a parecerse a
-- 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
La ventaja de esta notación es que ahora tenemos una distinción firme entre variables matemáticas y ranuras mutables. Las variables pueden tomar ranuras como sus valores, pero la ranura particular nombrada por una variable es constante en todo su alcance.
Usando esta notación podemos reescribir el mk_counter
ejemplo (esta vez en una sintaxis similar a la de Haskell, aunque decididamente una semántica similar a la de Haskell):
mkCounter =
let x = newSlot
in (\() -> let old = get x
in get (put x (old + 1)))
En este caso, estamos utilizando procedimientos que manipulan esta ranura mutable. Para implementarlo, necesitaríamos cerrar no solo un entorno constante de nombres, x
sino también un entorno mutable que contenga todos los espacios necesarios. Esto está más cerca de la noción común de "cierre" que la gente ama tanto.
De nuevo, mkCounter
es muy impuro. También es muy referencialmente opaco. Pero tenga en cuenta que los efectos secundarios no surgen de la captura o el cierre del nombre, sino de la captura de la célula mutable y las operaciones de efectos secundarios en ella como get
y put
.
En última instancia, creo que esta es la respuesta final a su pregunta: la pureza no se ve afectada por la captura de variables (matemáticas) sino por las operaciones de efecto secundario realizadas en ranuras mutables nombradas por variables capturadas.
Es solo que en los idiomas que no intentan estar cerca de LC o no intentan mantener la pureza, estos dos conceptos a menudo se combinan y generan confusión.
y
no puede cambiar, por lo que la salida def(3)
siempre será la misma.y
es parte de la definición def
aunque no esté marcado explícitamente como una entrada paraf
- sigue siendo el caso quef
se define en términos dey
(podríamos denotar la función f_y, para hacer que la dependencia seay
explícita), y por lo tanto el cambioy
da una función diferente . La función particularf_y
definida para un particulary
es muy pura. (Por ejemplo, las dos funcionesf: x -> x + 3
yf: x -> x + 5
son diferentes funciones, y ambos puro, a pesar de que pasó a utilizar la misma letra para denotar ellos.)