A Tutorial on Programming Features in ATS:
PrevNext

Chapter 26. Linear Closure-Functions

A closure-function is a boxed record that contains a pointer to an envless function plus bindings that map certain names in the body of the envless function to values. In practice, a function argument of a higher-order function is often a closure-function (instead of an envless function). For instance, the following higher-order function list_map_cloref takes a closure-function as its second argument: 

fun{
a:t@ype}{b:t@ype
} list_map_cloref{n:int}
  (xs: list (a, n), f: (a) -<cloref> b): list_vt (b, n)

Closure-functions can be either linear or non-linear, and linear ones can be explicitly freed in a safe manner. The keyword -<cloref> is used to form a type for non-linear closure-functions. As a variant of list_map_cloref, the following higher-order function list_map_cloptr takes a linear closure-function as its second argument: 

fun{
a:t@ype}{b:t@ype
} list_map_cloptr{n:int}
  (xs: list (a, n), f: !(a) -<cloptr> b): list_vt (b, n)

As can be easily guessed, the keyword -<cloptr> is used to form a type for linear closure-functions. Note that the symbol ! indicates that the second argument is still available after a call to list_map_cloptr returns.

A typical example making use of list_map_cloptr is given as follows: 

fun foo{n:int}
(
  x0: int, xs: list (int, n)
) : list_vt (int, n) = res where
{
//
val f = lam (x) =<cloptr> x0 + x
val res = list_map_cloptr (xs, f)
val () = cloptr_free ($UNSAFE.cast{cloptr(void)}(f))
//
} (* end of [foo] *)

Note that a linear closure is first created in the body of the function foo, and it is explicitly freed after its use. The function cloptr_free is given the following interface: 

fun cloptr_free {a:t0p} (pclo: cloptr (a)): void

where cloptr is abstract. The cast $UNSAFE.cast{cloptr(void)}(f) can certainly be replaced with something safer but it would make programming more curbersome.

There is also some interesting interaction between currying and linear closure-functions. In functional programming, currying means turning a function taking multiple arguments simutaneously into a corresponding one that takes these arguments sequentially. For instance, the function acker2 in the following code is a curried version of the function acker, which implements the famous Ackermann function (that is recursive but not primitive recursive): 

fun
acker(m:int, n:int): int =
(
  case+ (m, n) of
  | (0, _) => n + 1
  | (m, 0) => acker (m-1, 1)
  | (_, _) => acker (m-1, acker (m, n-1))
) (* end of [acker] *)

fun acker2 (m:int) (n:int): int = acker (m, n)

Suppose that we apply acker2 to two integers 3 and 4: acker2(3)(4); the application acker2(3) evaluates to a (non-linear) closure-function; the application of this closure-function to 4 evaluates to acker(3,4), which further evaluates to the integer 125. Note that the closure-function generated from evaluating acker2(3) becomes a heap-allocated value that is no longer accessible after the evaluation of acker2(3)(4) finishes, and the memory for such a value can only to be safely reclaimed through garbage collection (GC).

It is also possible to define a curried version of acker as follows: 

fun acker3 (m:int) = lam (n:int): int =<cloptr1> acker (m, n)

While the evaluation of acker3(3)(4) yields the same result as acker2(3)(4), the compiler of ATS (ATS/Postiats) inserts code that automatically frees the linear closure-function generated from evaluating acker3(3) after the evaluation of acker3(3)(4) finishes.

In ATS1, linear closure-functions play a pivotal role in supporting programming with higher-order functions in the absence of GC. Due to advanced support for templates in ATS2, the role played by linear closure-functions in ATS1 is greatly diminished. However, if closure-functions need to be stored in a data structure but GC is unavailable or undesirable, then using linear closure-functions can lead to a solution that avoids the risk of generatig memory leaks at run-time.

Please find on-line the entirety of the code used in this chapter.

PrevHomeNext
Extvar-DeclarationUpStack-Allocated Closure-Functions