Introduction to Programming in ATS:
<<< PreviousIntroduction to Dependent TypesNext >>>

Example: Binary Search on Arrays

Given a type T (of the sort t@ype) and a static integer I (i.e., a static term of the sort int), array(T, I) is a boxed type for arrays of size I in which each stored element is of the type T. Note that such arrays are without size information attached to them. The following interface is for a function template array_make_elt that can be called to create an array (with no size information attached to it): 

fun{a:t@ype}
array_make_elt {n:nat} (asz: size_t n, elt: a): array (a, n)

Given a static integer I, the type size_t(I) is a singleton type for the value of the type size_t in C that represents the integer equal to I. The function templates for reading from and writing to an array cell have the following interfaces: 

fun{a:t@ype}
array_get_elt_at {n:int}
  {i:nat | i < n} (A: array (a, n), i: size_t i): a
overload [] with array_get_elt_at

fun{a:t@ype}
array_set_elt_at {n:int}
  {i:nat | i < n} (A: array (a, n), i: size_t i, x: a): void
overload [] with array_set_elt_at

Note that these two function templates do not incur any run-time array-bounds checking: The types assigned to them guarantee that each index used for array subscripting is always legal, that is, within the bounds of the array being subscripted.

As a convincing example of practical programming with dependent types, the following code implements the standard binary search algorithms on an ordered array: 

fun{a:t@ype}
bsearch_arr {n:nat} (
  A: array (a, n), n: int n, x0: a, cmp: (a, a) -> int
) : int = let
  fun loop
    {i,j:int |
     0 <= i; i <= j+1; j+1 <= n} (
    A: array (a, n), l: int i, u: int j
  ) :<cloref1> int =
    if l <= u then let
      val m = l + (u - l) / 2
      val x = A[m]
      val sgn = cmp (x0, x)
    in
      if sgn >= 0 then loop (A, m+1, u) else loop (A, l, m-1)
    end else u // end of [if]
  // end of [loop]
in
  loop (A, 0, n-1)
end // end of [bsearch_arr]

The function loop defined in the body of bsearch_arr searches the segment of the array A between the indices l and u, inclusively. Clearly, the type assigned to loop indicates that the integer values i and j of the arguments l and u must satisfy the precondition consisting of the constraints 0 <= i, i <= j+1, and j+1 <= n, where n is the size of the array being searched. The progress we have made by introducing dependent types into ATS should be evident in this example: We can not only specify much more precisely than before but also enforce effectively the enhanced precision in specification.

Please find on-line the code employed for illustration in this section plus some additional code for testing.

<<< PreviousHomeNext >>>
Example: String ProcessingUpTermination-Checking for Recursive Functions