container の設計

設計目標

汎用コードでは、ストレージの種類(密な配列、永続ベクトル、ビュー、遅延関数、外部バッファ)を気にせずに、行列やベクトルの表現の間でデータを移したり、個々の要素を参照したりする必要がよくあります。container はこうした構造的な能力を algebra の数学的な能力とは別に記述します。これにより、型は代数法則を主張せずにデータ移動に参加でき、その逆も可能です。

数学的背景

コンテナは関数の表現である

抽象的には、要素が TT に属する長さ nn のベクトルは関数 v:[n]→Tv : [n] \to T([n]={0,…,n−1}[n] = \{0, \dots, n-1\})であり、r×cr \times c 行列は関数 m:[r]×[c]→Tm : [r] \times [c] \to T です。具体的なコンテナ型 V はこうした関数を 表現 します。2 つの能力が、表現とそれが表す関数とを結び付けます。

  • 読み取り は表示を与えます: i<length(v)i < \mathtt{length}(v) について ⟦v⟧(i)=get(v,i)\llbracket v \rrbracket(i) = \mathtt{get}(v, i)。
  • 構築 は逆向きです: tabulate(n,f)\mathtt{tabulate}(n, f) は、ff を [n][n] に制限したものの何らかの表現です。

両者を結び付ける基本法則は、構築してから読み取ると元の関数に戻る、というものです。

length(tabulate(n,f))=n,get(tabulate(n,f),i)=Ok (f(i))(0≤i<n).\mathtt{length}(\mathtt{tabulate}(n, f)) = n, \qquad \mathtt{get}(\mathtt{tabulate}(n, f), i) = \mathrm{Ok}\,(f(i)) \quad (0 \le i < n).

読み取ってから構築すると、元のコンテナと 観測的に 等しいコンテナが得られます。get を通じては区別できませんが、メモリ上では別の値かもしれません。

合成としての汎用アルゴリズム

この 2 つの写像を使うと、汎用アルゴリズムは表示上の関数の合成になります。

⟦vector_map(v,g)⟧=g∘⟦v⟧,⟦matrix_transpose(m)⟧(i,j)=⟦m⟧(j,i).\begin{aligned} \llbracket \mathtt{vector\_map}(v, g) \rrbracket &= g \circ \llbracket v \rrbracket, \\ \llbracket \mathtt{matrix\_transpose}(m) \rrbracket(i, j) &= \llbracket m \rrbracket(j, i). \end{aligned}

ここから 2 つの法則が直接導かれ、テストで検査するのはこれらです。

map(v,id)≃convert(v),map(map(v,g),h)≃map(v,h∘g),transpose(transpose(m))≃convert(m),shape⁡(transpose(m))=(c,r),\begin{aligned} \mathtt{map}(v, \mathrm{id}) &\simeq \mathtt{convert}(v), & \mathtt{map}(\mathtt{map}(v, g), h) &\simeq \mathtt{map}(v, h \circ g), \\ \mathtt{transpose}(\mathtt{transpose}(m)) &\simeq \mathtt{convert}(m), & \operatorname{shape}(\mathtt{transpose}(m)) &= (c, r), \end{aligned}

ここで ≃\simeq は観測的な等しさです。最初の組は関手の法則です。表示の上では map は後合成であり、後合成は恒等と合成を保ちます。

レンズとしての編集

永続的な編集 set(v,i,x)\mathtt{set}(v, i, x) と読み取り get(v,i)\mathtt{get}(v, i) は位置 ii 上のレンズをなし、正しい実装はすべての有効なインデックスについて 3 つのレンズ法則を満たします。

get(set(v,i,x),i)=x(you get what you set)get(set(v,i,x),j)=get(v,j),j≠i(nothing else changes)set(v,i,get(v,i))≃v(setting what is there changes nothing)\begin{aligned} \mathtt{get}(\mathtt{set}(v, i, x), i) &= x && \text{(you get what you set)} \\ \mathtt{get}(\mathtt{set}(v, i, x), j) &= \mathtt{get}(v, j), \quad j \ne i && \text{(nothing else changes)} \\ \mathtt{set}(v, i, \mathtt{get}(v, i)) &\simeq v && \text{(setting what is there changes nothing)} \end{aligned}

さらに永続的なので、vv 自体は変更しません。可変な編集は、返り値の代わりに「呼び出し後の vv の状態」を使って同じ等式を満たします。

設計上の判断

trait ではなく操作辞書

問題。 「コンテナ V から型 T の要素を読み取る」といった能力は 2 つの型を関係づけます。MoonBit の trait は Self パラメータを 1 つしか持たず、関連型もありません。

