Introduction to Programming in ATS:
PrevChapter 9. Introduction 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), arrayref(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 have no 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:int} (asz: size_t(n), elt: a): arrayref(a, n)

Given a static integer I, the type size_t(I) is a singleton type for a 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}
arrayref_get_at
  {n:int}{i:nat | i < n} (A: arrayref(a, n), i: size_t i): (a)
overload [] with arrayref_get_at
//
fun{a:t@ype}
arrayref_set_at
  {n:int}{i:nat | i < n} (A: arrayref(a, n), i: size_t i, x: a): void
overload [] with arrayref_set_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 algorithm on an ordered array: 

fun{
a:t@ype
} bsearch_arr{n:nat}
(
  A: arrayref(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: arrayref(a, n), l: int i, u: int j
) :<cloref1> int =
(
  if l <= u then let
    val m = l + half(u - l)
    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, inclusive. 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.

PrevHomeNext
Example: String ProcessingUpTermination-Checking for Recursive Functions