`bin_float_checked` 设计

设计目标

bin_float_checked 让二进制浮点计算可以写成一条操作链：每一次失败都是显式的，且不会丢失，同时无需在每一步之后解包。BinFloatResult 使 Result[BinFloat, ArithmeticError] 在 bin_float 的各项运算下封闭：它不增加任何算术，只提供组合。API 页面列出了各项运算，教程展示了流水线的实际用法。

数学背景

错误单子

设 $V$ 为 BinFloat 值的集合， $E$ 为 ArithmeticError 值的集合。一个 BinFloatResult 是如下不交并中的元素

M V = V + E = \{\, \mathrm{Ok}(x) : x \in V \,\} \cup \{\, \mathrm{Err}(e) : e \in E \,\}.

$M$ 是错误类型固定的异常（或 Either）单子。¹1 E. Moggi, “Notions of computation and monads”, Information and Computation 93(1), 1991；P. Wadler, “Monads for functional programming”, 1995。它的单位与绑定分别是 ok 和 bind：

\begin{aligned} \eta(x) &= \mathrm{Ok}(x), \\ \mathrm{Ok}(x) \mathbin{>\!\!>\!\!=} f &= f(x), \\ \mathrm{Err}(e) \mathbin{>\!\!>\!\!=} f &= \mathrm{Err}(e), \end{aligned}

其中 $f : V \to M V$ 。函数 $f : V \to M V$ 称为 Kleisli 箭头：即可能失败的操作。一旦固定其非值参数，bin_float 的每个 checked 运算（BinFloat::sqrt、div_checked、try_ln_ctx、…）以及 Luna-Flow/arithmetic 的每个 checked trait 方法（SqrtChecked::sqrt_checked、DivChecked::div_checked、PowIntChecked::pow_int_checked、…）都是这样的箭头。包装类型把它们变为既接受又返回 $M V$ 的方法，从而箭头可以串联。

map 是函子作用，它等于先绑定再取单位：

\texttt{map}(m, g) = m \mathbin{>\!\!>\!\!=} (\eta \circ g),

这正是代码的计算方式（Result::map）。由于 $\eta \circ g$ 从不返回 $\mathrm{Err}$ ，map 不可能引入错误。

提升二元运算

二元运算 $\oplus : V \times V \to M V$ （对不会失败的运算符为 $\eta(x \oplus y)$ ）通过下式提升为 $M V \times M V \to M V$

\operatorname{lift}_{\oplus}(a, b) = a \mathbin{>\!\!>\!\!=} \bigl(x \mapsto b \mathbin{>\!\!>\!\!=} (y \mapsto x \oplus y)\bigr),

这就是私有辅助函数 bin_result_lift2_checked（对不会失败的 $\oplus$ 则为 bin_result_lift2，其内层步骤使用 map）。展开定义即得到 API 所描述的三种情形：

\operatorname{lift}_{\oplus}(a, b) = \begin{cases} \mathrm{Err}(e) & a = \mathrm{Err}(e),\\ \mathrm{Err}(e') & a = \mathrm{Ok}(x),\ b = \mathrm{Err}(e'),\\ x \oplus y & a = \mathrm{Ok}(x),\ b = \mathrm{Ok}(y). \end{cases}

clamp 按值、min、max 的顺序嵌套三次绑定，因此它以同样的方式在三个操作数的错误中作出选择。

设计决策

封闭的包装类型，而非处处使用 `Result`

问题。 bin_float 的 checked 运算返回 Result，而不会失败的运算返回普通值。混用两者的计算需要在每个 checked 步骤之后解包或 match，而且过早解包很容易丢掉错误。

方案。 (a) 让用户编写 match 链。(b) 使用 MoonBit 的 raise 错误。(c) 提供一个封闭类型，其每个运算都接受可能已失败的操作数。

选择：(c)。 Luna-Flow 各库以结构化的 Result 值而非抛出的错误来报告失败，因此 (b) 会破坏 checked trait 的约定。采用 (c) 时每个运算都接受 BinFloatResult 操作数，于是公式 two / (one / a + one / b) 可以用普通运算符书写，第一个失败步骤的错误会一直传递到最后。包装类型保持为独立类型，使普通的 BinFloat 在代数代码中保留其 IEEE 语义（1 / 0 为 $+\infty$ ）。

只取第一个错误，而非全部错误

问题。 当一个运算的两个操作数都已失败时，必须返回其中一个错误。

方案。 (a) 返回左侧的错误。(b) 像 applicative 校验那样收集两者。(c) 任意返回一个。

选择：(a)。 收集错误需要 ArithmeticError 上的幺半群结构，而该类型并没有；错误列表也将是另一种类型。左偏的选择是确定性的，且与表达式的阅读顺序一致；下文的第一错误定理精确说明了整个表达式报告的是哪个错误。

运算使用哪个上下文

