Const arguments

I would like to be able to

fn f(const notify: bool) {
    if notify {
        send_notification();
    }
    do_things();
}
1 Like

I would very much like to see this functionality as well, especially in the context of SIMD. See this thread for discussions:

So if I understand this correctly, it means that it would become possible to define a function that accepts an arg that must be const?

my understanding was that it was mostly an alternative formulation around ā€˜const generic parametersā€™ such as fn foo<const notify: bool>() {} which would be an equivalent to the OP unless Iā€™m missing something

Not quite: this form would explicitly opt them out of any sort inference and ban them from appearing in where clauses.

The first part of your sentence seems right. Why would it ban them in where clauses?

I think that essentially, <const N: usize> vs. (const N: usize) should be seen as implicit arguments (Agda, Idris, ..) vs. explicit arguments where the former is inferrable and the latter is not and must always be specified.

I think it is fine to have (const N: usize), but then I'd like to have explicit argument quantification of type variables to have more symmetry in the type system. So you should also be allowed to write:

fn repeat(T: type, vec: Vec<T>) -> usize { .. }

3 == foo(&'static str, vec!["foo", "bar", "baz"); // OK.
3 == foo::<&'static str>(vec!["foo", "bar", "baz"); // ERROR.
3 == foo(vec!["foo", "bar", "baz"); // ERROR.

This very roughly translates to (ignoring const-ness, currying, etc.):

repeat : Ī  (T: type) ā†’ Ī  (vec: Vec T) ā†’ usize

in some dependent type theory.

Ehmā€¦ Your proposal is elegant from theoretical point of view, but I think will be confusing as hell for most of programmers. const val: T works nicely because itā€™s ā€œjust a function argumentā€ with an additional constancy constraint, it easily fits into existing mental model regarding how functions work.

5 Likes

But it is not. It differs vastly in that it involves dependent quantification:

fn foo(const N: usize)
    -> Foo<N> // The dependency here is the important bit.
{ .. }

I think if anything, T: type clarifies that T is a parameter to foo (which also happens when you write foo<T>, but it is an inferrable parameter).

I meant in the mental model which can be a bit imprecise, but gets stuff done. For example:

fn create_2d_array(const columns: usize, const rows: usize)
    -> [[u32; columns]; rows] { .. }

// well, looks nice and clear!
// Some even can forget about const sizes of the array for a moment.
let foo = create_2d_array(10, 3);

Feels quite natural. While this snippet will be quite confusing (at least for me):

fn create_2d_array(T: type, const columns: usize, const rows: usize)
    -> [[T; columns]; rows] { .. }

// ehm.. is `f32` a typo? shouldn't it be `0f32` or something?
let foo = create_2d_array(f32, 10, 3);
// this would have been much better, even considering turbofish
let foo = create_2d_array::<f32>(10, 3);

It is just about expectations, in function arguments you expect values, not types. And breaking this expectation will cause a substantial dissonance.

1 Like

I think the notion that you can add dependent types without changing / expanding the mental model is mistaken personally.

Even better:

fn create_2d_array<const columns: usize, const rows: usize>()
    -> [[u32; columns]; rows] { .. }

let foo = create_2d_array(); // Sizes are inferred.

Clearly that can't be true. The function signature explicitly states that T is a type.

I think similarly there is an expectation that you only have types (and lifetimes) in <T, ..>, and permitting <const N: usize> breaks that by allowing values within <..>. My view is that both expectations need to be adjusted once you're in a (const) dependently typed language.

1 Like

So, itā€™s not just a human expectation that only types appear in <>, but the parser expects it, too. Allowing something like

expr `(` ty `)`

would confuse the hell out of the parser. How do I parse f(&x)? Is this f-of-address-of-x or f-of-reference-to-x-with-lifetime-'_? The correct parse depends on the definition of f, and now Rust is no longer context free (ok Rust isnā€™t context free but thatā€™s for hilarious reasons related to raw strings that arenā€™t nearly as bad). I really think Rust should avoid a situation where the parser needs to be aware of the semantics of Rust (outside of raw string hilarity, of course).

I do think that the expectation that things in <> being types is flawed; rather, the expectation is that the contents of <> be known at compile time, and the contents of () be known at runtime. The reason types and lifetimes can only live in the angle brackets is because they are a compiler fiction: the CPU cares not for types (much less for lifetimes) beyond their width.

While const type arguments seems like an ergonomic win, it breaks this very tidy call-site mnemonic.

1 Like

That's a good point. Dependently typed languages usually solve this by unifying the syntax at the term and type levels (types are just terms...). f(&x) is indeed a problem. You would need to insert something to disambiguate, which makes it less pleasant. This is essentially what we did with const generics by forcing you to write Vec<{expr}, ..> in certain circumstances.

Even that is problematic. If we at some point add inferrable run-time-value-dependent types, like:

fn foo<T: Clone, n: usize>(elt: T) -> Vec<{n}, T> { .. }

then that clearly does not hold anymore.

1 Like

Yes, but this expectation holds today, and I think breaking that expectation is a very, very bad idea. What would runtime value inference even look like? This sounds a lot like Scala's implicit arguments, which I believe are a misfeature that makes for hard-to-read code (and, as well all know, code is read far more often than it is written).

1 Like

It has never been my expectation. I've always seen the stuff inside <..> as stuff that can be inferred (which holds today, and would also hold with run-time values in <..>).

The basic idea is that it would be like for const N: usize but at runtime. Something like this:

let first: Vector<u8, _> = mk_vector_1(); // Length is some runtime value N.
let second: Vector<u8, _> = mk_vector_2(); // Length is some runtime value M.
let appended = append(first, second);  // Length has to be N + M, there is no choice.

fn append<T, N: usize, M: usize>
    // The arguments lhs and rhs constrain N and M fully.
    (lhs: Vector<T, N>, rhs: Vector<T, M>)
    -> Vector<T, {N + M}>
{ .. }

I've never used Scala. But in Agda or Idris, you wouldn't want to be without implicit arguments when you are proving arbitrary properties about your code. It would get immensely verbose, repeating redundant information that the compiler already knows. So it would get old very quickly. If you want to get a feel for how implicit arguments work in a dependently typed language, try one of those languages.

In fact, I'd say that Rust essentially has implicit arguments for types and with <const N: usize> you also essentially have implicit arguments at the term level. What makes run-time values so special?

1 Like

While I have written very little in such languages, I've read enough proof assistant code to know that the resulting it is very unpleasant to decode unless I'm carrying around a sophisticated typeck in my head... which is a mental overhead that I should only need when writing code, not reading it. In contrast, I run borrowck in my head when writing Rust, but never to read it.

I think it comes down to a matter of taste. I think that inference is a powerful but dangerous tool that can make writing code better but reading it worse. Having written a lot of code in inference-heavy languages, I think that it is very useful for simple tasks, and being able to encode complicated invariants in the type system is desirable, to stop yourself from shooting yourself in your own foot. However, becoming reliant on the compiler to figure out what you should be writing down can lead to extreme overuse of inference, producing unreadable programs an inscrutable error messages... look no further than the overuse of template metaprogramming in C++, which style guides like Google C++ strongly discourage.

I like to be conservative when it comes to how much inference should be allowed. Rust is already on its way to allowing as much inference as C++ does (backflowing type inference in function bodies is the only kind of inference Rust has that C++ doesn't, but I think that isn't actively harmful right now), and I don't think I'm alone in feeling that Rust should be learning from C++'s mistakes.

Finally, I do not think it is a win to add formal verification facilities to Rust (at least, in the next 10 to 15 years), for a few reasons:

  • For this to be of any actual value, we (or someone else) would need to formally verify both LLVM and rustc, both Herculean undertakings.
  • We would also need to formally verify all uses of unsafe in std as well (easier).
  • You would only be able to depend on crates which are formally verified.
  • We would need to figure out how to teach formal verification in the context of Rust, which I think is truly beyond the scope of most engineers working on systems code. My background is algebraic topology, and even with that I've found learning formal verification very difficult.
2 Likes

I've personally never felt the need to do any sort of heavyweight mental type checking. Most of the inference done by proof assistants such as Agda and Idris feels pretty straight forward and obvious most of the time to me. If you remove the inference, it feels harder to read.

Sure; That is why I always use global type inference in Haskell exclusively as a development aid, but end up committing small functions with type signatures on them even if I could leave them out. So I think what is really important is type signatures on functions.

Inference is best when it removes things that you can easily infer yourself from the context (as in my snippet above).

I would say we are pretty reliant on the compiler in Rust today, getting great error messages about borrows and such. With Agda and Idris, you even have interactive modes where you can essentially let the compiler write the program for you. What is important then is the type signature. If the signature specifies enough, then you don't really need to look at the body of functions.

I believe C++'s error messages are uniquely bad because it is template metaprogramming, that is: it is macro based.. and substitution failures are not errors. I don't think error messages are anything like that in the proof assistants.

I think it is mistaken to say that just because we can't verify 100%, doesn't mean we can't gain a lot more confidence by employing some formal verification. After all, Agda and such languages have JavaScript backends, so then you have to trust the JavaScript engines... So should we give up on formal verification then?

Furthermore, you usually don't verify the entire compiler. Idris for example is written in Haskell. What is proved (sometimes not even mechanically verified) is the soundness of the proof kernel, which is usually a much smaller part.

It would be good to do so, but it is not strictly necessary. unsafe { .. } can essentially be seen as "this part of the proof has been done on paper or in my brain".

I disagree. You can formally verify things or specify your invariants more precisely in the small. You don't have to verify every single part of your program for it to be useful. Do it where it matters most. This is how the type system is used even today. Some APIs are more stringly, some are more type safe.

Some basic stuff could and should be taught yes. We need to advance the teaching in this area for sure. However, it is not so much formal verification that needs teaching, but rather dependent types.

Finally I would say that I'm not advocating we rush to add run-time-dependent types to Rust. It should take its time. We already have a long backlog of other features to implement and ship. The research into dependent types in Rust also needs to be done. It is not something you just add without scientific research before.

That said, we have already started to add some more formal verification facilities with const generics, GATs, etc..

Quote of the week? :slight_smile:

Feel free, hehe.

Aren't QotWs supposed to be jokes? :wink:

I just want it as plain arguments that are const-checked, to help catch bugs.

No relation to const generics, really. You shouldnā€™t be able to (directly) construct an array with them.

This could be relaxed once const generics exist.

2 Likes

We do have a compiler-internal scheme for something like this for SIMD shuffle. But I think the tenor around that code is ā€œFIXME: remove once const generics are a thingā€.

Adding these checks properly is probably just as much work as adding a form of const generics that allow us to only use the constants in runtime situations. So maybe that should be the proposal?