Comment by tel
10 years ago
Functions that don't "close over the environment" are ones that are defined in the null environment. Normally you have
Gamma, x : a |- e : b
--------------------------
Gamma |- \x -> e : b
But you could also have "bare functions" if you liked
x : a |- e : b
----------------------
. |- \x -> e : b
This would force all names to be explicitly applied, I think.
The use of 'closure' is an idiomatic shortcut to express that.
Sort of. It's also a didactic method to talk about it and it often is quickly followed with people talking about stack pointers or environment frames. You can blur the lines if you like, but I find it tends to pay to be precise here.