hom 设计

设计目标

在 MoonBit 现有类型系统里表达”保持结构的映射”，并把无法由类型系统证明的同态律交给开发者，同时让这些义务可审计、可测试。

约束

MoonBit 的 trait 只有 Self 一个参数，没有多参 trait 和关联类型，因此 A -> B 的同态不能写成 trait。
从 ℕ、ℤ 出发的同态是唯一的（始对象），所以 FromNat 与 FromInteger 可以作为目标侧 trait 存在。其他同态一般不唯一，必须作为值存在。

核心设计决策

LCF 风格的证书：Hom[S, A, B] 字段私有，只能由本包构造。
唯一的公开信任入口是 Hom::postulate。内核规则使用包内私有的 trust，所以搜索 postulate 得到的正好是全部用户层义务。（assume 是 MoonBit 的保留字，因此不用这个名字。）Section::postulate 是截面的信任入口，典范的 Hom::from_integer 与 Section::of_integral 是另外的叶子：它们的义务落在 trait 实例上。
从商提升回覆盖代数的映射是 Section 而不是 Hom。它把投影作为 Hom 携带，只承诺 proj(lift(q)) == q；在代表元上与运算一致这一点由该定律推出。把两者分开，可以防止 Int -> BigInt 这类代表元提升被当作同态来复合。
签名以幽灵类型 S 出现在类型上，代数以字典 Algebra[S, A] 的形式作为值传递，两者分离：证书说明”保持什么”，字典用于检查。
签名之间的包含关系用只有本包能构造的 Reduct[S, T] 见证表示。
保持强度由检查时的关系 rel 决定，严格、lax 与近似同态共用一套 API。

截面

hom 教程在不涉及这些数学的情况下使用 Section。

定义

设 π : A -> Q 是满同态，例如约化 BigInt -> Int。截面是满足对每个 q 都有 π(s(q)) = q 的映射 s : Q -> A：它从每个类 π⁻¹(q) 中选出一个元素。由第一同构定理，Q 就是商 A / ker π，所以截面就是为商代数选取代表元。

截面保持什么

对每个运算 ω 与参数 x：

s(ω(x)) 与 ω(s(x)) 模 ker π 同余。对两者作用 π：由截面律 π(s(ω(x))) = ω(x)；由于 π 是同态，π(ω(s(x))) = ω(π(s(x))) = ω(x)。
s(ω(x)) = ω(s(x)) 当且仅当 ω(s(x)) 位于 s 的像中。若 ω(s(x)) = s(y)，则由同样的计算 y = π(s(y)) = π(ω(s(x))) = ω(x)，所以 ω(s(x)) = s(ω(x))。反过来，s(ω(x)) 总在像中。

同样两步的公式形式：对 $n$ 元运算 $\omega$ 与 $x = (x_1, \dots, x_n)$ ，记 $s(x) = (s(x_1), \dots, s(x_n))$ ：

\begin{aligned} \pi\bigl(s(\omega_Q(x))\bigr) &= \omega_Q(x) && \text{section law} \\ \pi\bigl(\omega_A(s(x))\bigr) &= \omega_Q(\pi(s(x))) = \omega_Q(x) && \pi \text{ is a homomorphism} \end{aligned}

因此只要 $A$ 有减法，就有 $s(\omega_Q(x)) - \omega_A(s(x)) \in \ker \pi$ 。若对某个 $y$ 有 $\omega_A(s(x)) = s(y)$ ，两边作用 $\pi$ 得 $y = \omega_Q(x)$ ，从而 $\omega_A(s(x)) = s(\omega_Q(x))$ 。

因此 Section::check 只检验截面律；check_ops 检验 π 在提升后的参数上是同态，第 2 点随之成立。对 Int 而言，s 的像是 [-2^31, 2^31)，“结果在像中”就是“结果没有回绕”。

进位

对 Int 的加法，第 1 点中的差为 s(a) + s(b) - s(a + b) = c(a, b)·2^32，其中 c(a, b) ∈ {-1, 0, 1}，即进位。把 s(a) + s(b) + s(e) 按两种方式展开得到

c(a, b) + c(a + b, e) = c(b, e) + c(a, b + e)

