internal 设计

设计目标

immut 和 mutable 检查相同的前置条件(是否方阵、边界、形状是否兼容),并且必须以相同方式报告。internal 为每项检查只保留一份实现,使两个包不会逐渐分化,同时不把这些辅助函数暴露给下游代码。

数学背景

每个守卫都是 错误设计中某个定义域的特征检验:dom⁡(tr⁡)={A:r=c}\operatorname{dom}(\operatorname{tr}) = \{A : r = c\}、dom⁡(⋅)={(A,B):cA=rB}\operatorname{dom}(\cdot) = \{(A, B) : c_A = r_B\},等等。把检验写成一个全函数 χ:X→Unit+E\chi : X \to \mathrm{Unit} + E,即可得到部分运算的两种形式:

checked(x)=χ(x)> ⁣ ⁣> ⁣ ⁣=(_↦Ok(f(x))),unchecked(x)={f(x)χ(x)=Ok(())abortotherwise.\mathtt{checked}(x) = \chi(x) \mathbin{>\!\!>\!\!=} (\_ \mapsto \mathrm{Ok}(f(x))), \qquad \mathtt{unchecked}(x) = \begin{cases} f(x) & \chi(x) = \mathrm{Ok}(()) \\ \text{abort} & \text{otherwise.} \end{cases}

由受检守卫推导出中止守卫(ensure_x 对 ensure_x_checked 做匹配),使二者按构造在每个输入上都一致。

设计决策

内部包

MoonBit 的内部包规则将 Luna-Flow/linear-algebra/internal 的导入限制在本模块的包内。因此这些辅助函数可以自由修改,而它们的效果则在公开方法上加以规定。

HasShape 与 MatrixShape 分离

@algebra.MatrixShape 有相同的方法,但 algebra 是实验性的,具体包不应依赖它。HasShape 为守卫提供一个由 immut 和 mutable 在本地实现的约束。这种重复是让稳定的具体包独立于实验层的代价。

先行后列

ensure_index_in_bounds 先检查行,再检查列,并且各自与自身的维度比较。若改为把扁平偏移 rc′+cr c' + c 与 rc′rc' 比较,就会接受溢出到下一行的列索引。

正确性与不变量

  • ensure_x(m) 中止当且仅当 ensure_x_checked(m) 返回 Err。
  • 每个受检守卫都返回 API 页面上所列的错误类型,并带有固定的消息。
  • 所有守卫都在 O(1)O(1) 内运行,且只调用 shape。

被否决的方案

  • 在每个包中重复这些检查,这正是 0.4 系列之前边界行为出现分歧的原因。
  • 公开的辅助函数。 它们会变成下游代码所依赖的 API。

边界

internal 只检查形状和索引。它不包含算术、存储,也不包含依赖于数值的检查(奇异性、数据是否为空、收敛性)。