I'm perhaps an oddball, but dependent types interest me deeply
Naturally "need" is a subjective matter, but I would note a few things:
Just because you have dependent types does not mean you must use them everywhere; you can use them in the parts of your code where it is most natural and where it is most important to prove properties about your program behavior.
If you already specify QuickCheck properties about your code, the step to dependent types is natural as you've already specified invariants to some degree.
With any advanced type-system feature you'll get increased compile times, but only if you use the features so you pay for what you use. You can already do a bunch of type hackery with traits and such, but with dependent types, these are expressed more naturally.
As for binary bloat, I think you can avoid that if you avoid monomorphization, and I detailed how this could be avoided. Where it comes to functions such as fn replicate(length: usize, elem: Foo) -> Vec<Foo, {length}> {..} this should be zero cost in the sense that you couldn't have hand-written better code. When the values are known at compile time, the compiler should be able to use this information to optimize further.
Languages like Ada have refinement typing and it is used in industry for safety critical applications (c.f. aerospace). I think the notion of upping our ability to give more fine-grained guarantees jives well with Rust's overall focus on correctness and safety.
The snippet you wrote brings a few questions to front. First, it seems to me that writing Foo<a>::new() immutably borrows (or moves) a until u is no longer out of scope. v should do the same thing. I think therefore that a.modify(); must be rejected unless typeof(a): Copy. It further occurs to me that a may have no interior mutability. It is highly non-trivial to integrate linear types or region-typing with runtime-value-dependent types. Neel Krishnaswami discusses this wrt. linear types in a lecture series, https://www.youtube.com/watch?v=5i3YDgQyIwE. Still, even if we impose these restrictions, a whole bunch of types are Copy or do not have interior mutability.
I think we can more or less regain your use-case here by having some a.token() which is initialized when a is constructed and then even if you do modify a, the token stays the same. Thus we have:
let token = a.token();
let u = Foo<{token}>::new();
a.modify();
let v = Foo<{token}>::new();
let equal = v == u; // valid
Not necessarily. It may be desirable to borrow in some case (or even possibly to move a) but it does not have to be either mandatory or even the default case. The minimal semantics are just that u and v are somehow related to a. More specifically u and v may be used together as parameters of certain functions only because their types match (=i.e. they are related to the same a). This naturally implies that:
a must be specified when u and v are created ;
neither u nor v can outlive a.
But that does not mean that the value of a needs to be used anywhere in functions that consumes items of types Foo<a>. And even when such value is actually needed, the borrow can perfectly start when the function is called, not when u is created. Certainly a dedicated syntax would be necessary to specify which behavior is intended.
Let's imagine something like this (the syntax proposed here is cumbersome and ugly, but let's agree this is not the point):
// a is not used anywhere inside bar_tag
fn bar_tag<let a: MyContext>(u: &Foo<a>, v: &Foo<a>) { … }
// a is borrowed when calling bar_ref
fn bar_ref<let ref a: MyContext>(u: &Foo<a>, v: &Foo<a>) { … }
// a is mutably borrowed when calling bar_ref
fn bar_mut<let mut ref a: MyContext>(u: &Foo<a>, v: &Foo<a>) { … }
…
let a : MyContext = …
let u = Foo::<a>::new( … );
let v = Foo::<a>::new( … );
// a is not borrowed when we reach this point
bar_tag(u, v); // u and v are borrowed at this point but a is not impacted
bar_ref(u, v); // a is immutably borrowed here
// ... and released here
bar_mut(u, v); // ... and reborrowed mutably here
// but neither u not v can outlive a
An interesting aspect is that u and v do not necessarily have to carry any internal reference to a (that would require a to be locked). However they do represent data that may only be interpreted in the light of a (sometimes the actual value of a is required, sometimes we just need to know that it is the same a, independently of its actual value). Of course you may also want to borrow a from the start (when u or v are created) but this can be handled independently by lifetimes.
That may work indeed, although it requires that token() copies some information.
It seems to me that if we have dependent types (with unification), when you want to ensure that u and v are related to the same a, you must prevent a from having been modified in-between.
This is because I'm imagining that you would be able to use a inside bar_tag and that the language does not prevent this. Your snippet is interesting; I'll have to think it over some more.
Sure; but I would like to have sigma types in the language as well; and then you could carry an internal reference to a.
True; hopefully the compiler is smart enough to optimize away when it realizes that it is just a constant value used the same way in both places. But since compiler optimization is black magic, you never know.
Bluss has written a very nice indexing library that uses a lifetime, 'id, to express that an index Index<'id> belongs to a the static interval Range<'id, P>. In other words the lifetime acts as a kind of type level reference from the index to the range.
I don’t know if this approach can be tailored to solve your problem, and it may get annoying to have lifetimes in all structs, but have a look.
