Addition does not commute in generic_const_exprs

[WalterSmuts]

I tried this code:

#![allow(incomplete_features)]
#![feature(generic_const_exprs)]

// Works!
pub fn append<T: Default, const SIZE: usize>(input: [T; SIZE]) -> [T; SIZE + 1] {
    concat(input, [T::default()])
}

// Fails to compile...
pub fn prepend<T: Default, const SIZE: usize>(input: [T; SIZE]) -> [T; SIZE + 1] {
    concat([T::default()], input)
}

pub fn concat<T, const M: usize, const N: usize>(_: [T; M], _: [T; N]) -> [T; M + N] {
    unimplemented!()
}

I expected that both append and prepend would compile because they evaluate to the same expression.

Instead, I realise that addition does not commute and that you can switch which implementation does not compile by switching N and M.

I realise that generic_const_exprs is still unstable. Just thought I'd add it here for visibility and perhaps to illicit a workaround. It's currently blocking array_append from being used ergonomically.

Meta

$ rustc --version --verbose
rustc 1.65.0-nightly (eaadb8947 2022-08-27)
binary: rustc
commit-hash: eaadb8947b850a025404082f6297766c4680a42a
commit-date: 2022-08-27
host: x86_64-unknown-linux-gnu
release: 1.65.0-nightly
LLVM version: 15.0.0

[asquared31415]

Here's an example that very clearly shows the shortcoming and the error is much more obvious what's going wrong:

#![allow(incomplete_features)]
#![feature(generic_const_exprs)]

pub fn identity_but_flipped<const N: usize, const M: usize>(val: [(); N + M]) -> [(); M + N] {
    val
}

(playground)

Errors with (nightly 2022-09-14)

error[E0308]: mismatched types
 --> src/lib.rs:5:5
  |
5 |     val
  |     ^^^ expected `M + N`, found `N + M`
  |
  = note: expected constant `M + N`
             found constant `N + M`

[asquared31415]

@rustbot label +A-const-generics

[workingjubilee]

...Technically it is indeed the case that addition is not commutative by default in Rust due to the quirks of how std::ops::Add works. (obviously the compiler can "just" prove that it would be in this case, however)

[fmease]

CC: This Reddit comment of mine. Inlined:

I'm not quite in the loop wrt evaluatable bounds, I know that there were some syntax proposals like const { N } (e.g. here) but I think I've also seen some more sophisticated ideas being thrown around which sadly I don't remember or can't link to.

Right now, const equality (which is required under the hood to solve those bounds) is fairly primitive as it's mostly syntactic (after having evaluated the consts beforehand of course) which is not a bad thing per se – that's how most dependently-typed languages are implemented at their core – however without more tools or tricks provided by the language, it gets painful very quickly. E.g. N + M is not considered (definitionally, judgementally) equal to M + N (where N and M are const parameters) in Rust or in most dependently typed languages.

In the latter however, the user can write proofs for the commutativity of addition (and the standard library can provide a standard definition) and make them (propositionally) equal. In Rust, however, you just can't do that and I doubt it's ever coming.

Maybe Rust is gonna ship with some “common” laws but that's not gonna cut it. Alternatively, requiring the usage of an SMT solver like Z3 to type-check your program (which is what some? all? type checkers of languages with refinement types use), I don't think anybody wants that. So the future is relatively unclear.

Addendum: I like to compare this topic to dependently typed languages and their implementations since they're quite related.