Introduction to Programming in ATS:
<<< Previous	Introduction to Dependent Types	Next >>>

Example: Dependent Types for Debugging

Given an integer x >= 0, the integer square root of x is the greatest integer i satisfying i * i <= x. An implementation of the integer square root function is given as follows based on the method of binary search:

fun isqrt (x: int): int = let
  fun search (x: int, l: int, r: int): int = let
    val diff = r - l
  in
    case+ 0 of
    | _ when diff > 0 => let
        val m = l + (diff / 2)
      in
        // x < m * m is more efficient but can overflow easily
        if x / m < m then search (x, l, m) else search (x, m, r)
      end // end of [if]
    | _ => l (* the result is found *)
  end // end of [search]
in
  search (x, 0, x)
end // end of [isqrt]

This implementation passes typechecking, but it seems to be looping forever when tested. Instead of going into the standard routine of debugging (e.g., by inserting calls to some printing functions), let us attempt to identify the cause for infinite looping by proving the termination of the function search through the use of dependent types. Clearly, the function search is assigned the function type (int, int, int) -> int, meaning that search takes three integers as its arguments and returns an integer as its result, and there is not much else that can be gathered from a non-dependent type as such. However, the programmer may have thought that the function search should possess the following invariants (if implemented correctly):

l * l <= x and x <= r * r must hold when search(x, l, r) is called.
Assume l * l <= x < r * r for some integers x, l, r. If a recursive call search(x, l1, r1) for some integers l1 and r1 is encountered in the body of search(x, l, r), then r1-l1 < r-l must hold. This invariant implies that search is terminating.

Though the first invariant can be captured in the type system of ATS, it is somewhat involved to do so due to the need for handling nonlinear constraints. Instead, we try to assign search the following dependent function type:

{x:nat} {l,r:nat | l < r} .<r-l>. (int(x), int(l), int(r)) -> int

which captures a weaker invariant stating that l < r must hold when search(x, l, r) is called. The termination metric .<r-l>. is provided for checking that the function search is terminating. When we assign search the dependent function type, we have to modify its body as certain errors are otherwise reported during typechecking. The following code we obtain after proper modification does pass typechecking:

fun isqrt {x:nat}
  (x: int x): int = let
  fun search
    {x,l,r:nat | l < r} .<r-l>.
    (x: int x, l: int l, r: int r): int = let
    val diff = r - l
  in
    case+ 0 of
    | _ when diff > 1 => let
        val m = l + (diff / 2)
      in
        if x / m < m then search (x, l, m) else search (x, m, r)
      end // end of [if]
    | _ => l (* the result is found *)
  end // end of [search]
in
  if x > 0 then search (x, 0, x) else 0
end // end of [isqrt]

It is now rather clear that infinite looping in the previous implementation of search may happen if search(x, l, r) is called in a situaltion where r-l equals 1 as this call can potentially lead to another call to search of the same arguments. However, such a call leads to a type-error after search is assigned the aforementioned dependent function type.

By being precise and being able to enforce precision effectively, the programmer will surely notice that his or her need for run-time debugging is diminishing rapidly.

<<< Previous	Home	Next >>>
Termination-Checking for Recursive Functions	Up	Datatype Refinement