-
Notifications
You must be signed in to change notification settings - Fork 1.6k
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
RFC: Constant generics (restricted Π types) for Rust, core RFC (v2) #1931
Conversation
Also changes the formatting of the FAQ a bit and makes all questions questions :)
Fix some typos in Pi Types RFCs
@kryptan We can't check types for equality that late, even if we wanted to, it'd make the whole trait system less useful. What we can do, however, is codegen unconditional panics inside functions (and warn), while outside functions we should be able to treat evaluation of constants in type as if it "propagates" like WF. That said, I'd need to talk to @arielb1 or @nikomatsakis to understand how well the WF analogy works. |
@kryptan @withoutboats I think |
@kennytm |
@eddyb Sorry I do mean "the equality is unknown". Switched to a better symbol. |
Treating non-panicness of consts as WF would not allow you to do things such as fn bar<n: const usize>(...) {}
fn foo<n: const usize>() {
bar::<n+1>();
} Because we can't prove that constant functions won't panic. |
@arielb1 Right, but I did mention a different strategy in that case (as opposed to using
|
What will we do with local variables? Will we panic when the local is defined? When the local is used? fn main() {
let x;
// ...
x = [0isize; !0 + 1];
} |
If we want to keep consistency with what the compiler already does, we would panic at the assignment:
|
@arielb1 I think the best we can do is when evaluating the array repeat, i.e. as if it were unsized. |
I want to add to @Rufflewind's comment that such provability only comes when you have a recursive expression; non-recursive expressions can be safely evaluated. I don't mind adding that restriction TBH. |
My plans were to get back too this in this weekend, but I was busy. I apologize. I hope that I can do so this week instead. |
We talked about this in IRC a bit today & I had a few thoughts. First, the unification issues seem to come from bracketed expressions. Can we accept a version of this RFC that accepts only literals and variables, and not expressions like Second, the sort of "design" issues (e.g. do we want this in the language? what is the best syntax? how will we teach this?) come mainly from the expression of const parameterization to arbitrary types. We already have one type which is parameterized by a const |
I too think that we should do a minimal version of this RFC as possible, so that we can merge it as fast as possible. For example, we should disallow any calculation, like I have heard @eddyb say though that impl args and struct args are handled the same way in the compiler, so disallowing const generics as generic struct params would involve more work than allowing them. Alternatively, we can do it like with the |
I do think there should at least be a consensus about the syntax for using expressions, even if they aren't in the base RFC. |
@withoutboats, would that subset of features support doing |
I am also curious what @ticki thinks... |
|
||
```rust | ||
// [T; N] is a constructor, T → usize → 𝓤 (parameterize over T and you get A → 𝓤). | ||
fn foo<const n: usize, const l: [u32; n]>() -> [u32; n] { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
In my browser, the letter lowercase L (l)
and the number 1
are almost identical. For a little bit I actually thought it was the number 1
and I was really confused. Something like arr
instead of l
would eliminate any possible confusion
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We use UPPER_SNAKE_CASE
for const
globals and I still would like that somewhat - unless, of course, there's a good argument for keeping it lowercase.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You mean SCREAMING_SNAKE_CASE
?
@rfcbot fcp close In favor of #2000. Thanks for this RFC @ticki, and the previous one as well. This trilogy as a whole has been more ambitious than we feel comfortable committing to right now, but it really highlighted how valuable const generics would be to many users in the community. I'm excited to see us move toward a more expressive const system, if in more incremental steps. |
Team member @withoutboats has proposed to close this. The next step is review by the rest of the tagged teams: No concerns currently listed. Once these reviewers reach consensus, this will enter its final comment period. If you spot a major issue that hasn't been raised at any point in this process, please speak up! See this document for info about what commands tagged team members can give me. |
I'm going to go ahead and close this for the time being; I don't think there's much point in waiting for the final checkbox and FCP here. Discussion has clearly moved to the new RFC. Thanks all! |
boundary between value and type. Unfortunately, as cool as it sounds, it has | ||
some severe disadvantages: most importantly, the type checking becomes | ||
undecidable. Often you would need some form of theorem prover to type check | ||
the program, and those have their limitations too. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I just want to say that the part about undecidability here is very misleading.
To be clear, type checking in Agda and Coq is decidable in general. Undecidability potentially comes into play from non-termination of some program fragment during evaluation that occurs while type checking. But by default, both Agda and Coq require that programs pass the termination check before they can be used. So that source of undecidability cannot arise unless termination checking is explicitly disabled.
The case may be different for Idris since it does not enforce termination by default as far as I know.
However, even in the case where there is undecidability, it's also misleading to bring it up as a serious disadvantage in the context of Rust. The fact of the matter is that type checking in Rust is already undecidable due to the expressive power of associated types. For instance, you can already encode a full lambda calculus interpreter in the type system.
This is one of 3 RFCs. The collection of the pi type RFCs is tracked by issue #1930.
Rendered.