Future Direction: Const Generics and Dispatching

At momentum, the stabilizing (not yet) feature of const generics seem to exclude const equality/const ordering or at least allows them to some minor extent, for good reasons.

My interest would go after this as described by the RFC Section Specialization on Const Parameters

Although the mentioned example is quite interesting, generalizing to include the full semantic of equality and order leads to undecidable type checking, for example:

fn fun<T:Comparable>(x:T, y:T) where x<y
fn fun<T:Comparable>(x:T, y:T) where x<=y

To get the former method preferred when applying fun to x,y, you are required to compare <=, < either by traversing all relation members (this is undecidable for T with infinite members) or you prove the code given the where signatures.

The latter requires understanding semantics usually expressed over higher order logic (HOL), e.g. for describing reflexivity, symmetry and transitivity.

Beside that some cases are decidable and could be inferred in reasonable time, others are not, i.e. typechecking becomes undecidable.

So what is the future direction to go with specialization?

I've heard from @oli-obk that specialization is disregarded at momentum for const generics, i.e. two trait methods with the signature except for different const value expressions are deemed to be (possibly) equal resulting into an error?

Is the target to allow const expr in trait methods with decidable semantic specialization or is it generally possible to formulate undecidable problems. When, how to tackle them in the right way? Writing own proofs or change the dispatch behavior in the undecidable case and when is a const expr known to be undecidable regarding order, i.e. how many scenarios have to be enumerated to exclude any undecidable case?

Another approach coming from D is to treat relations of any kind (this includes all operators, functions too) as simple propositions such that ==(x,x^2+1) becomes substituted to ==(x,y), the former known to be false for every x, the latter may include the possibility that x==y because we have no semantic meaning of ops like ^,+ .

It means these two functions are possibly equal:

fn fun<T:Comparable>(x:T, y:T) where x<y
fn fun<T:Comparable>(x:T, y:T) where x<=y

Therefore, it will be rejected by the compiler considering only propositions. It can, however, be alleviated with the following rewrite:

fn fun<T:Comparable>(x:T, y:T) where x<y
fn fun<T:Comparable>(x:T, y:T) where x<=y && not(x<y)

Is a bit more nasty to write that and it doesn't scale that much, but it is at least manually possible and you can control the way it dispatches. Imagine that semantic dispatching even when decidable can take a while to compute, dispatching over propositions is much faster and has the advantage to be decidable.

Would this be a reasonable approach for Rust, too or can we expect a mix of semantic vs propositional dispatching.

1 Like
default fn fun<T:Comparable>(x:T, y:T) where x<=y
fn fun<T:Comparable>(x:T, y:T) where x<=y && not(x==y)

seems the most likely to me and is something which I expect to be somewhat straightforward.

I personally would maybe allow reasoning about inductive datatypes, meaning that

(3, U) can specialize (T, U) and Foo { v: 3, u: N + 1 } can specialize Foo { v: M, u: N + 1 }

This would also allow for the following:

trait Foo<const V: Option<usize>> { fn test() {} }

impl<const N: usize> Foo<{ Some(N) }> for () {}

imp Foo<None> for () {
    fn test() {
        println!("I am none");
    }
}

Also, like I said on github, I am mostly concerned with getting the simple version to work correctly before I even think to deeply about any of this though.

1 Like

A solution based on specialization has a lot of problems:

  • It's highly nonintuitive, especially if there are more cases than two.
  • In some cases we may want to use associated types, but default type prevents the compiler from resolving associated type projections to concrete types in some cases – an unnecessary limitation.
  • Also, specialization currently has no path to stabilization at all, except for min_specialization, which would not work for this.

I wish we had something like if constexpr...

1 Like

Did you suggest some kind of static if or to what exactly did you refer to?

default fn fun<T:Comparable>(x:T, y:T) where x<=y
fn fun<T:Comparable>(x:T, y:T) where x<=y && not(x==y)

Note that stuff like this should probably get written as

fn fun<T:Comparable>(x:T, y:T) where x<=y`{
    if x == y {
        // whatever
    } else {
        // whatever
    }
}

you can specialize on const expressions by branching on their value.

2 Likes

Is this not

#![feature(inline_const)]

if const { true } {
    ...
}

Isn't if constexpr in C++ a way to make the compiler discard one of the branches depending on the condition, to enable weird duck-typing conditional compilation based on the template arguments? I don't think this can apply in any way to Rust code.

The proposed if consteval in C++ which would allow conditional compilation depending on if we are currently executing in a const context or not could be feasible, but... that is also a real can of worms.

1 Like

Other question: Would it be possible to call/instantiate C++ templates constrained by concepts and constraints in a safe/compatible manner? I mean, additionally calling C++ logic over the ABI, it could also be possible to use C++ logic over the ASI (Application Source Interface) / or ATI (Application Template Interface), don't know.

While I'd love to see a project to integrate rustc with a C++ compiler for better FFI, it's definitely not on topic in this thread.