RFC: const-dependent type system.

[ticki]

Introduce Π type constructors for Rust.

Rendered

[thepowersgang]

As currently written, this introduces parsing ambiguities:

• When passing these type-level values you need to know if a type or an expression is being parsed.
• Same with bounds - The lefthand side of a bound has to be parsed as either a type or an expression. (where n < 2 vs where Box<T>: Clone)

[gnzlbg]

From the type grammar I am not sure if floating point types (f34, f64) are allowed or not. Could you clarify this?

[ticki]

@gnzlbg No. The [...] means "the rest of the scalar types".

[thepowersgang]

The section of the type grammar doesn't clearly indicate what has been added.

[ticki]

@thepowersgang

The section of the type grammar doesn't clearly indicate what has been added.

I will update it.

As currently written, this introduces parsing ambiguities:

Oh, that's right. I don't care about the proposed syntax, it was merely for demonstrational purposes. Any ideas on fixing these ambiguities/improving the syntax?

[Amanieu]

I think the easiest way would be to require the const keyword in bounds and generic parameters as well.

[brendanzab]

Isn't Rust's type checker already undecidable? Are you just suggesting that this proposal doesn't add any more undecidable language features? And if so, how do you know?

[ticki]

Well, yes and no. The recursion bound makes it decidable.

[ticki]

But, what I really mean is that there is no theorem proving involved (SMT or SAT solvers).

[thepowersgang]

I believe earlier proposals required const before the first numeric parameter (and all subsequent parameters were assumed to be numeric)

[ticki]

const BLAH: u32 is a possibility.

[Amanieu]

Given this code where a and b are two const fn returning bool:

fn x<n: const usize>() where a(n) {
    y::<n>();
}
fn y<n: const usize>() where b(n) {}

The compiler needs to be able to determine that a(n) implies b(n) for all n in order for this code to successfully typecheck. This RFC doesn't go into much detail about how this is done.

As an example, consider this definition of a and b:

const fn a(n: usize) -> bool {
    n == 0 || n == 1 || n == 2
}
const fn b(n: usize) -> bool {
    n == 1
}

[ticki]

@Amanieu The point is to do the type checking lazily.

fn x<n: const usize>() where a(n) {
    y::<n>();
}
fn y<n: const usize>() where b(n) {}

will compile, no matter what. But, when you start invoking it, the conditions are run.

This is described in the document.

[ticki]

So for example,

fn x<n: const usize>() where a(n) {
    y::<n>();
}
fn y<n: const usize>() where b(n) {}

const fn a(n: usize) -> bool {
    n == 0 || n == 1 || n == 2
}
const fn b(n: usize) -> bool {
    n == 1
}

compiles, but calling the functions will fail, since

x::<2>(); // checks a(2), suceeds.
          // checks b(2), fails and throw error.

Edit: To clarify, the error is thrown at compile time after the check failed.

[Amanieu]

This is a big change from the way Rust currently deals with generics and should probably be listed as a drawback.

I previously proposed adding compilation errors at monomorphization time for atomic operations (depending on platform support) in #1505, but people didn't seem to like the idea much.

[ticki]

@Amanieu Well, often these are rejected for being "too narrow". This is a general solution, which allows for stuff like that, and a lot more.

[ticki]

But yeah, it is a big change (as in semantics. In CLOC, probably not).

[ticki]

Another thing to consider is passing it as arguments, which possibly allows for better syntax (i.e. const_index(2)).

[kennytm]

1. How to express where clauses involving traits and those involving constexpr together? Like this?

fn<p: const usize, q: const usize, T, U> weird()
    where T: Deref<Box<U>> + Copy, 
               T::Target: ?Sized, 
               Vec<U>: Borrow<T>,
               p + q > 1 && p - q > 1 {}

2. Since the stuff inside the <...>, ::<...> and the where clause can now be expressions, would this make parsing / semantic checking more difficult? (How would the grammar be modified to accept const arguments?)

3. Will this parse?

foo::<1<2>()

