Initial Idea: Bounded Numbers

[blacktemplar]

In a lot of my projects I argue in some way or another along the lines:

Those inputs are (per API specifications) guaranteed to be smaller than X, therefore summing two of them up can never overflow within u8.

Thinking about this problem more. I was wondering if we could move this argumentation from a purely meta level to the type level and let the compiler do the reasoning.

This is what I want to achieve with my project GitHub - blacktemplar/bounded-num.

It is in a very prototype state and the API is very minimal and documentation is missing fully.

The idea is that instead of:

let a: u8 = ...;
let b: u8 = ...;
let c: u8 = a + b;

one would do:

let a: BoundedNum<u8, P5, P100> = ...;
let b: BoundedNum<u8, P7, P150> = ...;
// type hint is unnecessary here, I just put it here for illustration,
// the compiler could figure it out just fine
let c: BoundedNum<u8, P12, P250> = a + b;

This has multiple benefits: One sees directly from the type the potential range of the value AND operators like Add can be implemented in a way that they never overflow. I consider the latter part the more important part given the motivation of this project. For me overflows can be quite dangerous, especially since they can happen silently in production (and are hard to debug if you cannot reproduce production with overflow checks turned on).

Just to illustrate how the compiler helps to avoid overflows, this would not compile

let a: BoundedNum<u8, P5, P100> = ...;
let b: BoundedNum<u8, P7, P156> = ...;
let c = a + b;

because a might be 100 and b might be 156 which would lead to an overflow of u8 when added.

It would be great to hear from others if this idea could be useful and if there are no other crates that achieve the same / a similar thing (I have tried searching for such crates but couldn't find one that satisfied me). Also, of course if someone wants to review my very early prototype code I am very happy to get feedback (although at this stage a review of the idea is more important for me than the code).

[Jesper]

Pascal had something like that:

var
  x: 1..10;

It could check you didn't assign an out-of-range value to x ... though I don't think the checks extended to later non-constant assignments. But you could do that in rust ...

[philomathic_life]

Refinement types is the more general concept. flux is one example of a refinement type checker for Rust. You can read other topics on the matter like this one. In Rust it seems like the term "pattern type" is more common, and here is a now-closed MVP on the matter which also mentions why pattern/refinement types likely won't have a subtyping relation (e.g., like &'static T is a subtype of &'a T) but instead would rely on less powerful coercion (e.g., like ! coerces to T).

[blacktemplar]

Wow, thank you for the good references. I have looked into flux and it is a very cool concept. Although I think it is quite a bit different to what I had in mind. Of course it is much more general but it also means it feels a bit like a patch, given that a third-party tool is needed to check it and the way the annotations are designed as opt-in (if I understand it correctly) it might happen that one forgets to add some annotations. The last point is for me especially important in the context of overflows. I want to have an API that just doesn't allow silent overflows for my types (of course we can have stuff like wrapping_add so that the user explicitly states that they want to wrap around the type boundaries).

So I think for the concrete use case of bounded numbers I feel like a more explicit direct type approach has benefits. Of course it is a trade-off as my approach is much more enforcing once you use the bounded types and therefore can also be restrictive (although there is always the option to get the unbounded inner value like u8 and directly work with it, I see this somehow as the equivalent of unsafe as you have to be careful with overflows if you do it).

Of course it would be great if this would be a language-built-in as you suggested in your other links and that it would have sub-type relations or at least some type of coercion. But until this happens my library I would say can achieve almost the same thing except that sub-typing/coercion is not given so one has to call .into() or .try_into() manually if one wants to change the bounds (note that currently I don't implement Into and TryInto but have those methods without any traits because I ran into problems with overlapping implementations when I tried to implement the traits).

So long story short, I still see a use case for this much more specific approach to refinement types compared to flux.

[tdelmas]

Something like that ? ranged_integers - Rust

let x = r!([1 6] 5);
let y = r!([1 6] 4);

let a = x + y;  // The minimum is (1+1)=2, the maximum is (6+6)=12
let check_add: Ranged<2, 12> = a;  // Range assertion assignment
assert_eq!(check_add, r!(9));

let s = x - y;  // The minimum is (1-6)=-5, the maximum is (6-1)=5
let check_sub: Ranged<-5, 5> = s;  // Range assertion assignment
assert_eq!(check_sub, r!(1));

[jhpratt]

I created the deranged crate for this purpose, and it does anything possible within compiler limitations. It even includes niche value optimization via a custom struct!

[Redglyph]

There's an RFC but it's still open (not sure why):

Numerical Constrained Types

Yes, I remember using that in Pascal, Ada and VHDL. It can be very handy.

[tdelmas]

@jhpratt you mean https://crates.io/crates/deranged ? (your link is a 404 for me)

[blacktemplar]

Oh this looks interesting, thanks for the link, I think this is something similar to what I imagined. Interesting that they use const generics (vs me using typenum) and get away with it with some helper trait construct.

[jhpratt]

Fixed! I typed it off hand