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):
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 //
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.