这个恒等式来自结合律。记 $m = 2^{32}$ 且 $s(a) + s(b) = s(a + b) + c(a, b)\,m$ ，然后把三个提升之和按两种方式结合：

\begin{aligned} (s(a) + s(b)) + s(e) &= s(a + b) + s(e) + c(a, b)\,m \\ &= s(a + b + e) + \bigl(c(a + b, e) + c(a, b)\bigr)\,m, \\ s(a) + (s(b) + s(e)) &= s(a) + s(b + e) + c(b, e)\,m \\ &= s(a + b + e) + \bigl(c(a, b + e) + c(b, e)\bigr)\,m . \end{aligned}

两边在 ℤ 中相等，所以 $m$ 的系数相同。 $c$ 的界来自代表元的范围： $s(a) + s(b) \in [-2^{32}, 2^{32} - 2]$ 且 $s(a + b) \in [-2^{31}, 2^{31})$ ，所以 $c(a, b)\,m$ 严格介于 $-3 \cdot 2^{31}$ 与 $3 \cdot 2^{31}$ 之间，从而 $c(a, b) \in \{-1, 0, 1\}$ 。

所以 c 是一个 2-上闭链，把 ℤ 描述为 ℤ/2^32 被 2^32ℤ 的扩张。该扩张不分裂，因为 ℤ 没有有限阶元素，所以任何代表元选择都不能让 s 成为同态。直接地说：一个可加截面 $\sigma : \mathbb{Z}/m \to \mathbb{Z}$ 会给出 $m\,\sigma(1) = \sigma(m \cdot 1) = \sigma(0) = 0$ ，于是 $\sigma(1) = 0$ ，与 $\pi(\sigma(1)) = 1$ 矛盾。对乘法而言，偏差是乘积的高位字。

范式

n = s ∘ π : A -> A 是一个范式：n(n(a)) = n(a)，a 与 n(a) 同余，且 a、b 同余当且仅当 n(a) = n(b)。商上的运算在代表元上按 s(ω_Q(x)) = n(ω_A(s(x))) 计算：先在 A 中计算，再化为范式。回绕的 Int 运算正是 A = ℤ 时的这种计算。由于 Section::normalize 由 s 与 π 构造，它不可能给两个同余的值不同的范式。

为什么 `Section` 不是 `Hom`

截面是单射，并且在它的像上与运算一致，所以很容易被误认为同态并按同态来复合。把它放在单独的证书里，就能在类型上看出区别：Section 把 π 作为 Hom 携带，只承诺 π(s(q)) = q。

定律并不规定选哪些代表元。[0, 2^32) 与 [-2^31, 2^31) 都给出 BigInt -> Int 的截面，只有后者保持 Int 的有符号序。这类性质需要单独检验。

被否决的方案

由类型实现的同态 trait Hom[A, B]：它需要两个类型参数，而 MoonBit 的 trait 没有；而且它对每对类型只允许一个同态，而一对类型通常有多个同态，例如复数上的恒等映射与共轭。
不带证书的普通函数 (A) -> B：无法把已检查的同态与任意转换区分开，复合也不会记录义务来自何处。
把 Int -> BigInt 这样的代表元提升当作同态：上文的上闭链论证表明它们不是，所以它们有自己的证书 Section。
在类型中记录检查关系（严格、宽松、容差）：这会让推理规则按强度成倍增加。改为在检查时选择关系，其代价在下文的边界中说明。

边界

只覆盖单类别签名。模这类多类别结构（标量加向量）不在本子系统内。
没有 HKT，因此函子提升（多项式、矩阵等）由各自的包提供，不在本包内泛化。
同态律不被证明，只被测试。证书保证的是”来源可追溯”，不是”定律成立”。
then 的可靠性依赖于每个载体上只有一个 S-代数。内置标签由 trait 的一致性保证这一点；Algebra::make 构造的字典只能靠约定。
证书不记录 check_by 所用的关系，因此松弛映射与近似映射会被当作严格同态来复合。
定宽整数是 ℤ/2^k，不是 ℤ 或 ℕ。从它们到 ℤ 的映射是截面，所以只在运算不回绕时与运算一致。
截面律不规定选哪些代表元，因此保序之类的性质需要单独检验。