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)
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] *)
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)
It is also possible to define a curried version of acker as follows:
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.