显示 HN：Rust 中可组合数值转换的伽罗瓦连接

阅读此处或 docs.rs 上的文档。概述伽罗瓦连接作为一流的 Rust 值。使用它们在数字类型之间合法地进行转换，并组成转换阶梯，其往返行为由简单的不等式决定，而不是由偶然决定。从 Conn 派生的每个操作（舍入、饱和度、中值……）都带有经过属性测试的不变量。生成的固定宽度整数、Q 格式、NonZero 和 iso 系列还具有用于全位宽 SMT 证明的 Kani 线束；浮动 SMT 覆盖范围较窄，并在测试 → SMT 验证下进行调出。 MSRV：铁锈 1.88。 MSRV 的升级将被视为次要版本更改 - 引脚连接 =“0.1”，并且 MSRV 升级将作为 0.2 版本出现，而不是补丁更新中的静默中断。该板条箱是 Haskell 库连接的 Rust 原生端口。为什么这个板条箱伽罗瓦连接是部分有序类型之间静态、合法转换的正确形状（例如 f64 → f32 、 Duration → 秒 、 f32 → u32 → IpAddr 等），其中链中的每个链接都可以在编译时指定。标准转换运算符 as 、 From 和 Into 一次只为您提供一个方向 - 特别是 as 在舍入、饱和和有损转换方面保持沉默。这个包为您提供了标准工具无法提供的两个具体功能： 清晰的语义。 (x as f32) as f64 != x 对于许多 x: f64 。对于 Conn ，对于此板条箱中的每个连接，至少对以下一对不等式进行属性测试： 左伽罗瓦： ceil(a) ≤ b iff a ≤ upper(b) 右伽罗瓦： lower(b) ≤ a iff b ≤ Floor(a) Conn 是 Copy 、 const 可构造的、无堆的，并且板条箱是 #![forbid(unsafe_code)] 。可安全组合。撰写！宏在编译时将一串成对的 Co​​nns 折叠成一个新的 Conn。组合的 Conn 遵循与其构造的组件连接相同的属性。快速开始使用连接 :: conn :: ConnR ;使用连接 :: core :: u032 :: U032I032 ； // Rust 的 `as` 保留低位；这个康恩使饱和变得明确。断言_eq！ ( u32 :: MAX 作为 i32 , - 1 ) ;断言_eq！ (U032I032.floor(u32::MAX), i32::MAX); // 根据右伽罗瓦定律，反向臂与“floor”配对。断言_eq！ (U032I032.下(-1),0_u32);请参阅 EXAMPLES.md，了解各个领域的十个有效示例的序列。什么是连接？先序 A 和 B 之间的伽罗瓦连接是一对单调映射 f: A → B 和 g: B → A ，使得 f(x) ≤ y ⇔ x ≤ g(y) 。我们说 f 是连接的左伴随或下伴随，g 是连接的右伴随或上伴随。这是两个三元素集之间的简单连接：（图片由 7 Sketches in Compositionality 提供）。每行是一个 (a, b) 对；箭头显示 f（A → B，底部图例）和 g（B → A，顶部图例）的作用。单独的箭头标记单向地图（ f(1) = 1 , g(2) = 2 ）； ↔ 标记两个伴随词一致的匹配对（ f(3) = 3 , g(3) = 3 ）；相邻的 ↰ ↳ 字形描绘了透镜 f(2) ↔ g(1) — 第 2 行和第 1 行之间的两条不相交的曲线，即伴随性的几何特征。如何使用连接 伽罗瓦连接构成： (f₁ ⊣ g₁) ∘ (f2 ⊣ g2) 又是一个附属词，并且构成！静态地构建该组合，并作为一个整体进行法律检查。当您应用析构函数（例如 upper 、 lower 、 ceil 、 Floor 等）时，您就离开了 Conn 代数并产生了一个无法再组合的具体值。因此，早期的解构抛弃了整个链本来可以享受的静态保证。因此，如果您遵循两个启发式方法，您将获得最大的收益。通过 Conn 进行提升。Conn 是一个小黑匣子：较高数量的助手（例如 ceil* 、 Floor* 、 round* 、 truncate* 等）接受您的参数，在 Conn 的其他（通常是更高保真度）域中对它们执行某些操作，并将结果返回到您的原始域中。 ceil2(t, h, b1, b2) 是 f(h(g(b1), g(b2))) ：通过 g 将 b1 / b2 嵌入到更广泛的域中，在那里运行闭包 h ，通过 f 绕回。使用它来进行域算术，这会在您自己的类型中溢出或丢失精度 - 在更广泛的域中执行此操作并四舍五入。永远不要手卷饱和数学。在现场撰写。在库级别导出 Conns 并使用 ConnL / ConnR / ConnK API 而不是 get/set 函数。当客户端代码需要多跳转换时，请在调用站点使用 compose 宏（ compose 、 compose_l 、 compose_r 、 compose_k ）静态构建精确的 Conn。不要用手穿线中间体。如果客户端代码采用运行时参数，那么最好将助手保留为普通的命名函数，其主体明显与其所依赖的合法 Conns 组成。将运行时参数和转换策略选择推送到静态 Conn 调用站点附近的规则意味着策略和静态转换在同一主体中都是可见的。结果是代码明显正确、易于测试并且可扩展到未来的用例。图书馆 L & R 类型连接