4. How hard should the compiler perform the value type inference?

fn f0<n: const usize>(p: [u8; n]) {}
fn f1<n: const usize>(p: [u8; n - 1]) {}
fn f2<n: const usize>(p: [u8; n + 100]) {}
fn f3<n: const usize>(p: [u8; n * 5]) {}
fn f4<n: const usize>(p: [u8; n*n*n*n*n - n*n*n*n - 40*n*n*n + 112*n*n - 25*n - 100]) {}

f0([0; 75]);
f1([0; 75]);
f2([0; 75]);
f3([0; 75]);
f4([0; 75]);

5. Are these valid?

fn a<n: const Option<i32>>() {}
fn b<n: const (i32, u32, f32)>() {}
fn c<n: const &'static str>() {}
fn d<n: const Option<Mutex<Rc<fn(String)>>>() {}
a::<None>();
b::<(1, 3, 9.0)>();
c::<"hello">();
d::<None>();

6. Are these valid?

fn foo<T, n: const T>() -> T { n }
fn bar<T, n: const Option<T>>() -> Option<T> { n }
fn baz<n: const usize, l: const [u32; n]>() -> [u32; n] { l }
let x = foo::<u16, 123>();
let y = bar::<Mutex<Rc<fn(String)>>>, None>();
let z = baz::<6, [1,2,3,4,5,6]>();
let z2 = baz::<_, [1,2,3,4,5,6]>();  // ?

[ticki]

1. That's correct.

2. and 3) The syntax is simply explanatory and nothing is proposed about it yet (I am working on a new commit).

3. That's impossible, see Hilbert's tenth problem.

4. Yes.

5. Not as it stand currently. I will add a section about inveritble relations (thus allowing that).

[eddyb]

@ticki Correct me if I'm wrong, but the RFC text doesn't seem to talk about compile/run-time differences and it seems like these are compile-time constant value parameters that monomorphize like type parameters do.
I feel like "dependent types" is potentially misleading, because it's been used for type-level value relationships that are not required to be compile-time constants.

[ticki]

@eddyb, a depedent type is in the most literal sense, just a family of types paremeterized over a value, i.e. f : A → 𝓤, so this is dependent typing, albeit not as expressive as certain other type systems.

[ticki]

But yeah, it is CTFE-only.

[kennytm]

@ticki If all of 4 is impossible how would the compiler knows if a type implements a trait?

impl<T, n: const usize> Clone for [T; n] { ... }
impl<T, n: const usize> InsaneClone for [T; n*n] { ... }

let p1 = [0; 64];
let q1 = p1.clone(); // <- we expect this line should compile, right?
let r1 = p1.insane_clone();

let p2 = [0; 72];
let q2 = p2.clone();
let r2 = p2.insane_clone(); // <- this line should not compile

[eddyb]

@ticki However, theoretical typesystems are simpler than the reality of an efficient/monomorphizing implementation.
Object safety, and particularily the lack of generic methods in them, is probably the most obvious example of that.
I don't mind the term "dependent" if it's explained that unlike e.g. Idris, runtime values cannot be used with value parameters.
It's heavily implied by "constant" but someone coming from Haskell + GHC extensions, Idris, or other such languages may get the wrong impression.

[ticki]

Well, you will have to specify the type. A general inference algorithm would require a SMT solver (which can be added if needed in the future).

[ticki]

@eddyb Agreed.

[matthieu-m]

It seems that as is, any type that can be computed by const fn is eligible as a non-type generic parameter. Am I right?

If so, how do you deal with checking for equality? Structural or using a const Eq?

[aturon]

The lang team discussed this RFC a bit in our most recent meeting from a big-picture perspective. Here are some of our thoughts.

• The problem space. The lack of const generics in Rust is clearly a gap, which ranges from an annoyance (e.g., traits in the standard library implemented for only a fixed set of array sizes) to a show-stopper (e.g., for some libraries in scientific computing). Everyone on the lang team agrees that this is a problem we want to solve eventually. The question is when, and how.

