# Variable dependent types? **URL:** \ **Category:** language design\ **Created:** [July 25, 2018, 8:27pm UTC](https://internals.rust-lang.org/t/variable-dependent-types/8064 "2018-07-25T20:27:04Z")\ **Posts on this page:** 5\ **Page:** 2
**Author:** ![Centril](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/centril/32/3334_2.png) [@Centril](https://internals.rust-lang.org/u/Centril)\ **Post date:** [August 4, 2018, 1:03am UTC](https://internals.rust-lang.org/t/variable-dependent-types/8064/21 "2018-08-04T01:03:52Z")
> [@burakumin](#): > > I was just worried about extending a thread that potentially no one else would care about. If you haven't seen it before, this might interest you: - [https://github.com/rust-lang/rfcs/pull/1933](https://github.com/rust-lang/rfcs/pull/1933) - [A taste of dependent types](https://kmcallister.github.io/talks/rust/2015-dependent-types/slides.html) I'm perhaps an oddball, but dependent types interest me deeply 🙂 > [@burakumin](#): > > But at the same time I consider these questions: do I really need this ? what price (in term of code complexity, increase of compilation time, binary bloat) am I ready to pay for something like this ? And even more interestingly I’m considering this other piece of code: 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 {..}` 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. > [@burakumin](#): > > As already said, I have no deep understanding about how dependent type works but my gut feeling is that such code would be rejected because - correct me if I’m wrong - the values those types depend on must be immutable. The snippet you wrote brings a few questions to front. First, it seems to me that writing `Foo::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](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. > [@burakumin](#): > > Why should it be a better idea to support your case rather than mine? Not to say the answer is obvious ; at least it is not to me (and in the end each of these two ideas don’t even have to exclude the other one). 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: ```rust let token = a.token(); let u = Foo<{token}>::new(); a.modify(); let v = Foo<{token}>::new(); let equal = v == u; // valid ``` ---
**Author:** ![burakumin](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/burakumin/32/1838_2.png) [@burakumin](https://internals.rust-lang.org/u/burakumin)\ **Post date:** [August 6, 2018, 5:13pm UTC](https://internals.rust-lang.org/t/variable-dependent-types/8064/22 "2018-08-06T17:13:31Z")
> [@Centril](#): > > The snippet you wrote brings a few questions to front. First, it seems to me that writing `Foo::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` . 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`. 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): ```rust // a is not used anywhere inside bar_tag fn bar_tag(u: &Foo, v: &Foo) { … } // a is borrowed when calling bar_ref fn bar_ref(u: &Foo, v: &Foo) { … } // a is mutably borrowed when calling bar_ref fn bar_mut(u: &Foo, v: &Foo) { … } … let a : MyContext = … let u = Foo::::new( … ); let v = Foo::::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. > [@Centril](#): > > ```rust > let token = a.token(); > let u = Foo<{token}>::new(); > a.modify(); > let v = Foo<{token}>::new(); > let equal = v == u; // valid > > ``` That may work indeed, although it requires that `token()` copies some information. ---
**Author:** ![Centril](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/centril/32/3334_2.png) [@Centril](https://internals.rust-lang.org/u/Centril)\ **Post date:** [August 6, 2018, 5:38pm UTC](https://internals.rust-lang.org/t/variable-dependent-types/8064/23 "2018-08-06T17:38:55Z")
> [@burakumin](#): > > Not necessarily. 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._ > [@burakumin](#): > > 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). Sure; but I would like to have sigma types in the language as well; and then you could carry an internal reference to `a`. > [@burakumin](#): > > That may work indeed, although it requires that `token()` copies some information. 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. ---
**Author:** ![nielsle](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/nielsle/32/3356_2.png) [@nielsle](https://internals.rust-lang.org/u/nielsle)\ **Post date:** [August 7, 2018, 6:23am UTC](https://internals.rust-lang.org/t/variable-dependent-types/8064/24 "2018-08-07T06:23:08Z")
Bluss has written a very nice [indexing](https://docs.rs/indexing/0.3.2/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. ---
**Author:** ![system](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/system/32/14092_2.png) [@system](https://internals.rust-lang.org/u/system)\ **Post date:** [March 25, 2019, 8:30am UTC](https://internals.rust-lang.org/t/variable-dependent-types/8064/25 "2019-03-25T08:30:36Z")
Closed on March 25, 2019, 8:30am UTC This topic was automatically closed 90 days after the last reply. New replies are no longer allowed. [Previous page](https://internals.rust-lang.org/t/variable-dependent-types/8064.md?page=1)