Rust 用伽罗瓦连接实现可组合数值转换

背景

在 Rust 中进行数值类型转换时，标准库提供了 as、From 和 Into 等操作符。然而，这些操作符每次只能处理一个转换方向，并且 as 对舍入、饱和（saturation）以及有损转换（lossy conversion）保持沉默。例如，(x as f32) as f64 != x 对于许多 x: f64 都成立，这意味着标准转换缺乏可预测的往返行为。开发者需要一种更严谨、可组合且具备数学保证的数值转换方案。

Galois connections（伽罗瓦连接）是序理论中一对单调函数，满足 f(x) ≤ y ⇔ x ≤ g(y)。这种结构天然适合偏序类型之间的静态、合法转换，例如 f64 → f32、Duration → seconds、f32 → u32 → IpAddr 等。本文介绍的 Rust crate 名为 connections，是 Haskell 库 connections 的原生移植版，将 Galois connections 作为一等公民引入 Rust，并围绕其构建了类型安全的数值转换体系。

核心内容

该库的核心是 Conn<A, B, K> 结构体，其中 K 是 Kind 标签（L 或 R），它精确地表示一个 Galois connection。一个 Conn 包含一对单调函数 f: A -> B 和 g: B -> A，其伴随角色由 Kind 标签决定：

• L‑kind：满足 f(a) ≤ b ⇔ a ≤ g(b)，对外暴露 ceil（上取整方向）和 upper（上伴随）。
• R‑kind：满足 g(b) ≤ a ⇔ b ≤ f(a)，对外暴露 floor（下取整方向）和 lower（下伴随）。

Conn 是 Copy 类型，可 const 构造，无堆分配，且 crate 声明 #![forbid(unsafe_code)]，保证安全。

库提供了两组关键能力：

1. 清晰的语义。与标准 as 不同，每个 Conn 都经过属性测试（property-tested）并满足不变式。对于每一条连接，至少有一对不等式被验证：

   • 左‑Galois：ceil(a) ≤ b iff a ≤ upper(b)
   • 右‑Galois：lower(b) ≤ a iff b ≤ floor(a)

2. 安全的可组合性。通过 compose! 宏在编译时将多个两两 Conn 折叠成一条新的 Conn<Src, Dst>。组合后的 Conn 继承了各组件连接的全部性质。例如：

use connections::conn::ConnR;
use connections::core::u032::U032I032;

// Rust 的 `as` 保留低位；这个 Conn 显式处理饱和
assert_eq!(u32::MAX as i32, -1);
assert_eq!(U032I032.floor(u32::MAX), i32::MAX);
// 根据右‑Galois 律，反向臂与 `floor` 配对
assert_eq!(U032I032.lower(-1), 0_u32);

库提供了丰富的内置类型家族，包括固定宽度整数（I/U 前缀）、Q 格式（Q 前缀）、NonZero（N 前缀）、IEEE 浮点（F 前缀）以及 iso 系列等。这些类型均通过 Kani（形式验证工具）进行了全比特宽度 SMT 证明（SMT proofs），浮点部分的 SMT 覆盖范围较窄，在文档 Testing → SMT verification 有标注。

API 设计的两条启发式原则：

1. 提升至 Conn 内部操作。Conn 是一个黑盒，高阶辅助函数（如 ceil*、floor*、round*、truncate* 等）会将参数嵌入到另一个（通常精度更宽的）域中执行计算，然后将结果舍入回原域。例如 ceil2(t, h, b1, b2) 实际执行 f(h(g(b1), g(b2)))：先用 g 将 b1、b2 嵌入宽域，在宽域中运行闭包 h，再通过 f 舍回。这用于避免在原类型中发生溢出或精度损失。

2. 在调用点进行组合。库级别导出 Conn 常量，并通过 ConnL/ConnR/ConnK API 暴露，而不是提供 get/set 函数。客户端代码需要在调用点使用 compose 系列宏静态构建多跳转换，不应手动串联中间类型。若客户端需要运行时参数，应将其保留在普通具名函数体内，该函数内部明显使用合法的 Conn 进行组合。

Kind 标签的纪律性：在 L‑kind 的 Conn 上调用 .floor() 是编译错误（该方法仅存在于 Conn<_, _, R> 上），反之亦然。两用辅助函数（如 interval、round、truncate、median）仅绑定于实现了 ConnK 的类型（ConnK 是 ConnL + ConnR 的超 trait），因此只能在双向标记（two-sided marker）上调用，不能用于单向 Conn。

当 upper 和 lower 可以由同一个内函数实现，并且满足额外的 order‑reflecting 性质（称为 Sandwich 不等式）时，库会将两个结果连接合并为一个零大小（zero-sized）的标记结构体，该结构体通过一个超 trait 提供第三组“双用”辅助函数，同时支持 ceil/floor/upper/lower 等全部方法。

关键要点

• Galois connections 作为 Rust 的一等值：Conn<A, B, K> 结构体直接表示一个 Galois connection，具有明确的伴随方向（L 或 R）。
• 类型安全的方向约束：Kind 标签 K 决定可调用的方法（ceil/upper 只在 L 上，floor/lower 只在 R 上），违反在编译时报错。
• 组合宏 compose!：在编译时静态连接多个 Conn，生成的新 Conn 自动继承所有组件的不变式。
• 丰富的内置类型家族：涵盖固定宽度整数、Q 格式、NonZero、IEEE 浮点等，均带有形式验证或属性测试。
• 无 unsafe 代码：crate 声明 #![forbid(unsafe_code)]，所有操作均基于安全 Rust。
• 最低支持 Rust 版本 1.88：MSRV 的升级会作为次要版本变化处理（connections = "0.1" 时，MSRV 升级将触发 0.2 版本，而非静默破坏补丁更新）。
• 避免手动串联：推荐在调用点使用宏组合，不要手动连接中间类型，以保留静态保证。
• 高阶辅助函数：通过嵌入宽域再舍回的方式处理溢出/精度问题，避免手动实现饱和计算。
• 双向标记（ConnK）：当连接具有 order‑reflecting 性质时，提供零大小标记结构体，暴露全部双面方法。

意义与影响

该库将数学上优雅的 Galois connections 概念系统化地应用于 Rust 的数值类型转换领域，填补了标准库在显式语义和可组合性方面的空白。与 as、From、Into 等每次只给出一个方向且语义模糊的操作不同，connections 提供了一对匹配的映射，其往返行为由简单不等式严格约束，并通过属性测试和形式验证（SMT）保障正确性。

这一设计思路对 Rust 生态的影响体现在：

• 提升数值转换的可靠性：开发者不再需要猜测舍入方向或饱和行为，每条连接都自带明确的不变式。
• **