What is a “free variable”?

Question

(I'm sure this must have been answered on this site already, but search gets inundated with the concept of calling free() on a variable in C.)

I came across the term "eta reduction," which was defined something like f x = M x ==> M if x is "not free in M". I mean, I think I understand the gist of what it's trying to say, it seems like what you do when you convert a function to point-free style, but I don't know what the qualifier about x not being free means.

Answer 1

Here's an example:

\f -> f x

In this lambda, x is a free variable. Basically a free variable is a variable used in a lambda that is not one of the lambda's arguments (or a let variable). It comes from outside the context of the lambda.

Eta reduction means we can change:

(\x -> g x) to (g)

But only if x is not free (i.e. it is not used or is an argument) in g. Otherwise we'd be creating an expression which refers to a unknown variable:

(\x -> (x+) x) to (x+) ???

Answer 2

Well, here's the relevant Wikipedia article, for what that's worth.

The short version is that such definitions elide the body of a lambda expression using a placeholder like "M", and so have to specify additionally that the variable being bound by that lambda isn't used in whatever the placeholder represents.

So, a "free variable" here roughly means a variable defined in some ambiguous or unknown outer scope--e.g., in an expression like \y -> x + y, x is a free variable but y is not.

Eta reduction is about removing a superfluous layer of binding and immediately applying a variable, which is (as you would probably imagine) only valid if the variable in question is only used in that one place.