Const arguments

[drXor]

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.

[Centril]

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.

[newpavlov]

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.

[Centril]

because it’s “just a function argument” with an additional constancy constraint

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

[newpavlov]

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.

[Centril]

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

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);

Even better:

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

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

// ehm.. is `f32` a typo? shouldn't it be `0f32` or something?

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

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

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.

[drXor]

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.

[Centril]

would confuse the hell out of the parser.

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.

rather, the expectation is that the contents of <> be known at compile time , and the contents of () be known at runtime

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.

[drXor]

If we at some point add inferrable run-time-value-dependent types

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

[Centril]

Yes, but this expectation holds today, and I think breaking that expectation is a very, very bad idea.

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

What would runtime value inference even look like?

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}>
{ .. }

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

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?

[drXor]

But in Agda or Idris

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.

What makes run-time values so special?

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.

[Centril]

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

I think that inference is a powerful but dangerous tool that can make writing code better but reading it worse.

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

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…

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.

an inscrutable error messages… look no further than the overuse of template metaprogramming in C++, which style guides like Google C++ strongly discourage.

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.

For this to be of any actual value, we (or someone else) would need to formally verify both LLVM and rustc, both Herculean undertakings.

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.

We would also need to formally verify all uses of unsafe in std as well (easier).

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

You would only be able to depend on crates which are formally verified.

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.

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

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…

[leonardo]

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

Quote of the week?

[Centril]

Quote of the week?

Feel free, hehe.

Aren’t QotWs supposed to be jokes?

[Soni]

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.

[oli-obk]

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?

[Soni]

the idea is to use this as a stepping stone for const generics

[Ixrec]

Simultaneous Art from C++: http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p1045r0.html

[Soni]

basically I want a very simple and very limited form of const generics.

They’d only work in functions. they’d only be const-checked when calling the function, but inside the function it’d be treated like a non-const as far as everything is concerned. This is extremely limited, but compatible with const generics, so if we do get const generics we can then “fix” this, and make it work like const generics.

It would be a stepping stone for const generics, and would introduce an useful behavior - erroring if an argument isn’t const. It may not seem very useful but it really is. I’m working on some code that uses an argument to emit notifications, and we expect the argument to be fixed at compile-time.

Note that “const mut” would NOT be available, as that would be incompatible with const generics.

[system]

This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.