container 设计

设计目标

泛型代码经常需要在矩阵和向量表示之间搬运数据，或查看单个元素，而不关心其存储：稠密数组、持久化向量、视图、惰性函数、外部缓冲区。container 将这些结构能力与 algebra 的数学能力分开描述，使一个类型可以参与数据搬运而无需声称满足代数定律，反之亦然。

数学背景

容器是函数的一种表示

抽象地说，元素属于 $T$、长度为 $n$ 的向量是函数 $v : [n] \to T$，其中 $[n] = \{0, \dots, n-1\}$；$r \times c$ 矩阵是函数 $m : [r] \times [c] \to T$。具体的容器类型 V 表示这样的函数。有两种能力把表示与它所指称的函数联系起来：

• read 给出指称：对 $i < \mathtt{length}(v)$，$\llbracket v \rrbracket(i) = \mathtt{get}(v, i)$；
• build 方向相反：$\mathtt{tabulate}(n, f)$ 是 $f$ 限制在 $[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 无法区分，尽管在内存中可能是不同的值。

泛型算法即复合

有了这两个映射，泛型算法就是指称上函数的复合：

$$\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}$$

直接可得两条定律，也正是测试所检查的：

$$\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 是后复合，而后复合保持恒等与复合。

编辑即 lens

持久化编辑 $\mathtt{set}(v, i, x)$ 与读取 $\mathtt{get}(v, i)$ 构成位置 $i$ 上的一个 lens，正确的实现对每个合法索引都满足三条 lens 定律：

$$\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}$$

并且由于是持久化的，它不改变 $v$ 本身。可变编辑满足同样的等式，只是用“调用后 $v$ 的状态”代替返回值。

设计决策

用操作字典代替 trait

问题。 “从容器 V 中读取类型为 T 的元素”这类能力关联着两个类型。MoonBit 的 trait 只有一个 Self 参数，没有关联类型。

选项。 (a) 在 V 上定义一个固定元素类型的 trait，例如借助泛型方法。(b) 为每种元素类型在 V 上定义一个 trait。(c) 以两个类型为参数的函数记录。

决定。 (c)：VectorReadOps[V, T] 及其同类都是普通的闭包结构体，用 new 构造并显式传递。

理由。 记录可以直接表达这种双参数关系。它还允许一个容器类型发布多个字典，例如一个受检读取和一个截断读取，或为多态外部句柄的不同元素类型分别提供字典，而 trait 实例（每个类型唯一）做不到这一点。代价是需要显式传递；算法把字典作为参数接收。

读取与构造相互分离

视图可以读取但不能构造；只写的接收端可以构造但不能读取；外部句柄可能只允许读取。若把读取和构造合并为一种能力，所有这类类型要么得伪造缺失的一半，要么只能被排除在外。算法会准确说明各端需要哪一半：源端读取，目标端构造。

两种编辑模型

持久化编辑返回新值；可变编辑修改参数并返回 Unit。它们是不同的契约：针对持久化形式编写的泛型代码可能保留旧值并期望它不变，而可变实现会违反这一点。因此它们是不同的记录，类型提供与其所有权模型相匹配的那一种。二者都不意味着调整尺寸、插入或删除。

先全部读取，再构造

算法在调用 tabulate 之前，会把整个源读入一个临时数组。这需要 $O(n)$ 内存，但使失败具有原子性：只要有任何读取失败，算法就在目标创建之前返回该错误，因此调用者永远不会看到构造了一半的容器。它还保证用户的映射函数对每个元素按行主序恰好调用一次，这在函数有副作用或开销较大时很重要。

处处受检

每个字典函数都返回 Result。泛型算法无法知道任意容器的边界行为，因此契约要求每个实现以值的形式报告非法索引和形状，而不是中止。仓库中的适配器在访问存储之前先做校验。

正确性与不变量

• 形状保持。 map 和 convert 精确保持 $(r, c)$，包括 $0 \times n$ 和 $n \times 0$；transpose 产生 $(c, r)$。算法从不在空维度上调用 get。
• 转置的索引映射。 源按行主序缓冲，因此源元素 $(j, i)$ 位于偏移 $j c + i$ 处。目标在 $(i, j)$ 处的初始化函数读取该偏移，恰好得到 $\llbracket m \rrbracket(j, i)$。
• 错误优先级。 报告的形状为负时，在任何读取之前给出 NegativeDimension；否则返回第一个失败的读取（按行主序）；否则原样返回 tabulate 的结果。
• 复杂度。 对 $n = r c$：$n$ 次读取，一次 tabulate（对初始化函数求值 $n$ 次），以及 $n$ 次映射函数调用。

被否决的方案

• 通用的 insert、delete、create 或 remove。 删除稀疏存储项、将其置零、删除一行以及调整矩阵尺寸是不同的操作；用一个名字涵盖所有这些操作将没有清晰的定律。
• 在读取字典中加入优化的内核操作（行交换、带缩放的行加法）。强制要求它们会排除简单的容器。将来可以在 read 和 build 之外增加一个类似 MatrixKernelOps 的字典，作为可选能力。
• 不使用缓冲区的流式算法。 它们可以节省内存，但对于增量构造的目标会失去失败原子性。

边界

container 不定义存储、算术或代数定律。它本身不提供稀疏或惰性容器，不支持调整尺寸或结构性编辑，也不提供高性能内核；这些算法是通过闭包进行的 $O(n)$ 复制，用于互操作，而不是用于内层循环。针对本仓库类型的具体字典位于 container/adapters。