Numerical Constrained Types

[HallM]

Background

Numerical types with defined constraints can be a useful way to perform some sanity checks at compile time. Ada is one of language I know which has these constraints. There may be other applications, but numbers are the main thing I find a use for them. While not a total zero-cost abstraction, the bounds checks are controlled by the user. Further bounds checks within other functions for data validation is not required as the user can know the number is within bounds.

The advantage may be in areas such as libraries or applications with formulas that have defined boundaries for parameters. A library writer may add bounds checks to each function to validate invalid data is not being sent. With numerical constraints, the library writer can define a type and know for certain the parameters are valid. The same level of certainty applies to outputs as the receiver knows the data returns is within the expected range.

I believe these types could lead to more explicit code, especially in the field of medical devices or spacecraft where the data must not be outside of expected ranges. This could be a stepping stone towards Why3-like provers or design by contract, though those could happen externally such as a MIR to Why3's IL conversion.

Looking for some comments and refinement prior to writing an RFC if this sounds sane.

Additions

The language would need two new parts: a way to specify numerical constraints and a conditional-cast capability that performs the run-time validation.

Specify numerical constraints

One way to specify constraints similar to Ada could be:

type Hours = u32 in 0..23; // bounded on both upper and lower
type Celcius = f64 in -273.15..; // lower bound, but no upper bound

The addition would be adding the ability to specify the range of valid values. There may be some other concepts of defining constraints. I use the in keyword here instead of range as in is already a reserved keyword in Rust. Another option may be to allow a closure of function to be specified to handle the checks in special circumstances.

Conditional-cast

The second part, conditional-casting, is required as the compiler may not know if one thing could be cast to another. I propose introducing an as? cast which returns something similar to an Option<T>. If possible, having the ability for the compiler to know if a cast could be valid would be beneficial for some cases as well. Using something similar to Option<T> allows the user to handle out of bounds situations cleanly much like doing manual bounds checking. Option<T> itself could work, though None is a bit vague for "value could not cast."

let x: i32 = ...; // not important what x is, only that it is an i32
let h: Hours = 23 as Hours; // compiler may be able to know this is valid
let h: Hours = 24 as Hours; // compiler could know that this is invalid
let h: Option<Hours> = x as? Hours;
if let Some(h) = x as? Hours {}

The cast system could also understand that casting to a superset is always fine, but casting to a subset requires a check. Therefore, h as i32 compiles without a check as h is definitely within the i32 range. If there was a second type in the range 1..24, that type also could not cast to Hours as 1..24 does not cover the entire 0..23 range.

[brendanzab]

Note that Ada also has 'mod' types for things like angles and times, which could be nice.

I'm a fan of range types, but it would be nice if Rust's generic programming support would be powerful enough to support this as a library rather than building it into the language itself. You may run into annoying things like type-level floating point equality though (see: #1038 (comment)).

[ticki]

On a sidenote, this has been proposed multiple times, but often rejected due to introducing typestate. I'd just like to note, that it can be done without typestates, solely with subtyping relationship defined by the subset relation. In such a case, the bounded type does not change its state (bound), since the bound is a part of the type, not the state. Thus reassigning is only possible if it is a subtype of the original declared type.

One thing that would be cool with this is that you can make a vector primitive with some bound associated with its length. This makes it possible to index by some subtype of usize[0..len] without a bound check.

[ticki]

@bjz, mod types are a lot simpler.

[ticki]

Also, I would prefer having a function like shrink instead of as?.

[oli-obk]

We already have From/Into and TryFrom/TryInto are on the way, so there's no reason to use as or as?.

One way to specify constraints similar to Ada could be:
type Hours = u32 in 0..23; // bounded on both upper and lower

side-note: Rust uses ... to denote inclusive ranges and .. to denote exclusive ranges (excluding just the end of the range)

even better, once we have value generics, we can make the primitive types generic over their range:

type Hours = u32<0, 23>;

or if we get more than just integral value generics:

type Hours = u32<0..24>;

Together with defaults for generics, the primitive types' generic arguments would simply default to their maximal range.

This has the major advantage of

Rust's generic programming support would be powerful enough to support this as a library rather than building it into the language itself. You may run into annoying things like type-level floating point equality though (see: #1038 (comment)).

[HallM]

I didn't realize it had been discussed before. Github search didn't come up with anything of use. "Value Generics" wasn't something I would have expected as handling ranged-types. I did see the discussion on Design by Contract and thought range-types can handle some of the DbC use cases in the short term without as much effort.

Thanks for the heads up on the .. and .... I'm still fairly new to Rust (< 1 month experience) I had a feeling .. was wrong thinking of for i in 0..x does not include x. I didn't know there was an inclusive version.

The TryFrom looks to solves the conditional-cast part. as? was something that follows the standard cast syntax and also I am used to it with Swift. For my cases with scientific equations, shrink would be dangerous. If the number isn't in bounds, something failed and needs to be handled.

Mod types would also be useful, especially in angles.

I did realize I did not put any significant thought into arithmetic with range-types. There's so many possibilities and different use cases. With ranged types, range-overflow/underflow is very likely. Allowing an overflow without check breaks the type's contract, but is not zero-cost. One could perform arithmetic on the underlying type and return a value in that underlying type that the user must check-cast to their desired range-type. I'm thinking from a use case of scientific functions where parameters have various boundaries, but they are still operated on as numbers with some new type/unit and new set of boundaries as the result.

I'll just hang back for now to see how the value generics pan out.

[ticki]

More ideas in a similar style can be found here:

1. Range types for integers (or refinement types?) #671
2. Avoiding integer overflow #45
3. https://github.com/bill-myers/rfcs/blob/no-integer-overflow/active/0000-no-integer-overflow.md
4. https://www.reddit.com/r/rust/comments/43xbg2/why_this_error_was_not_detected_on_compile_time/

[rocallahan]

I'd find these useful. In my experience it's quite common to have a type that's either an integer in some range, or one of a set of "special values". In C and C++ the special values are encoded as integer constants. In Rust there's a strong temptation to do the same thing, so that you use no more space than C/C++ would. With bounded-range types, you could write the natural type in Rust and the compiler could give you the desired representation, and you'd get run-time bounds checking so you don't accidentally convert an integer value to a special value. As noted above, in some cases this would let you eliminate bounds checks.

Pascal had these in the 80s :-).

