Hacker News Reader

Comment by tolmasky | Hacker News Reader

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.

View on HN

You 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.

I 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.

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.

Doesn't Ada have this ability where you define numeric types with a range?

Yes, like so

  type jump_by_tenth is delta 0.1 range 1.0 .. 99.0;

Yes but afaik it translates to runtime checks.

It 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.

Reply on news.ycombinator.com