Hi HN — I just published 0.1.0 of `connections`, a Rust port of an older Haskell library I wrote.
It's intended to address a common issue with casting: each cast's individual behavior is specified, but the syntax doesn’t describe what a cast and its reverse do together. Once several conversions are chained, their rounding, saturation, and range choices become difficult to reason about compositionally.
The core type packages a pair of monotone functions intended to satisfy a Galois law. A left connection, for example, has `ceil: A -> B` and `upper: B -> A`, with:
ceil(a) <= b iff a <= upper(b)
There is a right-handed `lower`/`floor` form as well. When one embedding has both adjoints, the crate exposes `round`, `truncate`, interval, and related operations.
A small example of the boundary behavior:
use connections::conn::ConnR;
use connections::core::u032::U032I032;
assert_eq!(u32::MAX as i32, -1);
assert_eq!(U032I032.floor(u32::MAX), i32::MAX);
assert_eq!(U032I032.lower(-1), 0_u32);
Here `as` preserves the low bits and wraps to -1, while this connection saturates. The claim isn’t that saturation is universally better; it is that the choice is explicit and paired with its reverse under:
lower(b) <= a iff b <= floor(a)
The main payoff is composition. Provided the components satisfy their laws, Galois connections compose, so the compile-time composition macros preserve the relationship without inventing a new rounding policy at each hop.
0.1.0 includes families for Rust integers, IEEE floats, NonZero values, chars, sortable byte encodings, and IP/socket addresses, with optional Q-format, civil-time, hifitime, and hybrid-clock families. The default core has no third-party runtime dependencies; `Conn` is Copy, const-constructible, heap-free, and the crate forbids unsafe code.
Every included connection has a proptest law suite. Generated integer, Q-format, NonZero, and isomorphism families also have Kani harnesses over their full bit-width domains. The float claims are deliberately narrower and documented separately; floats use an N5 wrapper so NaN participates in an explicit reflexive preorder rather than being quietly excluded.
This isn’t intended to replace `TryFrom`: validation, runtime-parameterized conversions, and caller-selected policies generally belong in ordinary named functions.
partialsolve•2h ago
It's intended to address a common issue with casting: each cast's individual behavior is specified, but the syntax doesn’t describe what a cast and its reverse do together. Once several conversions are chained, their rounding, saturation, and range choices become difficult to reason about compositionally.
The core type packages a pair of monotone functions intended to satisfy a Galois law. A left connection, for example, has `ceil: A -> B` and `upper: B -> A`, with:
There is a right-handed `lower`/`floor` form as well. When one embedding has both adjoints, the crate exposes `round`, `truncate`, interval, and related operations.A small example of the boundary behavior:
Here `as` preserves the low bits and wraps to -1, while this connection saturates. The claim isn’t that saturation is universally better; it is that the choice is explicit and paired with its reverse under: The main payoff is composition. Provided the components satisfy their laws, Galois connections compose, so the compile-time composition macros preserve the relationship without inventing a new rounding policy at each hop.0.1.0 includes families for Rust integers, IEEE floats, NonZero values, chars, sortable byte encodings, and IP/socket addresses, with optional Q-format, civil-time, hifitime, and hybrid-clock families. The default core has no third-party runtime dependencies; `Conn` is Copy, const-constructible, heap-free, and the crate forbids unsafe code.
Every included connection has a proptest law suite. Generated integer, Q-format, NonZero, and isomorphism families also have Kani harnesses over their full bit-width domains. The float claims are deliberately narrower and documented separately; floats use an N5 wrapper so NaN participates in an explicit reflexive preorder rather than being quietly excluded.
This isn’t intended to replace `TryFrom`: validation, runtime-parameterized conversions, and caller-selected policies generally belong in ordinary named functions.
Install:
Docs: https://cmk.github.io/connections/ Examples: https://github.com/cmk/connections/blob/main/EXAMPLES.md Crate: https://crates.io/crates/connectionsI'd appreciate any feedback you can give me. Cheers!