Bluish Coder

My last post on ATS was about C style functions. This post covers what I've learnt about closures in ATS.

As I mentioned in my last post, closures are functions combined with an environment mapping names to values. These are like closures in dynamic languages that enable you to capture variables in the enclosing scope. To create a closure you must explicitly mark it as being a closure. A closure requires memory to be allocated to store the environment. This means you will either need to allocate the closure on the stack (so it is freed automatically when the scope exits), free the memory for the closure manually, or link against the garbage collector.

Persistent Closures

A persistent closure is allocated on the heap and is freed by the garbage collector when it is no longer used. To make this type of closure you use the tag 'cloref':

fun make_adder(n1:int): int -<cloref> int =
  lam (n2) =<cloref> n1 + n2;

implement main() = let
  val add5 = make_adder(5)
  val a = add5(10)
  val b = add5(20)
  val () = printf("a: %d\nb: %d\n", @(a,b))
in
  ()
end

As this example needs to use the garbage collector it must be built with the garbage collector included (using the -D_ATS_GCATS switch):

atscc -o eg1 eg1.dats -D_ATS_GCATS

In this example the 'make_adder' function takes an integer, n1, and returns a closure. This closure takes an integer, 'n2' and returns the addition of 'n1' and 'n2'. The 'main' function creates an adder with the initial function of '5' and uses the returned closure a couple of times.

Linear Closures

A linear closure is not freed by the garbage collector. It is the responsiblity of the programmer to free the memory manually. It is tracked by the type system and it is a compile time error to not call the function to free the linear closure. Linear closures have the tag 'cloptr'. The same example as before but using linear closures is:

fun make_adder(n1:int): int -<cloptr> int =
  lam (n2) =<cloptr> n1 + n2;

implement main() = let
  val add5 = make_adder(5)
  val a = add5(10)
  val b = add5(20)
  val () = printf("a: %d\nb: %d\n", @(a,b))
  val () = cloptr_free(add5)
in
  ()
end

Note the change from 'cloref' to 'cloptr' in the function tags, and the addition of a 'cloptr_free' call at the end of 'main'. If you leave out the 'cloptr_free' call then a compile time error results:

$ atscc -o closure2 closure2.dats
...
error(3): the linear dynamic variable [add5] needs to be consumed but it is preserved...
...

Because we are manually managing the memory the usage of linear closures does not require the garbage collector.

Stack Allocated Closures

It is possible to allocate linear closures on the stack rather than the heap. When this is done there is no need to free the memory manually as it is automatically deallocated when the stack scope exits:

implement main() = let
  var !add5 = @lam(n2:int) => 5 + n2
  val a = !add5(10)
  val b = !add5(20)
  val () = printf("a: %d\nb: %d\n", @(a,b))
in
  ()
end

A closure is allocated on the stack using '@lam' instead of 'lam'. This is assigned to a variable 'add5'. The variable is introduced using 'var' instead of 'val' which the examples have been using so far. 'val' is for 'value declarations' and 'var' is for 'variable declarations'. The latter are basically variables allocated on the stack that can be changed during the course of evaluation. See the val and var tutorial for details.

Variables allocated on the stack have an implicit proof variable that is used to allow access to its address. The use of '!' in the example appears to be a shorthand provided by ATS that can be used to avoid explicitly managing the proof's in some circumstances. I don't entirely understand why this is needed or how it works. If anyone has any helpful tips please let me know. The pointer tutorial seems to have some coverage of this.

For this example I don't create the closure in a 'make_adder' function. If the closure was allocated on the stack and returned from 'make_adder' it would be an error as we'd be returning a stack allocated object from a stack that just got destroyed. In ATS it is guaranteed by the type system that a closure allocated on the stack frame of a function cannot be used once the call to the function returns. A compile time warning occurs if this happens:

error(3): a flat closure is needed.

Standard Prelude Higher Order Functions

ATS has implementations of the usual higher order functions over lists and arrays. Things like 'map', 'filter', etc are available. The following example show's using higher order functions to sum a list:

staload "prelude/DATS/list.dats"

implement main() = () where {
  val a = '[1,2,3]
  val x = list_fold_left_cloref<int,int> (lam (a,b) =<cloref> a*b, 1, a)
  val () = printf("result: %d\n", @(x));
}

The 'list_fold_left_cloref' is defined in 'prelude/DATS/lists.dats'. It's a function template (similar to C++ templates) and needs the template types to be passed to it to be instantiated. In this case the types are both int's. This version of the code requires the garbage collector due to the use of 'cloref'.

Variants of list_fold_left exist for use with linear closures, functions, etc. For example, with a linear closure:

staload "prelude/DATS/list.dats"

implement main() = () where {
  val a = '[1,2,3]
  val clo = lam (pf: !unit_v | a:int,b:int):int =<cloptr> a*b;
  prval pfu = unit_v ()
  val x = list_fold_left_cloptr<int,int> (pfu | clo, 1, a)
  prval unit_v () = pfu
  val () = cloptr_free(clo)
  val () = printf("result: %d\n", @(x));

}

You'll notice the use of 'prval' in this version. The definition of 'list_fold_left_cloptr' is:

fun{init,a:t@ype} list_fold_left_cloptr {v:view} {f:eff}
  (pf: !v | f: !(!v | init, a) -<cloptr,f> init, ini: init, xs: List a):<f> init

This shows that both 'list_fold_left_cloptr' and the argument 'f' need a proof argument (anything to the left of the pipe '|' character, '!v' in this case). The example doesn't make use of the proof argument so we create one (unit_v ()) and release it later (the second 'prval' usage). Like I mentioned with proofs before, I don't quit understand why this takes a proof argument or why it passes it to the closure. Enlightenment in the comments would be welcome!

Note that even though this example manually manages memory for the closure it still needs the garbage collector for the allocation of the list stored 'a'. Even with the garbage collector included you can still manage memory manually for efficiency reasons if needed.

If using proof variables, manually managing closure memory, and related functionality proves to much of a burden then ATS provides alternative functions. The 'smlbas' routines provide much of the ML basis standard library implemented to use 'cloref1' function types. For example:

staload "libats/smlbas/SATS/list.sats"
staload "libats/smlbas/DATS/list.dats"
dynload "libats/smlbas/DATS/list.dats"

implement main() = () where {
  val a = list0_of_list1('[1,2,3])
  val x = foldl<int,int>(lam(a, b) => a + b, 1, a)
  val () = printf("result: %d\n", @(x));
}

This needs to be linked against the 'ats_smlbas' library to build:

atscc -o closure8 closure8.dats -D_ATS_GCATS -lats_smlbas

I had to pass the types to the 'foldl' template to get things to compile. Type inference is unfortunately not as simple as in some other functional languages. An alternative approach is to specify that you want to use the integer add function:

  val x = foldl(lam(a, b) => add_int_int(a, b), 1, a)

Unfortunately it wasn't enough to declare the types for the closure arguments:

  val x = foldl(lam(a:int, b:int) => a + b, 1, a)

This gives the error:

  error(3): the symbol [+] cannot be resolved: there are too many matches

Conclusion

This concludes my explorations of using closures and functions in ATS. I find using higher order functions somewhat difficult due to dealing with proofs and having to declare types everywhere.

This would probably be a bit easier if there was reference documentation on the ATS standard library with usage examples. Unfortunately I'm not aware of any apart from the library and example source code.

At least it's possible to use the 'smlbas' library and the simplified 'list0' and 'array0' types to avoid needing to understand the low level details of proofs and types while learning.