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.