Loop Constructs


In ATS, there are also constructs for forming for-loops and while-loops directly. While it is tempting for someone familiar with imperative programming to implement loops with these constructs (instead of using tail-recursion), it should be emphasized that the amount of effort involved in constructing loop invariants (if needed) often makes this style of programming difficult for beginners and, sometimes, for experts as well.

Simple Loops

The following code gives an implementation of the factorial function, where a while-loop is constructed:
fn fact (n: int): int = let
  var x: int = n
  var res: int = 1 // initialized
  val () = while (x > 0) (res := res * x; x := x - 1)
in
  res // res = n!
end // end of [fact]
The syntax for a while-expression is given as follows:
while $test $body
where $test is an expression of the type bool and $body is an expression of the type void. Usually, $body consists of a sequence of expressions of the type void.

In the following, another implementation of the factorial function is given, where a for-loop is constructed:

// a simple for-loop 
fn fact (n: int): int = let
  var x: int
  var res: int = 1 // initialized
  val () = for (x := 1 ; x <= n ; x := x+1) res := res * x
in
  res // res = n!
end // end of [fact]
The syntax for a for-expression is given as follows:
for ($init ; $test ; $post) $body
where $init is an expression of the type void, $test is an expression of the type bool, $post is an expression of the type void, and $body is an expression of the type void. Usually, $body consists of a sequence of expressions of the type void. Note that each of $init, $test, and $post can be omitted. The meaning of each omission should be evident. The following code gives yet another implemenation of the factorial function:
// a simple for-loop with omissions involving [break]
fn fact (n: int): int = let
  var x: int = 1 // initialized
  var res: int = 1 // initialized
  val () = for ( ; ; ) // infinite loop
    if x <= n then (res := res * x; x := x+1) else break
  // end of [val]
in
  res // res = n!
end // end of [fact]
Note that break in ATS is equivalent to its counterpart in C. Also, continue is supported in ATS as shown in the following implementation of the factorial function:
// a simple for-loop with omissions involving [break] and [continue]
fn fact (n: int): int = let
  var x: int = 1 // initialized
  var res: int = 1 // initialized
  val () = for ( ; ; x := x+1) // no loop test
(*
** note that [continue] means to loop again *after* post increment!
*)
    if x <= n then (res := res * x; continue) else break
  // end of [val]
in
  res // res = n!
end // end of [fact]

Loops with Annotated Invariants

It is also possible to annotate loops with invariants expressed in terms of state types. For such loops, the keywords while* and for* are used in place of while and for, respectively. As an example, the following code implements the standard binary search on an array of doubles:
fn bsearch {n:nat} (
    A: &(@[double][n]), n: int n, key: double
  ) :<> int = let
  var l: int = 0 and u: int = n-1; var res: int = ~1
  val () = while*
    {i,j:int | 0 <= i; i <= j+1; j < n} .<j+1-i>. (l: int i, u: int j) =>
    (l <= u) let
      val m = l + (u-l) / 2
      val sgn = compare (key, A.[m])
    in
      case+ 0 of
      | _ when sgn < 0 => (u := m-1; continue)
      | _ when sgn > 0 => (l := m+1; continue)
      | _ => (res := m; break)
    end // end of [val]
in
  res // 0 <= res < n if [key] is found; or res = ~1 if not
end // end of [bsearch]
The annotated invariant for the loop follows the keyword while*, and it is separated from the rest of the loop by the symbol =>. The invariant states that there are integers i and j satisfying 0 <= i, i <= j+1 and j < n such that the variables l and u are of the types int(i) and int(j), respectively, at the entry point of the loop, that is, the point immediately before the loop test. A termination metric .<j+1-i>. is provided to verify that the loop terminates: the metric must decrease whenever the loop goes back to its entry point.

As another example, an implementation of the factorial function is presented as follows that involves the use of an annotated for-loop:

fn fact {n:nat} (n: int n): int = let
  var x: int
  var res: int = 1
(*
  // the loop invariant indicates that
  // the value of [x] is [n+1] at the point where the loop exits
*)
  val () = for* {i:nat | i <= n+1} .<n+1-i>.
    (x: int i): (x: int (n+1)) => (x := 0; x <= n ; x := x+1) res := res * x
  // end of [val]
in
  res
end // end of [fact]
The annotated invariant for the for-loop follows the keyword for*, and it is separated from the rest of the loop by the symbol =>. This invariant consists of two parts, separated by the colon symbol (:). The part before the colon symbol essentially means that there is a natural number i satisfying i <= n+1 such that the variable x is of the type int(i) at the entry point of the for-loop, that is, at the point immediately after the loop initialization and before the loop test. There is also a termination metric in this part whose meaning should be evident. The part after the colon symbol essentially means that the variable x is of the type int(n+1) at the exit point of the loop.

Annotating loops with invariants correctly can be difficult, sometimes. If complex loop invariants are needed, we recommend that the programmer avoid constructing loops directly. Instead, the programmer can implement tail-recursive functions in place of loops. Note that each tail-recursive function in ATS is guaranteed to be compiled into a loop.


The code used for illustration is available here.