Val(ue) and Var(iable) Declarations

The keywords for introducing value identifiers and variable identifiers are val and var, respectiveily. The essential difference between a value identifier and a variable identifier is that the value referred to by the former cannot be changed during the course of evaluation while the value referred to by the latter can. This difference is clearly reflected in the following two styles of implementation of the factorial function:

// functional style
fn fact_val (x: int): int = loop (x, 1) where {
  fun loop (x: int, res: int): int =
    if x > 0 then loop (x-1, x * res) else res
  // end of [loop]
} // end of [fact_val]

// imperative style
fn fact_var (x: int): int = let
  var x: int = x; var res: int = 1
  val () = while (x > 0) (res := x * res; x := x - 1)
in
  res  
end // end of [fact_var]

In a functional language such as ML, where variable identifiers are not available, an imperative style of implementation of the factorial function may have to be written as follows:


// imperative style based on persistent references, which looks
// awkward and runs inefficiently (in terms of both time and memory)
fn fact_ref (x: int): int = let
  val x = ref<int> (x); val res = ref<int> (1)
  val () = while (!x > 0) (!res := !x * !res; !x := !x - 1)
in
  !res
end // end of [fact_ref]

An implementation as such is often written by a beginner in functional programming who has previously programmed in imperative languages (e.g., C, C++, Java). The function fact_ref is clearly inefficient as each call to it needs to allocate two references on heap (corresponding to x and res), which can only be reclaimed by GC later.

No Local Variable Escapes

In a language like C that supports local variables, many problems are caused by a local variable escaping its legal scope. This, however, is not an issue in ATS as the type system of ATS guarantees that local variables cannot be accessed out of its legal scope (while allowing the addresses of local variables to be passed as function parameters).

We give another implementation of the factorial function as follows that involves passing the addresses of local variables as function parameters:

fun loop {x,res:addr}
  (pf_x: !int @ x, pf_res: !int @ res | p_x: ptr x, p_res: ptr res): void =
  if !p_x > 0 then begin
    !p_res := !p_x * !p_res; !p_x := !p_x - 1; loop (pf_x, pf_res | p_x, p_res)
  end // end of [loop]
// end of [loop]

fn fact_var2 (x: int): int = let
  var x: int = x; var res: int = 1
in
  loop (view@ x, view@ res | &x, &res); res
end // end of [fact_var2]

Each variable identifier is assoicated with two pieces of properties: its address L, which is referred to by the same identifier, and a proof of VT@L, where VT is the viewtype of the content stored at L. For instance, in the implementation of fact_var2, we use view@ x for the proof associated with the variable x and &x for the address of x.

For each variable that is declared of viewtype VT, it is required that a proof of VT?@L is available at the end of the legal scope of the variable, where L is the address of the variable. This requirement guarantees that a local variable, while its address can be taken out of its scope, can never be accessed out of its scope due to the unavailability of a proof needed for accessing the address.

The code used for illustration is available here.