Numerical Constrained Types

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.

No files, tests, or implementation entry points are identified. Start by reviewing the proposed numerical constraints and conditional-cast designs, then consult the repository's RFC process to determine whether the proposal is sufficiently refined; completion would require an accepted design rather than a small code change.