• Roadmap. It's not totally clear how to think about const generics in the framework of our 2017 roadmap. While it's always difficult to say "no" or "not yet", it's also very important to do so if we want to complete our most important goals on time. So the roadmap, in particular, talks about not adding language features for their own sake, but only in the service of the major goals we've specifically chosen as a community.

  • There's not a clear-cut goal in the roadmap that leads directly to const generics. The goal of "Rust should have 1.0-level crates for essential tasks" probably comes closest, if we think of basic scientific computing libraries as one of the essential tasks for Rust. Maybe others can provide a stronger case?
  • On the other hand, there's a sense that const generics could unlock a significant new ecosystem, with a hard to predict impact on Rust's adoption.
  • Even if it doesn't fit into the roadmap, we can still make progress. See below.

• This RFC. There continue to be significant concerns about the scope of this RFC, in particular around the extensions to where clauses. It'd be great to see a minimal design for const generics as a starting point. Some months ago, @eddyb helped sketch such a design, but it hasn't been written up. Paring down the ambitions to a minimal core would be a good way to make progress.

• The state of the compiler. The constant system in the compiler today is encumbered with a huge amount of technical debt, which is one of the reasons that associated constants have made so little progress. Reworking this part of the compiler is basically a prerequisite for const generics. So it makes sense to focus there first, before getting too deep into a design for a system that sits on top. The compiler team is planning a week-long sprint for early next year, and a plan for const handling is one of the goals for that week.

