種 t@ype の型 T と静的な整数 I (例: 種 int の静的な項)が与えられた時、arrayref(T, I) はボックス化型で、保管されている要素が型 T であるサイズ I の配列です。 このような配列はサイズに関する情報を付随して持っていないことに注意してください。 次のインターフェイスは配列を生成するための関数テンプレート array_make_elt です。 このテンプレートが生成する配列もまたサイズ情報を持っていません:
静的な整数 I が与えられた時、型 size_t(I) はシングルトン型で、I と等しい整数を表わすC言語の型 size_t の値を表わします。 配列要素の読み書きのための関数テンプレートは次のようなインターフェイスを持ちます:// 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 //
依存型を使った実際のプログラミングの説得力のある例として、次のコードでは整列された配列に対する標準の二分探索アルゴリズムを実装しています:
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]
この章で紹介したコードと追加のテストコードは オンライン から入手できます。