In the PLT literature this is called (proof) erasure. In the talk “Type inference needs a revolution” Conor McBride talks about that and Milner’s coincidence.
More: http://staff.computing.dundee.ac.uk/frantisekfarka/tiap/#conor. There’s also a paper on erasure in Idris, which tries to erase proofs quite agressively, that might interest you: Practical Erasure in Dependently Typed Languages.
We can reinterpret (for the purposes of understanding the mechanics, not how you write it down syntactically):
fn foo(n: usize, m: usize) -> usize
where predicate(n, m) {
...
}
as the following:
fn foo<proof: predicate(n, m) == true>(n: usize, m: usize) -> usize {
...
}
In other words, there is a sort of implicit argument of type predicate(n, m) == true where == is the type constructor for propositional equality which is inhabited if and only if a and b are the same type. The compiler will try to construct a proof of this fact for you automatically when you try to call foo(x, y). In many ways, this is similar to what the compiler does for traits and their implementations.
I should note however that this is not an easy problem, and significant thinking / research will be needed to make this happen proficiently. But if it can be done well in Rust, it would be quite wonderful. It should also be noted that unlike Idris, Agda, etc. which are based on Intuitionistic logic, Rust is not. The affine nature (or to simplify a lot: linear nature) of Rust’s type system makes it difficult for dependent types. Neel Krishnaswami talks about this in a lecture series on Linear and Dependent types and McBride talks about it in a talk about “Worldly type systems + Linear dependent types”.
In Idris, we can encode foo by writing:
// Propositional equality, poly kinded:
data (=) : a -> b -> Type where
Refl : x = x
foo : {auto proof : Predicate(n, m) = True}
-> (n : Nat) -> (m : Nat) -> Nat
foo n m = the_body_of_foo
The thing inside { .. } is an implicit argument, which means that if the compiler can infer it from the surrounding context, we don’t have to specify it. For example take:
data Vec : (len : Nat) -> (elem : Type) -> Type where
Nil : Vec Z elem
(::) : (x : elem) -> (xs : Vect len elem) -> Vect (S len) elem
// which is really:
data Vec : (len : Nat) -> (elem : Type) -> Type where
Nil : {elem : Type} -> Vec Z elem
(::) : {elem : Type} -> {len : Nat}
-> (x : elem) -> (xs : Vec len elem) -> Vec (S len) elem
// Adding two vectors together, we know their lengths from the vectors themselves, so they can be implicit:
add : {n : Nat} -> {m : Nat} -> Vec n Color -> Vec m Color -> Vec (n + m) Color
add vec_a vec_b = ...
// or just:
add : Vec n Color -> Vec m Color -> Vec (n + m) Color
add vec_a vec_b = ...
The auto keyword will tell Idris to try and construct the proof for us automatically.
