Show HN: Rustにおける composable な数値キャストのためのガロア接続

ドキュメントはこちら、またはdocs.rsでご覧ください。 概要 ガロア接続を第一級のRust値として使用します。これらを使用して数値型間で合法的にキャストし、ランダムではなく単純な不等式によって決定されるラウンドトリップ動作を持つ変換の連鎖を composable に構築します。Connから派生したすべての操作（丸め、飽和、中央値など）は、プロパティテストされた不変量を持ちます。生成された固定幅整数、Qフォーマット、NonZero、およびisoファミリーは、完全なビット幅SMT証明のためのKaniハーネスも備えています。floatのSMTカバレッジは狭く、Testing → SMT verificationの下で示されています。 MSRV: Rust 1.88。MSRVへの更新はマイナーバージョン変更として扱われます—connections = "0.1"をピン留めすると、パッチアップデートでのサイレントな破壊ではなく、0.2リリースとしてMSRVのアップグレードが表示されます。 このクレートはHaskellライブラリconnectionsのRustネイティブポートです。 なぜこのクレートなのか ガロア接続は、部分順序集合（例: f64 → f32、Duration → seconds、f32 → u32 → IpAddrなど）間の静的で合法的な変換に適した形状をしています。各リンクはコンパイル時に指定できます。標準のキャスト演算子as、From、Intoは一度に1つの方向しか提供しません。特にasは、丸め、飽和、および損失のある変換についてサイレントです。 このクレートが標準ツールにない2つの具体的な機能を提供します: 明確なセマンティクス。 多くのx: f64に対して、(x as f32) as f64 != x となります。Connを使用すると、このクレートのすべての接続に対して、次の不等式のペアの少なくとも一方がプロパティテストされます。 左ガロア: ceil(a) ≤ b ⇔ a ≤ upper(b) 右ガロア: lower(b) ≤ a ⇔ b ≤ floor(a) ConnはCopy、const-constructible、heap-freeであり、クレートは#![forbid(unsafe_code)]です。 安全に composable。 compose!マクロは、ペアワイズConnの連鎖をコンパイル時に1つの新しいConn<Src, Dst>に折りたたみます。 composableされた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); // 逆方向のアームは、右ガロア法則によって`floor`とペアになっています。 assert_eq!(U032I032.lower(-1), 0_u32); 様々なドメインでの10個の作業例については、EXAMPLES.mdを参照してください。 接続とは何か？ 順序集合AとBの間のガロア接続は、単調写像のペアf: A → Bおよびg: B → Aであり、f(x) ≤ y ⇔ x ≤ g(y)を満たします。fを接続の左または下随伴、gを右または上随伴と呼びます。 ここに、3つの要素を持つ2つの集合間の単純な接続を示します（画像は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の間に交差しない2つの曲線があり、これは随伴性の幾何学的署名です。 接続の使用方法 ガロア接続は composable です: (f₁ ⊣ g₁) ∘ (f₂ ⊣ g₂) は再び随伴であり、compose!はそれを静的に、全体として法則チェックされた合成を構築します。デストラクタ（例: upper, lower, ceil, floorなど）を適用した瞬間、Conn代数を離れ、それ以上 composable できない具体的な値を生成します。したがって、早期の分解は、完全なチェーンがそうでなければ享受したであろう静的保証を失います。 そのため、次の2つのヒューリスティックに従うと、最も効果的です。 Connを通してリフトする。Connは小さなブラックボックスです。高階のヘルパー（例: ceil*, floor*, round*, truncate*など）は引数を受け取り、Connの他の（通常はより高忠実度の）ドメインで何かを実行し、結果を元のドメインに戻します。ceil2(t, h, b1, b2) は f(h(g(b1), g(b2))) です：b1/b2をg経由で広いドメインに埋め込み、そこでクロージャhを実行し、f経由で丸めて戻します。オーバーフローしたり精度を失ったりする可能性のあるドメイン演算にはこれを使用してください—より広いドメインで実行し、丸めて戻します。決して手作業で飽和演算を行わないでください。 サイトで composable する。ライブラリレベルでConnをエクスポートし、get/set関数の代わりにConnL/ConnR/ConnK APIを使用します。クライアントコードがマルチホップ変換を必要とする場合、composeマクロ（compose, compose_l, compose_r, compose_k）を使用して、呼び出しサイトで正確なConnを静的に構築します。中間値を手動でスレッドしないでください。クライアントコードがランタイムパラメータを受け取る場合、依存する合法的なConnと明らかに composable する名前付き関数としてヘルパーを保持するのが最善です。ランタイムパラメータと変換ポリシーの選択を静的なConn呼び出しサイトの近くにプッシュする規律は、ポリシーと静的キャストの両方が同じボディで可視的であることを意味します。結果として、明らかに正しい、テストしやすい、将来のユースケースに拡張可能なコードが得られます。 ライブラリL & R種類接続 このライブラリの基本的な型は次のとおりです: pub struct Conn<A, B, K: Kind = L> { f: fn(A) -> B, // L-kind: ceil; R-kind: floor g: fn(B) -> A, // L-kind: upper, R-kind: lower // プラスファントムの種類のタグ K ∈ {L, R} } Conn<A, B, K>は正確にはガロア接続です—単調関数(f, g)のペアであり、その随伴の役割は種類のタグに依存します。L-kind Connはf(a) ≤ b ⟺ a ≤ g(b)を満たし、R-kind Connはg(b) ≤ a ⟺ b ≤ f(a)を満たします。種類K = {L, R}がAPIを決定します。L/ConnLは.ceil()と.upper()を公開し、R/ConnRは.floor()と.lower()を公開します。方向名—ceil（上に丸める）とfloor（下に丸める）—は下流の直感に一致します。「天井キャストをください」は、呼び出し元が随伴のどちらの側にあるかを知る必要はありません。ただし、L-kind接続で.floor()を呼び出すか、R-kind接続でceilを呼び出すと、コンパイラエラーが発生します。位置名—upper（Lペアの上随伴）とlower（Rペアの下随伴）—は数学に一致します。一般的なT: ConnKバウンドは両方を公開します。なぜなら、トリプルは、具体的なインスタンスでそれぞれがどのように丸められるかに関係なく、両方の随伴を持つからです。 定数対マーカー - 通常の接続は、Conn<A, B, L>またはConn<A, B, R>型のpub constです。双方向ConnK接続はpub structとして出荷されます—両方のConnLとConnRを実装するゼロサイズのマーカー型です。const対structの形状は、名前がどちらの種類を参照しているかを一目でわからせます。 API Conn<_, _, L>（およびデフォルトメソッドディスパッチを介した任意のConnL実装者）のLサイドメソッド: ceil, upper, プラスceil1/2, upper1/2リフター。 Conn<_, _, R>（および任意のConnR実装者）のRサイドメソッド: floor, lower, プラスfloor1/2, lower1/2リフター。 双方向ヘルパー（クレートルートに再エクスポート）: interval, round/round1/round2, truncate/truncate1/truncate2, median。 すべてT: ConnK（ConnL + ConnRのスーパー・トレイト、同じ(A, B)上）にバインドされるため、単一方向のConnではなくトリプルマーカーでのみ呼び出し可能です。 種類規律は構造的です。L-kind Connで.floor(...)を呼び出すとコンパイラエラーになります（メソッドはConn<_, _, R>でのみ存在します）。同様にRで.ceil(...)を呼び出す場合も同様です。双方向ヘルパーも、単一方向のConnがConnKを実装していないため、コンパイル時に単一方向オペランドを拒否します。 モジュール ファミリー モジュール IEEE-754型 float Qフォーマット バイナリ固定小数点（Q###Q###、i8/u8 … i128/u128バックエンド） fixed::{i008,…,i128, u008,…,u128} (fixed cargo feature) 標準整数幅拡張+狭窄+クロスサイン（I###I###、U###I###、U###U###、I###U###） core::{i008,…,i128, u008,…,u128} iN/uN ↔ NonZero<{i,u}N>（I###N###、U###N###） core::{i008,…,i128, u008,…,u128} クロスクレートiso Fixed{I,U}<U0> ↔ {i,u}{N}（Q000I###、Q000U###）および符号付き正規化ビットアイソ（Q007I008 … Q127I128） fixed::{i008,…,i128, u008,…,u128} (fixed cargo feature) Float狭窄 f64 ↔ f32 ↔ f16 N5下（F064F032、F032F016、F064F016） core::{f032,f064} (f16用のf16 cargo feature) 時間クレート型（DATEJDAY、TIMENANO、TIMESECS、TDURSECS、F032TDUR、F064TDUR、PDTMDATE、ODTMDATE、ODTMSECS）およびstd::time::Durationファミリー（SDURU064、SDURU128、F064SDUR、F032SDUR）std::timeを使用するユーザー向け time::{clock,date,datetime,duration,of