選択肢。 (a) 要素型を(たとえば総称メソッドで)固定する V 上の trait。(b) 要素型ごとの V 上の trait。(c) 両方の型でパラメータ化された関数のレコード。

決定。 (c)。VectorReadOps[V, T] とその仲間はクロージャからなる素朴な構造体で、new で構築し、明示的に渡します。

理由。 レコードは 2 パラメータの関係を直接表現できます。また、1 つのコンテナ型が複数の辞書を公開することもできます。たとえば検査付きの読み取りと値を範囲内に丸める読み取り、あるいは多相的な外部ハンドルの要素型ごとの辞書などで、型ごとに一意な trait インスタンスではこれはできません。代償は明示的に渡す必要があることで、アルゴリズムは辞書を引数として受け取ります。

読み取りと構築は別々

ビューは読み取れても構築できません。書き込み専用のシンクは構築できても読み取れません。外部ハンドルは読み取りしか許さないかもしれません。読み取りと構築を 1 つの能力にまとめると、こうした型はすべて、欠けている半分を偽装するか、参加をあきらめるかのどちらかを強いられます。アルゴリズムは各側で必要な半分を正確に述べます。ソースには読み取り、ターゲットには構築です。

2 つの編集モデル

永続的な編集は新しい値を返し、可変な編集は引数を変更して Unit を返します。これらは異なる契約です。永続形式向けに書かれた汎用コードは古い値を保持し、それが変わらないことを期待するかもしれませんが、可変な実装はそれを破ってしまいます。そのため両者は別々のレコードであり、型は自身の所有モデルに合うほうを提供します。どちらもサイズ変更、挿入、削除を意味しません。

すべて読み取ってから構築する

アルゴリズムは tabulate を呼ぶ前に、ソース全体を一時配列に読み込みます。これには O(n)O(n) のメモリがかかりますが、失敗が不可分になります。どこかの読み取りが失敗すれば、アルゴリズムはターゲットが存在する前にそのエラーを返すので、呼び出し側が構築途中のコンテナを目にすることはありません。また、ユーザーの写像関数を要素ごとにちょうど 1 回、行優先順に呼び出します。これは関数が副作用を持つ場合や高コストな場合に重要です。

どこでも検査付き

辞書の関数はすべて Result を返します。汎用アルゴリズムは任意のコンテナの範囲外の扱いを知りえないため、契約は各実装に対し、不正なインデックスや形状を中断ではなく値として報告することを求めます。リポジトリのアダプタはストレージに触れる前に検証します。

正しさと不変条件

  • 形状の保存。 map と convert は 0×n0 \times n と n×0n \times 0 を含めて (r,c)(r, c) を正確に保存します。transpose は (c,r)(c, r) を生成します。アルゴリズムが空の次元に対して get を呼ぶことはありません。
  • 転置のインデックス対応。 ソースは行優先順にバッファリングされるため、ソースの要素 (j,i)(j, i) はオフセット jc+ij c + i にあります。(i,j)(i, j) におけるターゲットの初期化関数はそのオフセットを読み、それはちょうど ⟦m⟧(j,i)\llbracket m \rrbracket(j, i) です。
  • エラーの優先順位。 報告された形状が負であれば、読み取りの前に NegativeDimension を返します。そうでなければ(行優先順で)最初に失敗した読み取りを返し、それもなければ tabulate の結果をそのまま返します。
  • 計算量。 n=rcn = r c として、nn 回の読み取り、初期化関数を nn 回評価する tabulate 1 回、写像関数の nn 回の呼び出しです。

却下した代替案

  • 汎用の insert、delete、create、remove。 疎な要素の削除、ゼロの代入、行の削除、行列のサイズ変更は別々の操作であり、それらすべてに 1 つの名前を付けても明確な法則は得られません。
  • 読み取り辞書への最適化されたカーネル操作(行の交換、スカラー倍した行の加算)。それらを要求すると単純なコンテナが排除されます。将来、MatrixKernelOps のような辞書を、読み取りと構築に並ぶ任意の能力として追加するかもしれません。
  • バッファを使わないストリーミングアルゴリズム。 メモリは節約できますが、段階的に構築されるターゲットに対して失敗の不可分性を失います。

境界

container はストレージ、算術、代数法則を定義しません。疎や遅延のコンテナ自体、サイズ変更や構造的な編集、高性能なカーネルも提供しません。アルゴリズムはクロージャを介した O(n)O(n) のコピーであり、内側のループではなく相互変換のためのものです。このリポジトリの型に対する具体的な辞書は container/adapters にあります。