没有上下文参数的运算必须自行选定精度和指数范围。包装类型使用操作数自身的格式，从而以某一精度开始的流水线始终保持该精度：

操作	所用上下文
`+`, `-`, `*`, `/`, `min`, `max`	与 `BinFloat` 运算符相同：取操作数中较大的精度，就近舍入（偶数优先）
一元初等函数、`rootn`	`BinaryContext::unbounded(x.precision())`
`pow`, `hypot`, `atan2`	`BinaryContext::unbounded(max(p_x, p_y))`
`sqrt`, `pow_int`, `pown`	以操作数精度调用的 `BinFloat` 方法
`pow_nat`	`ArithmeticContext::new(x.precision())`，传给 `PowNatChecked`
每个 `*_ctx` 方法	给定的 `BinaryContext`

unbounded(p) 表示精度 $p$ 、就近舍入（偶数优先）且无指数限制，因此这些运算永远不会上溢或下溢。对于 pow_nat，包装类型经由 Luna-Flow/arithmetic 的 trait 实现，bin_float 用 BinaryContext::from_arithmetic_context 把 ArithmeticContext 映射为 BinaryContext：精度直接复制，RoundingMode 映射为二进制舍入属性，e_min / e_max 在存在时成为指数界（两者都缺省时即为 unbounded）。ArithmeticContext 的 clamp 字段在二进制中没有意义，不予使用。

上下文运算保留值、丢弃标志

BinFloat::*_ctx 运算返回 $(v, \phi) \in V \times F$ ，其中 $F$ 是 BinaryFlags 的集合。包装类型的 _ctx 方法将它们与投影 $\pi_1(v, \phi) = v$ 复合：

\texttt{add\_ctx}(a, b, c) = \operatorname{lift}_{\eta \circ \pi_1 \circ \oplus_c}(a, b).

这是有意为之的信息丢失。若保留标志，包装类型就会成为异常单子与 $F$ 上 writer 单子的组合，而二进制标志就必须与不报告任何标志的运算（map、普通运算符）合并。十进制流水线作出相反的选择，因为 IEEE 十进制算术通常依据其标志进行审计；参见 decimal_checked 设计。因此，_ctx 方法的 IEEE 异常情形都算作成功：div_ctx 除以零得到 $\pm\infty$ ，而 div（它调用 div_checked）则失败。两个名字让两种契约在调用处一目了然。

正确性 / 不变式

单子律

对所有 $x \in V$ 、 $m \in M V$ 以及 Kleisli 箭头 $f, g$ ：

\begin{aligned} &\text{(left identity)} && \eta(x) \mathbin{>\!\!>\!\!=} f = f(x),\\ &\text{(right identity)} && m \mathbin{>\!\!>\!\!=} \eta = m,\\ &\text{(associativity)} && (m \mathbin{>\!\!>\!\!=} f) \mathbin{>\!\!>\!\!=} g = m \mathbin{>\!\!>\!\!=} \bigl(x \mapsto f(x) \mathbin{>\!\!>\!\!=} g\bigr). \end{aligned}

证明。 左单位律即绑定的第一条定义式。对右单位律，情形 $m = \mathrm{Ok}(x)$ ： $\mathrm{Ok}(x) \mathbin{>\!\!>\!\!=} \eta = \eta(x) = \mathrm{Ok}(x)$ ；情形 $m = \mathrm{Err}(e)$ ：两边均为 $\mathrm{Err}(e)$ 。对结合律，情形 $m = \mathrm{Err}(e)$ ：左边为 $\mathrm{Err}(e) \mathbin{>\!\!>\!\!=} g = \mathrm{Err}(e)$ ，右边为 $\mathrm{Err}(e)$ 。情形 $m = \mathrm{Ok}(x)$ ：两边都化为 $f(x) \mathbin{>\!\!>\!\!=} g$ 。 $\square$

在代码中它们写作 BinFloatResult::ok(x).bind(f) ≡ f(x)、m.bind(BinFloatResult::ok) ≡ m 和 m.bind(f).bind(g) ≡ m.bind(x => f(x).bind(g))，其中 $\equiv$ 比较的是 result()。正是结合律使流水线与其如何拆分为辅助函数无关：串联两个 checked 步骤的辅助函数可以内联或提取，而不改变结果。

函子律可由 $\texttt{map}(m, g) = m \mathbin{>\!\!>\!\!=} (\eta \circ g)$ 推出：

\begin{aligned} \texttt{map}(m, \mathrm{id}) &= m \mathbin{>\!\!>\!\!=} \eta = m,\\ \texttt{map}(\texttt{map}(m, g), h) &= (m \mathbin{>\!\!>\!\!=} \eta g) \mathbin{>\!\!>\!\!=} \eta h = m \mathbin{>\!\!>\!\!=} (x \mapsto \eta(g x) \mathbin{>\!\!>\!\!=} \eta h) = m \mathbin{>\!\!>\!\!=} \eta (h \circ g) = \texttt{map}(m, h \circ g). \end{aligned}

