Skip to content

Range types for integers (or refinement types?) #19801

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
BryanQuigley opened this issue Dec 13, 2014 · 3 comments
Closed

Range types for integers (or refinement types?) #19801

BryanQuigley opened this issue Dec 13, 2014 · 3 comments
Labels
E-hard Call for participation: Hard difficulty. Experience needed to fix: A lot.

Comments

@BryanQuigley
Copy link

It seems like a natural extension of how variables (immutable by default, mutable if specified) are defined to allow the programmer to dictate a specific range of allowed values for an integer. If I know a value is only valid between 0-1000 the sooner I declare that the better it is for catching bugs, off by one errors, and more...

I'm not sure what exact syntax would work, maybe:

let mut(0,1000) x = 0i;

x is only valid from 0-1000 inclusive.

(Apologies if this is already possible, I've been parsing the docs trying to learn Rust.)

@aochagavia
Copy link
Contributor

@BryanQuigley Thanks for your comments! As this is a non-trivial change to the language, I suggest that you open a discussion on http://discuss.rust-lang.org/ and see what people think. If the idea gains traction, you could write an RFC for it.

@kmcallister kmcallister changed the title Declare variables with valid range? Range types for integers Jan 16, 2015
@kmcallister kmcallister added E-hard Call for participation: Hard difficulty. Experience needed to fix: A lot. A-an-interesting-project labels Jan 16, 2015
@kmcallister
Copy link
Contributor

Ada has this. It would be great in Rust, as we're going for the same niche of low-level + high-assurance.

I wonder though if we should go for a more general system, such as refinement types or pre/post-conditions. There have been a number of successes bolting these onto languages like Haskell, F#, and C#. AIUI, they manage this without heavy changes to the core language. The condition checker is a mostly-separate tool that gathers proof obligations from the source code and passes them to a SMT solver.

Basically I think this is an area where we should give researchers and other interested parties some time to experiment before we standardize something into Rust itself.

@kmcallister kmcallister changed the title Range types for integers Range types for integers (or refinement types?) Jan 16, 2015
@steveklabnik
Copy link
Member

I'm pulling a massive triage effort to get us ready for 1.0. As part of this, I'm moving stuff that's wishlist-like to the RFCs repo, as that's where major new things should get discussed/prioritized.

This issue has been moved to the RFCs repo: rust-lang/rfcs#671

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
E-hard Call for participation: Hard difficulty. Experience needed to fix: A lot.
Projects
None yet
Development

No branches or pull requests

4 participants