5 ms·
In a language with a sufficiently advanced type system you can use Peano numbers to specify a type specifying an integer between 0 and 10. These type systems us
by tolmasky 8y ago
In a language with a sufficiently advanced type system you can use Peano numbers to specify a type specifying an integer between 0 and 10. These type systems usually are smart enough to have optimized internal representation of said types.
- steveklabnik 8y agoYou can do that in rust, there’s even a package for it. It will destroy your compile times though. In the future we’ll have const generics that let you express it directly without that shenanigans.
- tolmasky 8y agoI would love to have something that would translate a more human readable version that looks like a constraint or range that internally translates to the same functionality of the peano solution. If that's what you're saying Rust intends to have then I'm very excited and continue to be impressed by the progress there.
- steveklabnik 8y agohttps://github.com/rust-lang/rfcs/blob/master/text/2000-const-generics.md https://github.com/rust-lang/rfcs/blob/master/text/2000-cons... is the current accepted design; we plan to go further in the future, but wanted something minimal at first. This is likely to land in nightly by the end of the year and be stable sometime early next year.
- jgibson 8y agoDoesn't Ada have this ability where you define numeric types with a range?
- MaxLeiter 8y agoYes, like so type jump_by_tenth is delta 0.1 range 1.0 .. 99.0;
- adrianN 8y agoYes but afaik it translates to runtime checks.
- red75prime 8y agoIt cannot be done in compile-time in general case. Rice's theorem forbids. Every non-trivial property of a program (like whether result of this function lies in this range for all inputs in that range) is undecidable. ETA: I'm not completely correct. Ada could have used something akin to 2-complement overflow handling, that is forcing every operation on a range to have a result in the same range, but it introduces runtime overhead too.