Nim was inspired by Ada & Modula, and has subranges [1]:
type
Age = range[0..200]
let ageWorks = 200.Age
let ageFails = 201.Age
$ nim c main.nim
Error: 201 can't be converted to Age
I know quite some people in the safety/aviation domain that kind of dislike the subranges, as it inserts run-time checks that are not easily traceable to source code, thus escaping the trifecta of requirements/tests/source-code (which all must be traceable/covered by each other).
Weirdly, when going through the higher assurance levels in aviation, defensive programming becomes more costly, because it complicates the satisfaction of assurance objectives. SQLite (whiches test suite reaches MC/DC coverage which is the most rigorous coverage criterion asked in aviation) has a nice paragraph on the friction between MC/DC and defensive programming:
https://www.sqlite.org/testing.html#tension_between_fuzz_tes...
Ideally, a compiler can statically prove that values stay within the range; it's no different than proving that values of an enumeration type are valid. The only places where a check is needed are conversions from other types, which are explicit and traceable.
If you have
The type of c could be u8 in 0..200. If you have holes in the middle, same applies. Which means that if you want to make c u8 between 0..100 you'd have to explicitly clamp/convert/request that, which would have to be a runtime check.In your example we have enough information to know that the addition is safe. In SPARK, if that were a function with a and b as arguments, for instance, and you don't know what's being passed in you make it a pre-condition. Then it moves the burden of proof to the caller to ensure that the call is safe.
But obviously the result of a + b is [0..200], so an explicit cast, or an assertion, or a call to clamp() is needed if we want to put it back into a [0..100].
Comptime constant expression evaluation, as in your example, may suffice for the compiler to be able to prove that the result lies in the bounds of the type.
That's pohibitively expensive in the general case when external input is used and/or when arithmetic is used on the values (main differerence to sum-types).
But if the number type’s value can change at runtime as long as it stays within the range, thus may not always be possible to check at compile time.
The branch of mathematics you need to compute the bounds of the result of an operation is called Interval Arithmetic [1]. I'm not sure of where its limits are (hah), but at the very least it provides a way to know that [0,2] / [2,4] must be within [0,1].
I see there's some hits for it on libs.rs, but I don't know how ergonomic they are.
[1] https://en.wikipedia.org/wiki/Interval_arithmetic
This is basically excuses being made by C people for use of a language that wasn't designed for and isn't suitable for safety critical software. "We didn't even need that feature!"
Ada's compile time verification is very good. With SPARK it's even better.
Runtime constraints are removable via Pragma so there's no tradeoff at all with having it in the language. One Pragma turns them into static analysis annotations that have no runtime consequences.
I like how better more reliable code is more expensive to certify and the problem is the code and not the certification criteria/process being flawed.
> as it inserts run-time checks that are not easily traceable to source code
Modifying a compiler to emit a message at every point that a runtime check is auto-inserted should be pretty simple. If this was really that much of an issue it would have been addressed by now.
Can you help me understand the context in which this would be far more beneficial from having a validation function, like this in Java:
To elaborate on siblings compile time vs run time answer: if it fails at compile time you'll know it's a problem, and then have the choice to not enforce that check there.
If it fails at run time, it could be the reason you get paged at 1am because everything's broken.
It’s not just about safety, it’s also about speed. For many applications, having to check the values during runtime constantly is a bottleneck they do not want.
Like other sibling replies said, subranges (or more generally "Refinement types") are more about compile-time guarantees. Your example provides a good example of a potential footgun: a post-validation operation might unknowingly violate an invariant.
It's a good example for the "Parse, don't validate" article (https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-va...). Instead of creating a function that accepts `int` and returns `int` or throws an exception, create a new type that enforces "`int` less than equal 200"
Something like this is possible to simulate with Java's classes, but it's certainly not ergonomic and very much unconventional. This is beneficial if you're trying to create a lot of compile-time guarantees, reducing the risk of doing something like `hmmm = works + 1;`.These kind of compile-time type voodoo requires a different mindset compared to cargo-cult Java OOP. Whether something like this is ergonomic or performance-friendly depends on the language's support itself.
It’s a question of compile time versus runtime.
Yeah it’s something that code would compile down to. You can skip Java and write assembly directly, too.
What happens when you add 200+1 in a situation where the compiler cannot statically prove that this is 201?
Your example also gets evaluated at comptime. For more complex cases I wouldn't be able to tell you, I'm not the compiler :) For example, this get's checked:
If it cannot statically prove it at comptime, it will crash at runtime during the type conversion operation, e.g.: Then, when you run it:Exactly this. Fails at runtime. Consider rather a different example: say the programmer thought the age were constrained to 110 years. Now, as soon as a person is aged 111, the program crashes. Stupid mistake by a programmer assumption turns into a program crash.
Why would you want this?
I mean, we've recently discussed on HN how most sorting algorithms have a bug for using ints to index into arrays when they should be using (at least) size_t. Yet, for most cases, it's ok, because you only hit the limit rarely. Why would you want to further constrain the field, would it not just be the source of additional bugs?
Once the program is operating outside of the bounds of the programmers assumption, it’s in an undefined state that may cause a crash to happen at a later point of time in a totally different place.
Making the crash happen at the same time and space as the error means you don’t have to trace a later crash back to the root cause.
This makes your system much easier to debug at the expense of causing some crashes that other systems might not have. A worthy trade off in the right context.
Out of bounds exception is ok to crash the program. User input error is not ok to crash the program.
I could go into many more examples but I hope I am understood. I think these hard-coded definition of ranges at compile time are causes of far more issues than they solve.
Let's take a completely different example: size of a field in a database for a surname. How much is enough? Turns out 128 varchars is not enough, so now they've set it to 2048 (not a project I work(ed) on, but am familiar with). Guess what? Not in our data set, but theoretically, even that is not enough.
> Out of bounds exception is ok to crash the program. User input error is not ok to crash the program.
So you validate user input, we've known how to do that for decades. This is a non-issue. You won't crash the program if you require temperatures to be between 0 and 1000 K and a user puts in 1001, you'll reject the user input.
If that user input crashes your program, you're not a very good programmer, or it's a very early prototype.
I think, if I am following things correctly, you will find that there's a limit to the "validate user input" argument - especially when you think of scenarios where multiple pieces of user input are gathered together and then have mathematical operations applied to them.
eg. If the constraint is 0..200, and the user inputs one value that is being multiplied by our constant, it's trivial to ensure the user input is less than the range maximum divided by our constant.
However, if we are having to multiply by a second, third... and so on.. piece of user input, we get to the position where we have to divide our currently held value by a piece of user input, check that the next piece of user input isn't higher, and then work from there (this assumes that the division hasn't caused an exception, which we will need to ensure doesn't happen.. eg if we have a divide by zero going on)
I mean, yeah. If you do bad math you'll get bad results and potentially crashes. I was responding to someone who was nonsensically ignoring that we validate user input rather than blindly putting it into a variable. Your comment seems like a non sequitur in this discussion. It's not like the risk you describe is unique to range constrained integer types, which is what was being discussed. It can happen with i32 and i64, too, if you write bad code.
Hmm, I was really pointing at the fact that once you get past a couple of pieces of user input, all the validation in the world isn't going to save you from the range constraints.
Assuming you want a good faith conversation, then the idea that there's bad math involved seems a bit ludicrous
I believe that the solution here is to make crashes "safe" eg with a supervisor process that should either never crash or be resumed quickly and child processes that handle operations like user inputs.
This together with the fact that the main benefit of range types is on the consumption side (ie knowing that a PositiveInt is not 0) and it is doable to use try-catch or an equivalent operation at creation time
For some reason your reply (which I think is quite good) makes me think of the adage "Be liberal in what you accept, and conservative in what you send" (Postels law).
Speaking as someone that's drunk the Go kool aid - the (general) advice is not to panic when it's a user input problem, only when it's a programmers problem (which I think is a restatement of your post)
Happens with DB constraints all the time, user gets an error and at least his session, if not whole process, crashes. And yes that too is considered bad code that needs fixing.
> Stupid mistake by a programmer assumption turns into a program crash.
I guess you can just catch the exception in Ada? In Rust you might instead manually check the age validity and return Err if it's out of range. Then you need to handle the Err. It's the same thing in the end.
> Why would you want to further constrain the field
You would only do that if it's a hard requirement (this is the problem with contrived examples, they make no sense). And in that case you would also have to implement some checks in Rust.
Also, I would be very interested to learn the case for hard requirement for a range.
In almost all the cases I have seen it eventually breaks out of confinement. So, it has to be handled sensibly. And, again, in my experience, if it's built into constraints, it invarianly is not handled properly.
Consider the size of the time step in a numerical integrator of some chemical reaction equation, if it gets too big the prediction will be wrong and your chemical plant could explode.
So too big times steps cannot be used, but constant sized steps is wasteful. Seems good to know the integrator can never quietly be wrong, even if you have to pay the price that tge integrator could crash.
Exactly, but how do you catch the exception? One exception catch to catch them all, or do you have to distinguish the types?
And yes... error handle on the input and you'd be fine. How would you write code that is cognizant enough to catch outofrange for every +1 done on the field? Seriously, the production code then devolves into copying the value into something else, where operations don't cause unexpected exceptions. Which is a workaround for a silly restriction that should not reside in runtime level.
> Why would you want this?
Logic errors should be visible so they can be fixed?
How does this work for dynamic casting? Say like if an age was submitted from a form?
I assume it’s a runtime error or does the compiler force you to handle this?
If you're using SPARK, it'll catch at compile time if there's ever a possibility that it would fit within that condition. Otherwise it'll throw an exception (constraint_error) during runtime for you to catch.
Isn’t this just Design By Contract from Eiffel just in another form?
No, range types are at best a very limited piece of DbC. Design by Contract lets you state much more interesting things about your program. It's also available in Ada, though.
https://learn.adacore.com/courses/intro-to-ada/chapters/cont...