`bin_float_checked` の設計

設計目標

bin_float_checked を使うと、2 進浮動小数点計算を演算の連鎖として記述でき、各演算の後でアンラップする手間なしに、すべての失敗が明示され、どの失敗も失われません。BinFloatResult は bin_float の演算に関して Result[BinFloat, ArithmeticError] を閉じたものにします。新しい算術は追加せず、合成だけを提供します。演算の一覧は 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. その単位と束縛（bind）は 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 トレイトメソッド（SqrtChecked::sqrt_checked、DivChecked::div_checked、PowIntChecked::pow_int_checked、…）は、値以外の引数を固定すればこのような射になります。ラッパーはこれらを、 $M V$ を受け取りかつ返すメソッドに変換するので、射を連鎖させることができます。

map は関手の作用であり、bind の後に単位を適用したものです。

\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$ には、内側のステップに map を使う bin_result_lift2）。定義を展開すると、API が述べる 3 つの場合が得られます。

\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 の順に 3 つの bind を入れ子にするので、3 つのオペランドのエラーからも同じ方法で選択します。

設計上の判断

あらゆる場所で `Result` を使う代わりに閉じたラッパーを使う

問題。 bin_float は checked 演算からは Result を、失敗しない演算からは素の値を返します。両者を混在させる計算では checked ステップのたびにアンラップか match が必要になり、早すぎるアンラップによってエラーを取りこぼしやすくなります。

選択肢。 (a) ユーザーに match の連鎖を書かせる。(b) MoonBit の raise エラーを使う。(c) すべての演算が失敗した可能性のあるオペランドを受け付ける、閉じた型を提供する。

選択：(c)。 Luna-Flow のライブラリは失敗を送出されるエラーではなく構造化された Result 値として報告するため、(b) は checked トレイトの慣例を破ることになります。(c) ではすべての演算が BinFloatResult のオペランドを受け取るので、式 two / (one / a + one / b) を通常の演算子で書くことができ、最初に失敗したステップのエラーが最後まで運ばれます。ラッパーを別の型にしておくことで、代数的なコードでは素の BinFloat が IEEE の意味（1 / 0 は $+\infty$ ）を保ちます。

すべてのエラーではなく最初のエラー

問題。 演算の両方のオペランドが失敗している場合、どちらか 1 つのエラーを返さなければなりません。

選択肢。 (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 のトレイトを経由し、bin_float は BinaryContext::from_arithmetic_context によって ArithmeticContext を BinaryContext に対応付けます。精度はそのままコピーされ、RoundingMode は 2 進の丸め属性に対応付けられ、e_min / e_max は存在すれば指数の上下限になります（両方ともなければ unbounded になります）。ArithmeticContext の clamp フィールドは 2 進では意味を持たないため使われません。

コンテキスト付き演算は値を保持し、フラグを捨てる

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 モナドの組み合わせになり、2 進フラグを何も報告しない演算（map、素の演算子）と組み合わせなければならなくなります。10 進のパイプラインは逆の選択をしています。IEEE の 10 進算術は通常フラグによって監査されるからです。decimal_checked の設計を参照してください。その結果、_ctx メソッドにおける IEEE の例外的なケースは成功として扱われます。div_ctx でゼロ除算すると $\pm\infty$ が得られますが、div（div_checked を呼び出す）は失敗します。2 つの名前によって、2 つの契約の違いが呼び出し箇所で見えるようになっています。

正しさ／不変条件

モナド則

すべての $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}

証明。 左単位則は bind の最初の定義式そのものです。右単位則について、 $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() を比較します。結合則があるからこそ、パイプラインはヘルパー関数への分割の仕方に依存しません。2 つの 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}

したがって、いずれも map である normalized、neg、abs、ulp、with_precision は、元の 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}$ の 2 番目の場合によってそれが返されます。これも帰りがけ順と一致します。それ以外では両方が成功であり、 $n$ がエラーを発生させるのはちょうど $x \oplus y$ が失敗するときで、それが結果となります。単項ノードは bind であり、同じ場合分けから従います。clamp は子が 3 つの版です。 $\square$

たとえば left + one / zero では葉 left が帰りがけ順で最初に来るのでそのエラーが報告され、one / zero + left では除算が最初になります。したがって、 $\oplus$ が値に関して可換であっても、持ち上げた演算はエラーに関して可換ではありません。成功同士では、丸めた 2 進加算が可換なので $\operatorname{lift}_{+}(\mathrm{Ok}\,x, \mathrm{Ok}\,y) = \mathrm{Ok}(x+y) = \mathrm{Ok}(y+x)$ ですが、エラーが 2 つある場合、報告されるエラーは順序に依存します。

その他の不変条件はない

ラッパーは Result を 1 つ保持するだけで状態を追加しないので、BinFloat のすべての不変条件（正規化された係数、精度が 1 以上、正しく丸められた演算）は成功の分岐にそのまま引き継がれます。各ラッパーステップのコストは、委譲先の演算に加えて $O(1)$ です。

却下した代替案

ラッパーに BinaryFlags を保存すること。 上記の決定を参照してください。フラグは bin_float の (value, flags) API に属します。
NaN の結果をエラーに変えること。 IEEE は NaN を値として定義しており、bin_float はどのケースがエラーかを checked API ですでに決めています。ここで 2 つ目の方針を設けると、ラッパーが同じ型の checked トレイト実装と食い違うことになります。
エラーの蓄積。 ArithmeticError 上の結合演算が必要ですが、Luna-Flow/arithmetic はそれを定義していません。
暗黙の回復。 エラーを値に戻すメソッドはありません。回復するかどうかは、result() の後で呼び出し側が決めます。

境界

独自の算術はありません。すべての数値結果は bin_float から得られます。
IEEE フラグ、コンテキスト状態、交換形式のエンコーディング、10 進変換はありません。
エラーの回復やエラーの蓄積はありません。最初のエラーだけが保持されます。
ラッパーには 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 の設計