# Const arguments **URL:** \ **Category:** language design\ **Created:** [June 27, 2018, 12:22pm UTC](https://internals.rust-lang.org/t/const-arguments/7811 "2018-06-27T12:22:57Z")\ **Posts on this page:** 20\ **Page:** 1
**Author:** ![Soni](https://avatars.discourse-cdn.com/v4/letter/s/a3d4f5/32.png) [@Soni](https://internals.rust-lang.org/u/Soni)\ **Post date:** [June 27, 2018, 12:22pm UTC](https://internals.rust-lang.org/t/const-arguments/7811/1 "2018-06-27T12:22:57Z")
I would like to be able to ```rust fn f(const notify: bool) { if notify { send_notification(); } do_things(); } ``` ---
**Author:** ![newpavlov](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/newpavlov/32/3290_2.png) [@newpavlov](https://internals.rust-lang.org/u/newpavlov)\ **Post date:** [June 27, 2018, 12:52pm UTC](https://internals.rust-lang.org/t/const-arguments/7811/2 "2018-06-27T12:52:54Z")
I would very much like to see this functionality as well, especially in the context of SIMD. See this thread for discussions: > [@pre-RFC \`const\` function arguments](https://internals.rust-lang.org/t/pre-rfc-const-function-arguments/6709): > > This is a rough draft to get the discussion started. (TODO: this needs to be more precise with respect to the terminology, in particular the technical terms const variables, const parameters, const expression, const projection, etc. should all be used correctly here) Summary This RFC allows const to be used in function argument position. This RFC does not propose an alternative syntax to the [RFC2000: const generics](https://github.com/rust-lang/rfcs/pull/2000), but rather builds upon it to improve ergonomics in some situations. [RFC2000: c…](https://github.com/rust-lang/rfcs/pull/2000) ---
**Author:** ![jjpe](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/jjpe/32/9779_2.png) [@jjpe](https://internals.rust-lang.org/u/jjpe)\ **Post date:** [June 28, 2018, 1:28pm UTC](https://internals.rust-lang.org/t/const-arguments/7811/3 "2018-06-28T13:28:49Z")
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`? ---
**Author:** ![fbstj](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/fbstj/32/424_2.png) [@fbstj](https://internals.rust-lang.org/u/fbstj)\ **Post date:** [June 28, 2018, 1:44pm UTC](https://internals.rust-lang.org/t/const-arguments/7811/4 "2018-06-28T13:44:35Z")
my understanding was that it was mostly an alternative formulation around ‘const generic parameters’ such as `fn foo() {}` which would be an equivalent to the OP unless I’m missing something ---
**Author:** ![mcy](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/mcy/32/6512_2.png) [@mcy](https://internals.rust-lang.org/u/mcy)\ **Post date:** [June 28, 2018, 5:41pm UTC](https://internals.rust-lang.org/t/const-arguments/7811/5 "2018-06-28T17:41:23Z")
> [@fbstj](#): > > my understanding was that it was mostly an alternative formulation around ‘const generic parameters’ such as `fn foo() {}` 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. ---
**Author:** ![Centril](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/centril/32/3334_2.png) [@Centril](https://internals.rust-lang.org/u/Centril)\ **Post date:** [June 28, 2018, 10:14pm UTC](https://internals.rust-lang.org/t/const-arguments/7811/6 "2018-06-28T22:14:22Z")
> [@mcy](#): > > 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, `` vs. `(const N: usize)` should be seen as _implicit arguments_ ([Agda](http://agda.readthedocs.io/en/v2.5.3/language/implicit-arguments.html), [Idris](http://docs.idris-lang.org/en/latest/tutorial/miscellany.html#implicit-arguments), ..) 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: ```rust fn repeat(T: type, vec: Vec) -> 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.): ```rust repeat : Π (T: type) → Π (vec: Vec T) → usize ``` in some dependent type theory. ---
**Author:** ![newpavlov](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/newpavlov/32/3290_2.png) [@newpavlov](https://internals.rust-lang.org/u/newpavlov)\ **Post date:** [June 28, 2018, 10:42pm UTC](https://internals.rust-lang.org/t/const-arguments/7811/7 "2018-06-28T22:42:16Z")
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. ---
**Author:** ![Centril](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/centril/32/3334_2.png) [@Centril](https://internals.rust-lang.org/u/Centril)\ **Post date:** [June 28, 2018, 10:50pm UTC](https://internals.rust-lang.org/t/const-arguments/7811/8 "2018-06-28T22:50:36Z")
> [@newpavlov](#): > > 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: ```rust fn foo(const N: usize) -> Foo // 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`, but it is an inferrable parameter). ---
**Author:** ![newpavlov](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/newpavlov/32/3290_2.png) [@newpavlov](https://internals.rust-lang.org/u/newpavlov)\ **Post date:** [June 28, 2018, 11:00pm UTC](https://internals.rust-lang.org/t/const-arguments/7811/9 "2018-06-28T23:00:13Z")
I meant in the mental model which can be a bit imprecise, but gets stuff done. For example: ```rust 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): ```rust 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::(10, 3); ``` It is just about expectations, in function arguments you expect values, not types. And breaking this expectation will cause a substantial dissonance. ---
**Author:** ![Centril](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/centril/32/3334_2.png) [@Centril](https://internals.rust-lang.org/u/Centril)\ **Post date:** [June 28, 2018, 11:13pm UTC](https://internals.rust-lang.org/t/const-arguments/7811/10 "2018-06-28T23:13:21Z")
I think the notion that you can add dependent types without changing / expanding the mental model is mistaken personally. > [@newpavlov](#): > > ```rust > 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: ```rust fn create_2d_array() -> [[u32; columns]; rows] { .. } let foo = create_2d_array(); // Sizes are inferred. ``` > [@newpavlov](#): > > ```rust > // 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`. > [@newpavlov](#): > > 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 ``, and permitting `` 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. ---
**Author:** ![mcy](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/mcy/32/6512_2.png) [@mcy](https://internals.rust-lang.org/u/mcy)\ **Post date:** [June 29, 2018, 4:21am UTC](https://internals.rust-lang.org/t/const-arguments/7811/11 "2018-06-29T04:21:30Z")
So, it’s not just a human expectation that only types appear in `<>`, but the parser expects it, too. Allowing something like ```rust 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. ---
**Author:** ![Centril](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/centril/32/3334_2.png) [@Centril](https://internals.rust-lang.org/u/Centril)\ **Post date:** [June 29, 2018, 4:33am UTC](https://internals.rust-lang.org/t/const-arguments/7811/12 "2018-06-29T04:33:33Z")
> [@mcy](#): > > 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. > [@mcy](#): > > 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: ```rust fn foo(elt: T) -> Vec<{n}, T> { .. } ``` then that clearly does not hold anymore. ---
**Author:** ![mcy](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/mcy/32/6512_2.png) [@mcy](https://internals.rust-lang.org/u/mcy)\ **Post date:** [June 29, 2018, 4:45am UTC](https://internals.rust-lang.org/t/const-arguments/7811/13 "2018-06-29T04:45:21Z")
> [@Centril](#): > > 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). ---
**Author:** ![Centril](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/centril/32/3334_2.png) [@Centril](https://internals.rust-lang.org/u/Centril)\ **Post date:** [June 29, 2018, 5:11am UTC](https://internals.rust-lang.org/t/const-arguments/7811/14 "2018-06-29T05:11:07Z")
> [@mcy](#): > > 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 `<..>`). > [@mcy](#): > > 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: ```rust let first: Vector = mk_vector_1(); // Length is some runtime value N. let second: Vector = 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 // The arguments lhs and rhs constrain N and M fully. (lhs: Vector, rhs: Vector) -> Vector { .. } ``` > [@mcy](#): > > 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](http://agda.readthedocs.io/en/v2.5.3/language/implicit-arguments.html) 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 `` you also essentially have implicit arguments at the term level. What makes run-time values so special? ---
**Author:** ![mcy](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/mcy/32/6512_2.png) [@mcy](https://internals.rust-lang.org/u/mcy)\ **Post date:** [June 29, 2018, 6:03am UTC](https://internals.rust-lang.org/t/const-arguments/7811/15 "2018-06-29T06:03:13Z")
> [@Centril](#): > > 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. > [@Centril](#): > > 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. ---
**Author:** ![Centril](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/centril/32/3334_2.png) [@Centril](https://internals.rust-lang.org/u/Centril)\ **Post date:** [June 29, 2018, 6:36am UTC](https://internals.rust-lang.org/t/const-arguments/7811/16 "2018-06-29T06:36:57Z")
> [@mcy](#): > > 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. > [@mcy](#): > > 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). > [@mcy](#): > > 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. > [@mcy](#): > > 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. > [@mcy](#): > > 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. > [@mcy](#): > > 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". > [@mcy](#): > > 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. > [@mcy](#): > > - 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.. ---
**Author:** ![leonardo](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/leonardo/32/1344_2.png) [@leonardo](https://internals.rust-lang.org/u/leonardo)\ **Post date:** [June 29, 2018, 7:24am UTC](https://internals.rust-lang.org/t/const-arguments/7811/17 "2018-06-29T07:24:21Z")
> [@Centril](#): > > I think the notion that you can add dependent types without changing / expanding the mental model is mistaken personally. Quote of the week? 🙂 ---
**Author:** ![Centril](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/centril/32/3334_2.png) [@Centril](https://internals.rust-lang.org/u/Centril)\ **Post date:** [June 29, 2018, 7:36am UTC](https://internals.rust-lang.org/t/const-arguments/7811/18 "2018-06-29T07:36:43Z")
> [@leonardo](#): > > Quote of the week? 🙂 Feel free, hehe. Aren't QotWs supposed to be jokes? 😉 ---
**Author:** ![Soni](https://avatars.discourse-cdn.com/v4/letter/s/a3d4f5/32.png) [@Soni](https://internals.rust-lang.org/u/Soni)\ **Post date:** [June 29, 2018, 12:11pm UTC](https://internals.rust-lang.org/t/const-arguments/7811/19 "2018-06-29T12:11:11Z")
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. ---
**Author:** ![oli-obk](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/oli-obk/32/3168_2.png) [@oli-obk](https://internals.rust-lang.org/u/oli-obk)\ **Post date:** [June 29, 2018, 12:51pm UTC](https://internals.rust-lang.org/t/const-arguments/7811/20 "2018-06-29T12:51:08Z")
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? [Next page](https://internals.rust-lang.org/t/const-arguments/7811.md?page=2)