• THE WAY FORWARD. Based on all of the above, here's one potential plan:

  • Compiler team develops and begins executing a plan for const evaluation.
  • In parallel, interested parties develop a more minimal const generics design, in consultation with the lang team (we'd be happy to have a meeting with stakeholders and work through a sketch). That's probably best done as a fresh RFC.
  • If we can reach consensus on the rough shape of the design, the lang team is potentially open to landing experiments behind a feature flag, before the RFC is finalized and accepted.

This plan, in particular, requires minimal bandwidth from the Rust teams (who are otherwise focused on the primary roadmap), but helps unblock other contributors from making progress here, while making sure there's at least rough agreement on the direction.

What do you think?

[mark-i-m]

One extra point regarding the roadmap, I think this RFC would be particularly useful for people coming from C++.

[gnzlbg]

@aturon I agree with all the points you make, but I wish that cleaning up the constant evaluation in the Rust compiler will become a concrete objective for 2017, since it would:

• allow new MIR optimizations which could speed up compilation by reducing the amount of LLVM IR generated => goal: improve compiler performance,

• allow new warnings and diagnostics, like out-of-bounds access of arrays (of compile-time bounds), dead code (branches that will never be taken), tautological / unnecessary comparisons, floating-point expression reordering... => goal: better error messages,

• some of which could translate into a better IDE experience (e.g. while writing code getting an IDE warning saying "this branch will never be taken because of this or that") => goal: solid but basic IDE support,

• and if volunteers team up to come up with RFCs might result in type-level usize support, which will give Rust the ability to abstract over fixed-length arrays of different sizes, closing one gap with C++, allowing better high-level SIMD libraries (there is a current effort to stabilize low-level SIMD), and => goal: improving Rust usability.

Whether volunteers will fix associated consts, const fns, or decide to write a minimal type-level usize RFC, that is up to them and out of scope for the 2017 Roadmap. However, without a solid constant evaluation story, those RFCs are just unimplementable wishful thinking. Constant evaluation is an important enabler technology, we don't know everything that it will allow, and we really need the core team to make it solid.

[eddyb]

Reminder that @solson/miri is in active development and thanks to @solson and @oli-obk's dedication, it can handle all const-eval cases AFAIK and a large number of runtime tests (it turns out that emulating libc works well in practice).
In the meanwhile, I've been trying to sort out the underlying compiler infrastructure needed to make any use of miri for evaluating constants in the type system.
Well, full disclosure: @solson and I were hoping to demo this a couple months ago, but no plan ever survives contact with reality. Maybe more of a focus could be put on this next year had we succeeded, but the work is already there, at least large portions of it, so it will eventually make its way into Rust.

There's also going to be a compiler team dev sprint next year and we will at least try to come up with an acionable MVP for type-level constants, even if they might not be the highest priority.

[eddyb]

I would, in fact, want to see a lot more focus on MIR (borrowck & optimizations), as this year we ran out of bandwidth after pulling the switch, and most of the work done after that was on incremental recompilation.

[aturon]

@gnzlbg

I wish that cleaning up the constant evaluation in the Rust compiler will become a concrete objective for 2017 since it would ...

Thanks for laying out that argument! A couple of thoughts.

First, while I don't disagree that improved const evaluation could impact some of the roadmap goals you mention, to some extent we need to think in terms of a global resource allocation problem.

• For example, there are a lot of things we could be doing that, in principle, could boost compilation speed. But putting more effort into incremental compilation is going to have a much bigger "bang for our buck" than MIR optimizations.
• Similarly, there are error messages in much more dire need of improvement than out of bounds detection.

So to the extent that const evaluation would take resources away from these other efforts, it'd be a net loss to our stated roadmap goals.

Constant evaluation is an important enabler technology, we don't know everything that it will allow, and we really need the core team to make it solid.

Understood, but again, there are a lot of potential enablers. Any of the various language integrations, for example, are potential enablers. The hard work of planning is that we have to make a guess as to the enablers likely to bear the greatest fruit. And that's exactly what the roadmap is trying to do.

That said, this is not a zero-sum game: the Rust community is large and growing, and if we can unlock areas of work, we can potentially gain more total resources. That's part of why, despite not being on the roadmap per se, const eval is part of the upcoming compiler team sprint, as I mentioned above. The key goal there is to set out a basic plan that can unlock contributions to implementation. And as @eddyb notes, there are already people like @solson and @oli-obk laying down important foundations here.

TL;DR: The Rust teams should devote most of their time to work that has the greatest impact on roadmap goals, but should also make small, targeted investments in planning and design sketches that unlock contributions elsewhere.

[aturon]

@rfcbot fcp close

Given the summary of where this RFC and the lang team stand, and the positive response to the steps described there, I'm going to propose FCP to close this RFC and request a fresh RFC taking the more minimalist approach mentioned in the summary. This does not entail rejecting the feature outright; rather, it's about getting to a more tightly-focused initial design. The lang team would be happy to work with stakeholders here to sketch out this more minimalistic design. A fresh RFC thread will help us focus in on the fine details there, and arrive at something plausible to be added after our general const story has been approved.

[rfcbot]

Team member @aturon has proposed to close this. The next step is review by the rest of the tagged teams:

• @aturon
• @eddyb
• @nikomatsakis
• @nrc
• @pnkfelix
• @withoutboats

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.

[ticki]

I haven't seen the response, for some reason. Sorry I missed.

Anyway, I will express that I am extremely disappointed for this close. Mainly because the reason doesn't seem clear at all. In fact, it seems more like a wildcard response to close without any real plan forward or fundamental concerns.

This thread contains a lot of discussion and all criticism has been more or less fixed, it seems.

For minimalistic design: It's kind of hard to define. There is a lot in this RFC, much of which is merely extension to the core proposal, but I can't see a way to more minimalistic describing a feature solving the problem.

I can't say I approve of this decision without futher reason behind it, and perhaps a less vague response with actual plans.

[aturon]

@ticki, just to check, did you read the summary of the lang team discussion? I feel like that comment was pretty detailed -- was there something specific there you felt was vague?

In terms of all criticism being addressed, the linked comment mentioned the repeated lang team concerns about the scope of this RFC with respect to where clauses, which have not been addressed. Given the state of both our constant evaluation system and our processing of where clauses in general, the team has a strong preference to pursue const generics in an incremental way -- first by simply having such generics, along with a minimal amount of compile-time arithmetic, but without where constraints. That should be sufficient for tackling the most pressing needs for const generics, and will give us a foundation for pursuing richer systems later. (And, again, given how much work is needed in the compiler to do any of this right now, we shouldn't get too far ahead of ourselves.)

As I mentioned in the earlier comments, the lang team is more than happy to help guide an RFC here to completion, including having a dedicated meeting to sketch out the more minimal design, but given that we want to start with a much more pared down design, and the enormous length of this comment thread already, a fresh PR with revised RFC text seems best.

---

Separately, it looks like RFC bot failed to mark this with the FCP label, which I'll add manually now.

[Ms2ger]

This link appears broken.

[dtolnay]

You need to expand some threads to find it. Here is the comment:

This error is currently reported during monomorphization, each of the arrays has acceptable size, but they cross the limit when combined together in one structure S:

struct S<T, U>(T, U);

fn f<T, U>() {
    let s: S<T, U>; // error: the type `S<[u8; 70368744177664], [u8; 70368744177664]>` is too big
}

fn main() {
    f::<[u8; 1 << 46], [u8; 1 << 46]>();
}

Overflows or division-by-zero in type level arithmetic with integer generic parameters feel very close to this situation, i.e. requiring where clauses for performing addition of two generic integers is similar to requiring where clauses for combining two generic types in a tuple like this:

struct S<T, U>(T, U) where sizeof(T) + sizeof(U) + PADDING < MAX_SIZE;

[torpak]

Wouldn't each of those arrays have terabytes of data? Who has this much ram?

[eternaleye]

@torpak: Consider mmap(2) (which allows any file to be addressed as memory), and that there are indeed array-like datasets that large.

[fottey]

This is quite possibly one of the most beautiful and well-written RFC's I have ever read. I don't know how to thank the author enough, not only for their time and hard work, but also for working so hard to make the material accessible to those without a heavy background in PL and type theory. I know I myself learned so much simply by following this RFC these past months. I have some very mixed feelings about the decision to close this RFC. My background is as a C++ programmer who has been eyeing Rust's development steadily this past year. Firstly, I understand and empathize with the language team's concerns regarding the amount of work required to implement the technical aspects of this RFC as well as their concern about its potential to impact the 2017 Roadmap. That said, I feel that the author, @ticki, really showed commitment to this RFC by attempting to address some of the language team's specific concerns in his August 10th post in this thread. Also, I feel this feature impacts a number of the 2017 Roadmap goals, though perhaps not as obviously as it first might seem.

One of the major goals I think that this feature implicitly impacts is the commitment that Rust's community should provide mentoring at all levels. I think to really scale this mentoring goal, one key element that I feel is important is that the Rust community grow. I feel that of all the various programming communities, C++ community members and Scala community members are particularly well positioned, and generally speaking, potentially most viable to be tapped to become Rust community members. Not only do these languages and Rust share methodologies and mindshare (RAII, a focus on concurrency, 'systems' programming, functional and generic programming, expressive type systems), they are all fairly complex languages. Yet I get the sense, and have seen evidence of, this general feeling from these communities that Rust isn't quite 'there' yet for various reasons. I think the addition of this feature and other type-system features would really bridge the gap in this perception and help persuade programmers and thought-leaders in those communities to engage more with Rust. I think the benefits in attracting members from these communities include not only gaining more mentors, but also include gaining more contributors to Rust and its ecosystem. I also think this feature also ties in directly and explicitly with the goals of ensuing the Rust language provides easy access to high quality crates, is well-equipped for writing robust, high-scale servers, and provides the foundation to build 1.0-level crates for essential tasks.

Another item of note: I feel like the roadmap for 2017 is focused very hard on accessibility. One thing I am unsure of is to what kind of user the language is trying to be accessible. ESR's articles on Rust have gained a lot of attention in this community recently, and I am reminded of how frustrated C++ programmers feel trying to persuade C programmers to give their language a chance. Rust is, in my opinion, not positioned well to replace C. If the C++ community has a great difficulty selling C++, which is backwards compatible with C in many ways, to C thought-leaders, how much harder must it be to sell Rust to a C thought-leader? I think selling Rust to a C++ or a Scala thought-leader is potentially a much easier sell, if it didn't include those developers feeling like they might miss features that they often love the most:

• HKTs
• Compile Time Evaluation
• Metaprogramming
• Dependent Types

While various members of the Rust community are working on all of these at the moment, I think there is a real perception from outside the Rust community, especially in the two aforementioned communities, that Rust isn't ready yet. I think the addition of this RFC could really generate a lot of interest in Rust, as this would be a very high-profile feature to thought-leaders in those communities. Just food for thought.

[newpavlov]

Maybe it's a bit late to bring this up, but I was looking forward to seeing this RFC implemented, mostly for crypto-hashes project. (to the lesser extent the same goes for block-ciphers) I don't plan to publish 1.0 versions until type-level integers get stabilized, so in my case holding off this RFC contradicts one of the 2017 roadmap goals "Rust should have 1.0-level crates for essential tasks". I think the same story will be true for numeric and scientific crates.

Currently I use generic-array crate and some other features of typenum crate, e.g. bounding values of the hash output size for given block size on the type level. So hypothetical minimal design will not help me to move from generic-array.

Also I am looking forward to be able to write conversion functions which will be able to safely and generically convert e.g. [u8; 4*N] to [u32; N] using given endiannes without any runtime costs for example in case of le conversion on le machine. This will allow to optimize code even further. (well impact of such functions will be not as big compared to SIMD stabilization, but nevertheless I think it will be very convenient and useful to have them)

[ehiggs]

@fottey I want this feature too. But because I want to use it. Not because it helps people learning Rust by giving them every feature from their current language. Going down that path is fraught with kitchen sinks and OO misfeatures.

Thought leaders will come to Rust when they see awesome software being released.

[aturon]

@fottey Thanks for sharing your thoughts.

I want to re-emphasize what I've said in the last comments: moving to close this RFC is not about rejecting this feature altogether, but about restarting discussion around a kernel proposal. In the response from @ticki that you mention, they proposed to split the RFC into separate ones, one covering the simplest mechanism needed to make const generics work, and the other layering on new where clauses. That hasn't happened yet, but it's the proposed way forward for this discussion. A fresh RFC thread will help focus discussion around the kernel proposal.

[ticki]

@fottey thanks a lot for the kind words. It has gone through a lot of iteration, and quite frankly, it was a train-wreck before feedback. This is a powerful strength of a community.

@aturon Ok, I still disagree that it is better off split up (I believe I explained why earlier in the discussion), but I'll accept it as a plan and will create new RFCs when I get time.

[aturon]

Thanks @ticki! Feel free to reach out to the lang team if you'd like to talk about the initial, minimal feature before opening a new RFC -- we'd be glad to set up a meeting or give feedback on a draft. And if you're busy, it's plausible we can find some people to help make a new draft. I'd also suggest opening just that core RFC to start with -- we should reach agreement on the core of the feature, which will take some time to implement in any case, before starting to explore significant expansions.

I'm going to go ahead and close this RFC, in anticipation of a new, more minimal proposal. Thanks all for the great discussion so far!

[iqualfragile]

I want to add, that this, at least in a simple form, which allows compile time variable sized arrays seems to be really important to the rust ecosystem, as exemplified by the reverse dependencies of the hack people have to currently use: https://crates.io/crates/generic-array/reverse_dependencies

[ticki]

generic-array is cool but it is unbelievably ugly (to be clear, I'm not blaming the authors, it's just that it needs language support to actually be convinient).

[ticki]

🎉

The new version of the RFC is here (as requested by @aturon): #1930

[jonysy]

generic-array is cool but it is..

@ticki I'm pretty sure @iqualfragile was only commenting on the usefulness of such a feature, not the design of that specific library.

I want to add, that this, at least in a simple form, which allows compile time variable sized arrays seems to be really important to the rust ecosystem...