Envless Functions and Closure Functions

I use envless as a shorthand for environmentless, which is not a legal word but I guess 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, 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 eventually leads to an error indicating that loop cannot be compiled into a toplevel function in C. The reason for this 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 (for representing closure functions) at run-time.

The need for creating closures often appears when the return value of a function call is a function itself. For instance, the following 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 that is assigned 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.