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} 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 //

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]

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