Envless Functions and Closure-Functions

I use envless as a shorthand for environmentless, which is not a legal word but I suppose that you have no problem figuring out what it means.

An envless function is represented by a pointer pointing to some place in a code segment where the object code for executing a call to this function is located. Every function in the programming language C is envless. A closure-function is also represented by a pointer, but the pointer points to some place in a heap where a tuple is allocated (at run-time). Usually, the first component of this tuple is a pointer representing an envless function and the rest of the components represent some bindings. A tuple as such is often referred to as a closure-function or simply closure, which can be thought of as an envless function paired with an environment. It is possible that the environment of a closure-function is empty, but this does not equate a closure-function with an envless function. Every function in functional languages such as ML and Haskell is a closure-function.

In the following example, the function sum, which is assigned the type (int) -> int, sums up all the integers between 1 and a given natural number:

fun sum (n: int): int = let fun loop ( i: int, res: int ) :<cloref1> int = if i <= n then loop (i+1, res+i) else res // end of [loop] in loop (1(*i*), 0(*res*)) end // end of [sum]

The inner function loop is a closure-function as is indicated by the special syntax :<cloref1>, and the type assigned to loop is denoted by (int, int) -<cloref1> int. Hence, envless functions and closure-functions can be distinguished at the level of types.

If the syntax :<cloref1> is replaced with the colon symbol : alone, the code can still pass typechecking but its compilation may eventually lead to a warning or even an error indicating that loop cannot be compiled into a toplevel function in C. The reason for this warning/error is due to the body of loop containing a variable n that is neither at toplevel nor a part of the arguments of loop itself. It is straightforward to make loop an envless function by including n as an argument in addition to the original ones:

fun sum (n: int): int = let fun loop ( n:int, i: int, res: int ) : int = if i <= n then loop (n, i+1, res+i) else res // end of [loop] in loop (n, 1(*i*), 0(*res*)) end // end of [sum]

As a matter of fact, what happens during compilation is that the first implementation of sum and loop gets translated, more or less, into the second implementation, and there is no actual creation of closures at run-time.

The need for creating closures often appears when a function is not directly applied. For instance, the return value of a function call may also be a function. In the following code, the defined function addx returns another function when applied to a given integer x, and the returned function is a closure-function, which always adds the integer x to its own argument:

// fun addx (x: int): int -<cloref1> int = lam y => x + y // val plus1 = addx (1) // [plus1] is of the type int -<cloref1> int val plus2 = addx (2) // [plus2] is of the type int -<cloref1> int //

It should be clear that plus1(0) and plus2(0) return 1 and 2, respectively. The closure-function that is given the name plus1 consists of an envless function and an environment binding x to 1. The envless function can essentially be described by the pseudo syntax lam (env, y) => env.x + y, where env and env.x refer to an environment and the value to which x is bound in that environment. When evaluating plus1(0), we can first bind env and y to the environment in plus1 and the argument 0, respectively, and then start to evaluate the body of the envless function in plus1, which is env.x + y. Clearly, this evaluation yields the value 1 as is expected.

Closures are often passed as arguments to functions that are referred to as higher-order functions. It is also fairly common for closures to be embedded in data structures.