サイズ情報が付属した永続化配列を サイズを伴う配列 (array-with-size) と呼びます。 観型 VT が与えられたとき、観型 VT の N 個の値を含むサイズを伴う配列の型は arrszref(VT, N) です。 本質的に、この型の値は型 arrayref(VT, N) と size_t(N) の2つを構成要素とするボッスク化ペアです。 サイズを伴う永続化配列に対する様々な関数のインターフェイスを prelude/SATS/arrayref.sats に見つけることができます。
次の関数 arrszref_make_arrpsz と arrszref_make_arrayref を呼び出すことで、サイズを伴う配列を生成することができます:
fun{} arrszref_make_arrpsz {a:vt0p}{n:int} (arrpsz (INV(a), n)): arrszref(a) fun{} arrszref_make_arrayref {a:vt0p}{n:int} (arrayref (a, n), size_t(n)): arrszref(a) // end of [arrszref_make_arrayref]
サイズを伴う配列を読み書きするために、関数テンプレート arrszref_get_at と arrszref_set_at をそれぞれ使うことができます。 これらの関数テンプレートには次のインターフェイスが割り当てられています:
fun{a:t@ype} arrszref_get_at (A: arrszref (a), i: size_t): (a) fun{a:t@ype} arrszref_set_at (A: arrszref (a), i: size_t, x: a): void
簡単な例として、次のコードは与えられたサイズを伴う配列の中身を逆順にする関数を実装しています:
fun{a:t@ype} arrszref_reverse ( A: arrszref (a) ) : void = let // val n = A.size val n2 = half (n) // fun loop (i: size_t): void = let in if i < n2 then let val tmp = A[i] val ni = pred(n)-i in A[i] := A[ni]; A[ni] := tmp; loop (succ(i)) end else () // end of [if] end // end of [loop] // in loop (i2sz(0)) end // end of [arrszref_reverse]
配列を用いたプログラミングが要求される実装のプロトタイピングに、サイズを伴う配列はうってつけです。 また、依存型にまだ精通していないプログラマにとって、配列よりもサイズを伴う配列の方が明らかに簡単に使えるでしょう。 ATS におけるプログラミングでは、私はサイズを伴う配列からはじめて、それからその恩恵が明確になってから配列で置き換えることがしばしばあります。
この章で紹介したコード全体は オンライン から入手できます。