Chapter 16. 永続化配列

サイズ n の永続化配列は、単に1行の中のヒープに確保された n 個のセル (もしくは参照) です。 この配列に対して確保されたメモリは手動で解放できないという意味で永続的です。 その代わりに、ガベージコレクション (GC) を通じて安全に回収されます。

viewtype VT が与えられたとき、viewtype VT の値 N を含む永続化配列の型は arrayref(VT, N) です。 ATS での配列はC言語のものと同じで、それらにはサイズ情報が付属しないことに注意してください。 永続化配列に関する様々な関数インターフェイスが SATS ファイル prelude/SATS/arrayref.sats に見つけることができます。 このファイルは atsopt によって自動的に読み込まれます。

配列を生成する様々な関数があります。 例えば、次の2つは一般的に使用されます:

fun{a:t@ype} arrayref_make_elt {n:nat} (asz: size_t n, elt: a):<!wrt> arrayref (a, n) // end of [arrayref_make_elt] fun{a:t@ype} arrayref_make_listlen {n:int} (xs: list (a, n), n: int n):<!wrt> arrayref (a, n) // end of [arrayref_make_listlen]

サイズと要素に適用されると、arrayref_make_elt は与えられた要素でそれぞれのセルを初期化した与えられたサイズの配列を返します。 リストとそのリストの長さに適用されると、arrayref_make_listlen は与えられた長さに等しいサイズの配列を返します。 このとき配列のそれぞれのセルは与えられたリストの対応する要素で初期化されます。

配列を読み書きするために、関数テンプレート arrayref_get_atarrayref_set_at を使うことができます。 それぞれ次のようなインターフェイスが割り当てられています:

fun{a:t@ype} arrayref_get_at {n:int} (A: arrayref (a, n), i: sizeLt (n)):<!ref> a fun{a:t@ype} arrayref_set_at {n:int} (A: arrayref (a, n), i: sizeLt (n), x: a):<!ref> void

配列 A, インデックス i, 値 v が与えられたとき、arrayref_get_at(A, i)arrayref_set_at(A, i, v) はそれぞれ A[i]A[i] := v のように書くことができます。

例として、次の関数テンプレートは与えられた配列の内容を逆順にします:

fun{a:t@ype} arrayref_reverse{n:nat} ( A: arrayref (a, n), n: size_t (n) ) : void = let // fun loop {i: nat | i <= n} .<n-i>. ( A: arrayref (a, n), n: size_t n, i: size_t i ) : void = let val n2 = half (n) in if i < n2 then let val tmp = A[i] val ni = pred(n)-i in A[i] := A[ni]; A[ni] := tmp; loop (A, n, succ(i)) end else () // end of [if] end // end of [loop] // in loop (A, n, (i2sz)0) end // end of [arrayref_reverse]

もし判定 i < n2i <= n2 に変更すると、型エラーが発生します。 なぜでしょうか? その理由は、ni が両方ともゼロに等しい場合に、A[n-1-i] が配列の添字指定の範囲外になるからです。 サイズがゼロの配列に遭遇することなく、もし早期に発見していなかったら、このようなバグはゾッとするほど奥深くに埋め込まれてしまうかもしれません!

懸命な読者は、種 t@ype がテンプレートパラメータ a に割り当てられていることに、既に気がついているかもしれません。 別の言い方をすると、arrayref_reverse の上記の実装は、与えられた配列内の値が線形型であるような場合を扱うことができません。 種 t@ype を選択している理由は、arrayref_get_atarrayref_set_at の両方が非線形型の値を含む配列にのみ適用できるからです。 次の実装では、テンプレートパラメータには種 vt@ype が与えられているので、線形型の値を含む配列を扱うことができます:

fun{a:vt@ype} arrayref_reverse{n:nat} ( A: arrayref(a, n), n: size_t(n) ) : void = let // fun loop {i: nat | i <= n} .<n-i>. ( A: arrayref(a, n), n: size_t n, i: size_t i ) : void = let val n2 = half (n) in if i < n2 then let val () = arrayref_interchange(A, i, pred(n)-i) in loop(A, n, succ(i)) end else () // end of [if] end // end of [loop] // in loop(A, n, i2sz(0)) end // end of [arrayref_reverse]

関数テンプレート arrayref_interchange のインターフェイスは以下のようになります:

fun{a:vt@ype} arrayref_interchange{n:int} (A: arrayref (a, n), i: sizeLt n, j: sizeLt n):<!ref> void // end of [arrayref_interchange]

arrayref_get_atarrayref_set_at の観点では、arrayref_interchange は (型安全でないコードを使わずに) 実装できないことに注意してください。

配列を左から右に、もしくは右から左に走査するのに役に立つ様々な関数があります。 また、次の2つの関数は配列を左から右に走査するために使うことができます:

// fun{a:t0p} arrayref_head{n:pos} (A: arrayref (a, n)): (a) // A[0] fun{a:t0p} arrayref_tail{n:pos} (A: arrayref (a, n)): arrayref (a, n-1) // overload .head with arrayref_head overload .tail with arrayref_tail //

例として、配列に対する左 fold 関数は次のように実装できます:

fun{a,b:t@ype} arrayref_foldleft{n:int} ( f: (a, b) -> a, x: a, A: arrayref (b, n), n: size_t(n) ) : a = ( if n > 0 then arrayref_foldleft<a,b> (f, f (x, A.head), A.tail, pred(n)) else x // end of [if] ) (* end of [arrayref_foldleft] *)

期待される通り、A.headA.tail はそれぞれ A[0]ptr_succ<T>(p0) に変換されます。 このとき T は A に保管されている要素の型で、p0 は A の開始アドレスです。

この章で紹介したコードの全体は オンライン から入手できます。