A Tutorial on Programming Features in ATS:
PrevNext

Chapter 14. References

A reference is a singleton array, that is, an array of size 1. It is persistent in the sense that the (heap-allocated) memory for storing the content of a reference cannot be freed manually in a type-safe manner. Instead, it can only be reclaimed through garbage collection (GC).

Given a viewtype VT, the type for references to values of viewtype VT is ref(VT). For convenience, the type constructor ref is declared to be abstract in ATS. However, it can be defined as follows: 

typedef
ref(a:vt@ype) = [l:addr] (vbox(a @ l) | ptr l)

The interfaces for various functions on references can be found in prelude/SATS/reference.sats.

For creating a reference, the function template ref_make_elt of the following interface can be called: 

fun{a:vt@ype} ref_make_elt (x: a):<!wrt> ref(a)

It is also allowed to use the shorthand ref for ref_make_elt. Note that the symbol !wrt indicates that the so-called wrt-effect may occur when ref_make_elt is called.

For reading from and writing through a reference, the function templates ref_get_elt and ref_set_elt can be used, respectively, which are assigned the following types: 

fun{a:t@ype} ref_get_elt (r: ref a):<!ref> a
fun{a:t@ype} ref_set_elt (r: ref a, x: a):<!refwrt> void

Note that the symbol !ref indicates that the so-called ref-effect may occur when ref_get_elt is evaluated. Similarly, !refwrt means both ref-effect and wrt-effect may occur when ref_set_elt. Given a reference r and a value v, ref_get_elt(r) and ref_set_elt(r, v) can be written as !r and !r := v, respectively, and can also be written as r[] and r[] := v, respectively, in terms of bracket-notation.

A reference is typically employed to record some form of persistent state. For instance, following is such an example: 

local
//
#define BUFSZ 128
//
val count = ref<int> (0)
//
in (* in of [local] *)

fun genNewName
  (prfx: string): string = let
  val n = !count
  val () = !count := n + 1
  var res = @[byte][BUFSZ]((*void*))
  val err =
  $extfcall (
    int, "snprintf", addr@res, BUFSZ, "%s%i", prfx, n
  ) (* end of [$extfcall] *)
in
  strptr2string(string0_copy($UNSAFE.cast{string}(addr@res)))
end // end of [genNewName]

end // end of [local]

The function genNewName is called to generate fresh names. As the integer content of the reference count is updated whenever a call to genNewName is made, each name returned by genNewName is guaranteed to have not been generated before. Note that the use of $extfcall is for making a direct call to the function snprintf in C.

Misuse of References References are commonly misused in practice. The following program is often written by a beginner of functional programming who has already learned (some) imperative programming: 

fun fact
  (n: int): int = let
  val res = ref<int> (1)
  fun loop (n: int):<cloref1> void =
    if n > 0 then (!res := n * !res; loop(n-1)) else ()
  val () = loop (n)
in
  !res
end // end of [fact]

The function fact is written in such a style as somewhat a direct translation of the following C code: 

//
int
fact (int n) {
  int res = 1 ;
  while (n > 0) { res = n * res; n = n - 1; } ;
  return (res) ;
}
//

In the ATS implementation of fact, res is a heap-allocated reference and it becomes garbage (waiting to be reclaimed by the GC) after a call to fact returns. On the other hand, the variable res in the C implementation of fact is stack-allocated (or it can even be mapped to a machine register), and there is no generated garbage after a call to fact returns. A proper translation of the C implementation in ATS can actually be given as follows: 

fun fact
  (n: int): int = let
  fun loop (n: int, res: int): int =
    if n > 0 then loop (n-1, n * res) else res
  // end of [loop]
in
  loop (n, 1)
end // end of [fact]

which makes no use of references at all.

Unless strong justification can be given, making extensive use of (dynamically created) references is often a sure sign of poor coding style.

Statically Allocated References Creating a reference by calling ref_make_elt involves dynamic memory allocation. If this is not desirable or even acceptable, it is possible to only employ statically allocated memory in a reference creation as is shown below: 

var myvar: int = 0
val myref = ref_make_viewptr (view@(myvar) | addr@(myvar))

The function ref_make_viewptr takes a pointer and a proof of some at-view associated with the pointer and returns a reference after consuming the proof. As ref_make_viewptr is a cast-function, it causes no run-time overhead. In the above code, myvar is statically allocated and it is no longer available after its at-view proof is consumed by ref_make_viewptr. It should be interesting to observe that both myvar and myref are just the same pointer in C but they are the reification of fundamentally different concepts in ATS: the former is a linear variable while the latter is a non-linear reference.

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

PrevHomeNext
ExceptionsUpBoxed Tuples and Records