因此 normalized、neg、abs、ulp 和 with_precision 都是 map，可以像底层的 BinFloat 函数那样被融合或重排。

这些定律可以在具体的箭头上检验；这里 $f$ 是 checked 平方根， $g$ 是 checked 对数：

///|
test "monad laws on checked arrows" {
  let f = fn(x : @bin_float.BinFloat) { @bin_float_checked.BinFloatResult::from_result(x.sqrt()) }
  let g = fn(x : @bin_float.BinFloat) {
    @bin_float_checked.BinFloatResult::ok(x).ln()
  }
  let same = fn(a : @bin_float_checked.BinFloatResult, b : @bin_float_checked.BinFloatResult) {
    match (a.result(), b.result()) {
      (Ok(x), Ok(y)) => x == y
      (Err(e), Err(d)) => e == d
      _ => false
    }
  }
  for n in [-4, 0, 2, 9] {
    let x = @bin_float.BinFloat::from_int(n)
    let m = @bin_float_checked.BinFloatResult::ok(x)
    assert_true(same(m.bind(f), f(x)))
    assert_true(same(m.bind(@bin_float_checked.BinFloatResult::ok), m))
    assert_true(same(m.bind(f).bind(g), m.bind(y => f(y).bind(g))))
  }
}

第一错误定理

考虑一棵表达式树，其叶子是 BinFloatResult 值，内部节点是包装类型的运算。MoonBit 对参数进行及早求值，因此每个节点都会被求值。若一个节点的所有子节点都成功而该运算本身失败，则称该节点产生一个错误（叶子若为 Err，则它产生自身的错误）。

定理。 若有任何节点产生错误，则表达式的值为按后序（子节点从左到右，然后是该节点）第一个产生错误的节点所产生的错误。否则其值为对叶子值应用 bin_float 运算所得的成功结果。

证明，对树作归纳。叶子的情形是显然的。对节点 $n = \operatorname{lift}_{\oplus}(t_1, t_2)$ ，后序依次列出 $t_1$ 的节点、 $t_2$ 的节点，然后是 $n$ 。若 $t_1$ 含有产生错误的节点，由归纳假设， $t_1$ 的值为其中第一个节点的错误 $e$ ，它在 $n$ 的后序中也排在最前，而 $\operatorname{lift}_{\oplus}$ 返回左侧错误 $e$ 。否则 $t_1$ 的值为 $\mathrm{Ok}(x)$ ；若 $t_2$ 含有产生错误的节点， $t_2$ 的值为其中第一个节点的错误，由 $\operatorname{lift}_{\oplus}$ 的第二种情形它被返回，同样与后序一致。否则两者都成功， $n$ 恰在 $x \oplus y$ 失败时产生错误，这就是结果。一元节点是绑定，可由同样的分情形讨论得出；clamp 是三个子节点的版本。 $\square$

例如，在 left + one / zero 中叶子 left 在后序中排在最前，因此报告它的错误；而在 one / zero + left 中除法排在最前。因此，即使 $\oplus$ 在值上可交换，提升后的运算在错误上也不可交换：在成功时 $\operatorname{lift}_{+}(\mathrm{Ok}\,x, \mathrm{Ok}\,y) = \mathrm{Ok}(x+y) = \mathrm{Ok}(y+x)$ ，因为舍入后的二进制加法可交换；但有两个错误时，报告哪一个取决于顺序。

没有其他不变量

包装类型只持有一个 Result，不增加任何状态，因此 BinFloat 的每个不变量（规范化的系数、精度至少为一、正确舍入的运算）都原样延续到成功分支。每个包装步骤在被委托运算之外只增加 $O(1)$ 的开销。

被否决的替代方案

在包装类型中存储 BinaryFlags。 参见上文的决策；标志属于 bin_float 的 (value, flags) API。
把 NaN 结果变为错误。 IEEE 把 NaN 定义为一个值，而 bin_float 已在其 checked API 中决定了哪些情形是错误；在这里再设一套策略，会使包装类型与同一类型的 checked trait 实现不一致。
错误累积。 需要 ArithmeticError 上的合并运算，而 Luna-Flow/arithmetic 并未定义。
隐式恢复。 没有任何方法能把错误重新变回值；恢复与否由调用者在 result() 之后决定。

边界

自身不含算术：每个数值结果都来自 bin_float。
没有 IEEE 标志、没有上下文状态、没有交换编码，也没有十进制转换。
没有错误恢复或错误累积；只保留第一个错误。
包装类型上没有 Eq、Show 或 Compare；请通过 result() 进行比较。
运算集合即生成的接口中所列者；bin_float 中没有对应包装方法的运算可通过 map 或 bind 使用。

E. Moggi, “Notions of computation and monads”, Information and Computation 93(1), 1991；P. Wadler, “Monads for functional programming”, 1995。 ↩

bin_float_checked 设计