5 ms·
Nim was inspired by Ada & Modula, and has subranges [1]: type Age = range[0..200] let ageWorks = 200.Age let ageFails = 201.Age Then at compile tim
by plainOldText 1y ago
Nim was inspired by Ada & Modula, and has subranges [1]:
type
Age = range[0..200]
let ageWorks = 200.Age
let ageFails = 201.Age
Then at compile time:
$ nim c main.nim
Error: 201 can't be converted to Age
[1] https://nim-lang.org/docs/tut1.html#advanced-types-subranges https://nim-lang.org/docs/tut1.html#advanced-types-subranges
- arzig 1y agoWhat happens when you add 200+1 in a situation where the compiler cannot statically prove that this is 201?
- plainOldText 1y agoYour 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: let ageFails = (200 + 2).Age Error: 202 can't be converted to Age If it cannot statically prove it at comptime, it will crash at runtime during the type conversion operation, e.g.: import std/strutils stdout.write("What's your age: ") let age = stdin.readLine().parseInt().Age Then, when you run it: $ nim r main.nim What's your age: 999 Error: unhandled exception: value out of range: 999 notin 0 .. 200 [RangeDefect]
- prerok 1y agoExactly 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?
- fainpul 1y ago> 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.
- prerok 1y agoExactly, 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.
- prerok 1y agoAlso, 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.
- deleted 1y ago[deleted]
- SiempreViernes 1y agoConsider 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.
- wucke13 1y agoI 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_testing_and_100_mc_dc_testing https://www.sqlite.org/testing.html#tension_between_fuzz_tes...
- nine_k 1y agoIdeally, 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.
- estebank 1y agoIf you have let a: u8 is 0..100 = 1; let b: u8 is 0..100 = 2; let c = a + b; 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.
- nine_k 1y agoBut 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.
- Jtsummers 1y agoIn 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.
- mr_00ff00 1y agoHow 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?
- ajdude 1y agoIf 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.
- zeroq 1y agoCan you help me understand the context in which this would be far more beneficial from having a validation function, like this in Java: int validate(int age) { if (age <= 200) return ago; else throw Error(); } int works = validate(200); int fails = validate(201); int hmmm = works + 1;
- jb1991 1y agoIt’s a question of compile time versus runtime.
- baq 1y agoYeah it’s something that code would compile down to. You can skip Java and write assembly directly, too.
- dwattttt 1y agoTo 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.
- jb1991 1y agoIt’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.
- lock1 1y agoLike 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-validate/ 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" class LEQ200 { ... } LEQ200 validate(int age) throws Exception { if (age <= 200) return age; else throw Exception(); } LEQ200 works = validate(200); // LEQ200 fails = validate(201); // LEQ200 hmmm = works + 1; // Error in Java LEQ hmmm = works.add(1); // Throws an exception or use Haskell's Either-type / Rust's Result-type 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.
- wombatpm 1y agoIsn’t this just Design By Contract from Eiffel just in another form?
- Jtsummers 1y agoNo, 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/contracts.html https://learn.adacore.com/courses/intro-to-ada/chapters/cont...