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.
In our code we use non byte numbers(deranged and arbitrary int crates), symmetric signed, ordered floats, new num type pattern, our const and categorical num traits(num-traits crate sucks), static assertions, prop tests, easy cast crate(sound as). We have custom decimals.
And newtypes of u64 * u64 = u128.
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:
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!
Not sure I clear on usage.
In our code we use non byte numbers(deranged and arbitrary int crates), symmetric signed, ordered floats, new num type pattern, our const and categorical num traits(num-traits crate sucks), static assertions, prop tests, easy cast crate(sound as). We have custom decimals. And newtypes of u64 * u64 = u128.
Looking into lean4 provers integrated into rust).
Can your crate compose somewhat with above?