Lambda the Ultimate

Second, some people claim that some lanuages don't have real closures because while the enclosed function has access to the values of variables in the enclosing environment, it is not able to revise the variables.

In a language with mutable variables, especially implicitly mutable variables, if you "close over" the bindings to those variables you should be able to mutate them (and have the changes reflected outside of the lexical scope). If not, you don't have lexical closures. But as you mention, the lack of this ability leads to a pointless and unnatural decrease in expressiveness or at least some annoying awkwardness, which is probably what people are more complaining about.

Second, some people claim that some lanuages don't have real closures because while the enclosed function has access to the values of variables in the enclosing environment, it is not able to revise the variables. So, for instance, in these languages you can't use closures to create a count function that returns an incremented value with each call. My conclusion here is that there is nothing in the definition of closures that require the ability to revise the environment; however for many people this is an important bit of functionality that they expect from any language that has closures. Saying the language doesn't have real closures is a way of expressing their disappointment. But again there is not fact to the matter here.

There are some relevant facts. Derek responded in general terms, but to take a specific example, in Java, you can create a kind of restricted closure, i.e. an anoynymous inner class which is capable of closing over any final (non-mutable) variables in the enclosing scope. Conversely, though, this means that an anonymous inner class cannot close some kinds of lexical variables (i.e. non-final ones). That's a factual limitation on the closure capability of Java. Whether that makes its closures less "real" is of course not a formal judgement (until someone gives a definition of "real closures" in a paper, perhaps along the lines of "proper tail recursion" ;-)

BTW, as Oleg points out in Closures without assignment, in lambda calculus (and by extension, in typical purely functional languages) closures aren't strictly necessary:

In lambda-calculus, abstractions are first class: we can apply abstractions to abstractions and get abstractions as the result. There are no closures -- only substitutions. Granted, doing substitutions is expensive, therefore, it makes sense to delay them and execute by need. Thus environment was invented as a list of pending substitutions. Now, when we pass an abstraction around, we also need to pass the list of substitutions that should be performed but weren't — we need to enclose the environment. The environment is merely a lazy substitution, an optimization technique.

This is the reason you don't see closures mentioned much in the Haskell context — because in that context, they're just an optimization technique. However, Oleg goes on to point out:

Closures are a big deal in a non-pure language, because mutable closed-over lexical variables can model an encapsulated mutable
state.

IOW, it's no coincidence that the languages in which one hears the most talk about closures are the ones which support mutable closed-over variables.

Here's a definition from EOPL (sec. 3.5, p. 85):

In order for a procedure to retain the bindings that its free variables had at the time it was created, it must be a closed package, independent of the environment in which it is used. Such a package is called a closure. In order to be self contained, a closure must contain the procedure body, the list of formal parameters, and the bindings of its free variables... We sometimes say the procedure is closed over or closed in its creation environment."

The semantic concept of "closure" is really not complicated, or ambiguous. However, things can get messy because the way in which the concept applies in a given language depends on the language. As Derek alluded to, concepts tend to get confused with implementation dependencies. The best way to avoid this confusion is to understand the semantic concept via a general theoretical model, which you can then map to specific languages. As you say, that requires some studying of theory.

Beginning to make sense, let me see if I can apply theory to a language I know. Consider k. K does not have lexically-scoped variables: variables are either global or local to a function. However you can do the following:

incr:{[incr] :{x+incr}}

incr is a function that returns an incrementor function:

  by1:incr[1]
  by1 3
4
  by1 5
6
  by2:incr[2]
  by2 3
5

Don't get confused by the curly brackets, it is k's lambda notation and doesn't indicate lexical context. There are a few statements I want to make about this example:
1 - This is an example of closure where the free variable in the returned functioned is closed off by the argument passed to the incr function.
2 - Strictly speaking this can't be a lexical closure because there is no lexical scoping in k, but this would take matters too literally. Lexical closures don't require lexical scoping but a reference to an environment that was present at the time the function was defined.
3 - You cannot revise the variables in a k closure but that's because k only has global and local variables. It is not the result of a restriction on k closures.

K does not have lexically-scoped variables: variables are either global or local to a function.
...
Don't get confused by the curly brackets, it is k's lambda notation and doesn't indicate lexical context.

I don't believe you. :)

In incr:{[incr] :{x+incr}}, the inner "lambda" references a parameter incr which is defined in, and local to, the outer lambda. Also, the inner lambda uses an implicit parameter x which is local to that lambda. This is almost certainly lexical scoping. (Otherwise, if dynamic scope is involved somehow, I would expect some variation of the funarg problem to apply.)

The example function looks to me to be equivalent to the following Scheme definition:

(define incr (lambda (incr) (lambda (x) (+ x incr))))

Note that since no mutation is involved in this example, uses of this function can be modelled using substitution and so strictly speaking there's no need for closures. See my comment entitled "Real closures". However, closures and an environment model of evaluation may still be useful as a reasoning tool.

3 - You cannot revise the variables in a k closure but that's because k only has global and local variables. It is not the result of a restriction on k closures.

This needs to be revised in light of my comments above. For example, what happens with code such as the following:

counter:{[n] :{n::n+1; n}}
c:counter[4]
c[]
c[]
c[]

I'm attempting with n::n+1 to increment the n defined in the outer lambda. The issue here is not that "k only has global and local variables", although it may be that mutation of locals defined in an enclosing scope is not allowed. (Perhaps my code would define 'n' as a new global?) In that case, this certainly seems to be a restriction on k closures (given that mutation of local variables is normally allowed).

OK, I think I'm with you. I had a subtle but fundamental misunderstanding about lexical closures and your first remark clears this up.

In regards to the k example, this is what you get:

  counter:{[n] :{n::n+1; n}}
  c:counter[4]
  c[]
5
  c[]
5
  c[]
5

I was pretty sure this wasn't going to work the way you expected, but I'm equally surprised by the result. I did a bit of research and here are the two relevent passages from the k reference manual:

. . . local names are strictly local, in that their values cannot be seen outside the function expression or inside any function called within the function expression.

and

Suppose that the function g is defined within the body of another functin f and uses the variable x in its definition, where x is local to f. then x is a constant in g, not a variable, and its value is the currente one when g is defined.

You're right that the double :: indicates global assignment. The problem is that no global variable is created when the above code is run. In any case I just don't see how this function can run without producing an error. That's my problem and not really relevent to the present discussion, but I thought you might be curious.

In regards to the k example, this is what you get:

  counter:{[n] :{n::n+1; n}}
  c:counter[4]
  c[]
5
  c[]
5
  c[]
5

I was pretty sure this wasn't going to work the way you expected, but I'm equally surprised by the result.

The result would be the same for:

  counter:{[n] :{m::n+1; m}}
  c:counter[4]

Wouldn't it? Except that a global variable should be created, if :: is for defining globals...

As for closures, if the closure needs to mutate a variable in the environment why not pass that variable along with the closure and use it as an argument to the closure? It would force the programmer to tell explicitely which variables he is leaking from the current environment.