[burdges]

Just a thought : A crate could supply a Range type that let users set associated consts. If associated consts to a struct allowed the sugar of being treated as type parameters, then the crate could impl Add, etc. for struct Ranged<T>(T,const min:T, const max: T); so user could do type Hours = Ranged<u8, min=0, max=23>; for this effect.

In fact, one could build a Ranged trait now so that users wrote :

struct Hours(u8);
impl Ranged<u8> for Hours {
    const min: u8 = 0;
    const max: u8 = 23;
    fn ...
}

so the crate could defines operation with impl<T: Ranged> Add for T { ... }, etc. using a few basic fns provided by impl Ranged for manipulating the value. It's clear that macros should simplify all this too, although not as much as setting associated constants as type parameters to a struct.

Also, there are situations where you do not want a numeric type constrained by wrapping so much as an assertion that the type does not violate some constraints. I mentioned in the startup initialized statics thread that an attribute could specify assertions that should occur every time a type gets used, but maybe only during debugging, something like #[debug_assert_invariant(..)], expect you want pre-, post-, etc. versions of _invariant.

[tzakharko]

Constrained types could also play well with compact enums, e.g. by encoding the tag within the unused bits. Lack of support for this is a major reason why I wait with porting my C triangulator code to Rust, as I rely on packed data structures a lot (implemented using C unions and bitfields, which works really nicely and offers a healthy performance boost).

[brendanzab]

Wonder if we could have some kind of linter extension that implements something like Liquid Haskell, with SMT solvers to check that you remain in the numeric range:

• http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/about/
• http://whiley.org/about/overview/
• https://github.com/Microsoft/dafny

Not sure how that would interact with @ticki's const dependent type system RFC (#1657).

[nordlow]

I guess you should mention the case

type X = f64 in ..100; // upper bound, but no lower bound

aswell, as I see no reason why that shouldn't be allowed aswell.

[jarcane]

I'm currently working on a library for generating die rolls, for which this would be very useful indeed, especially with one-sided bounds. Dice can't, for obvious reasons, have a negative or zero number of sides. At the moment, I manually error check for this, but being able to implement such a constraint at the type level a la struct StdDie { u64 in 1.. } would seem both more efficient and more expressive.

[cinemast]

Is there any update on this?

[cinemast]

I also found this: https://docs.rs/bounded-integer/0.1.1/bounded_integer/#examples, but it is no longer compiling under Rust 1.32.

[oli-obk]

Is there any update on this?

Still blocked on rust-lang/rust#44580 being implemented (which it is in the process of)

[sftim]

Rust now has const generics as an MVP.

[g-berthiaume]

+1 for this.
The ability to define things like a Percent type would be valuable.
A great example of "compile-time coordination".

type Percent = u8<0..100>;

This crate might be helpful for implementers : num_traits::Bounded.

[black7375]

It seems Dependent type.

• What is dependent typing?
• Haskell wiki - Dependent type

I think it will be really useful.
I remember that typescript's literal type was very comfortable.

[golddranks]

@black7375 The core capability of dependent types is to rely on runtime values. For example,

let a: u32 = read_input();
let b: u32 = read_input();
// Let's pretend that the return value of `convert_type_less_than` is a dependent type, unexpressable in Rust 1.63
if let Some(a_smaller) = convert_type_less_than(a, b) {
    // The fact that this always succeeds and is sound is guaranteed by a_smaller's type!
    unsafe { unsafe_assert!(a_smaller < b) };
}

Here, if a is' let's say 4 and b is 10, the branch with a_smaller get's executed, and a_smaller's type at this point of execution would be "u32, less than 10". Note that the type would be different on different executions, depending on b's value. In general, it would be "u32, less than b", so that the type depends on b. (I think this would called "sigma type" in type theory.)

Types that restrict the available set of values and depend only on compile time values for specifying the domain, are commonly called "refinement types".

[black7375]

@golddranks Yeah, you are right. Thank you for telling me good information.