# Variable dependent types?

**URL:** <https://internals.rust-lang.org/t/variable-dependent-types/8064>\
**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:** 20\
**Page:** 1

<div class="post-metadata">

**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:** [July 25, 2018, 8:27pm UTC](https://internals.rust-lang.org/t/variable-dependent-types/8064/1 "2018-07-25T20:27:04Z")

</div>

From time to time I’ve found myself wanting to express some weird concept that I have never found expressible in any language i know, something that might be called “variable dependent generic types”. For example:

```rust
struct VectorSpace {…}
struct Vector<let v: VectorSpace> {…}

impl<let v: VectorSpace> Add for Vector<v> {…}

fn main() {
    let a = VectorSpace::new();
    let b = VectorSpace::new();

    let x = Vector<a>::new(…);
    let y = Vector<a>::new(…);
    let z = Vector<b>::new(…);
    // x and y have the same type but type of z is distinct
    let u = x + y; // ok
    let v = x + z; // compilation error
}

```

**Disclaimer** : this is not a (pre-)rfc, not intended to become a (pre-)rfc in the near future. I’m not even sure there is a workable idea in the design space. I just hope to get feedback about similar design issues from other rust users, how they can be addressed, if related type system concepts are already known and whether these concepts might be considered for Rust in the future.

The problem i’m trying to solve is that sometimes we have a bunch of objects depending on what we could loosely call a common _context_ (= a common set of data that all these objects “share” and rely on). The crux of the matter is that objects related to _different contexts_ shouldn’t mix meaningfully. Consequently any attempt to connect them should be invalidated somehow. By “connecting them” I mean using them as parameters of the same method, just like the pairs of vectors that are added in the previous example. Generally this constrain is not (and as far as i can tell cannot be) encoded in the type system. As a consequence the only possible behavior left is to make every object keep a pointer/reference to the appropriate context, then to check if contexts are consistents, and finally to fail at runtime when incompatible contexts are erronously mixed.

In certain situations, the context may be represented by a value known at compilation time. In this case rfc for [const generics](https://github.com/rust-lang/rfcs/blob/master/text/2000-const-generics.md) might be enough. But this implies two strong limitations:

- Compile time constants … must be known at compile time. This means the compiler must already know the complete list of actually used types from the abstract family `A<const K : T>`. By consequence it is impossible to _create_ contexts dynamically.
- With such an approach contexts cannot have internal mutable state: they must be pure values in the mathematical sense.

The example above may look a bit abstract but I can think of many situations where this could be used:

- Imagine that you have two iterators pointing to different items of a collection. you may want to define some sort of `CollectionSlice` representing the sequence of items between these two positions. Of course you need the boundaries to belong to the same collection.
- Similarly one can consider the task of finding the shortest path between two vertices of a given graph.
- One can only apply arithmetic operations to square matrices if their sizes matches. Const generic can be used if you know this size at compile time but if you’re loading them from files or db the size may only be known at runtime. Still it would be nice to check size consistency once early on, encode it inside the type system and then apply whatever complex sequence of operations is needed.

Something that strikes me is the similarity between this kind of dependency to variables and lifetimes : `Vector<b>` should not outlive the scope of `b` just like `Foo<'a>` should not outlive lifetime `'a`. This seems to suggest Rust may be a good contender to express this kind of idea. I’m aware many aspects would need to be clarified (How type unification works? Can we move/borrow the variable and under which conditions? Does it require monomorphization?) and investigation might possibly show that in the end this cannot work. Or there might already exist other good-enough strategies to encode similar constrains. Just asking…

---

<div class="post-metadata">

**Author:** ![ExpHP](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/exphp/32/6208_2.png) [@ExpHP](https://internals.rust-lang.org/u/ExpHP)\
**Post date:** [July 25, 2018, 9:05pm UTC](https://internals.rust-lang.org/t/variable-dependent-types/8064/2 "2018-07-25T21:05:47Z")

</div>

This is often something I've vaguely wanted, but you can easily simulate it with locally-defined marker structs. In fact, I'm not even sure whether this has any less expressive power:

```rust
trait Tag {}
struct VectorSpace<V: Tag>(PhantomData<V>);
struct Vector<V: Tag>(PhantomData<V>);

macro_rules! new_vector_space {
    ($name:ident) => {{
        #[allow(bad_style)]
        enum $name {}

        impl Tag for $name {}

        VectorSpace::<$name>::new()
    }};
    () => { new_vector_space!{UnnamedVectorSpace} };
}

fn main() {
    // or 'let a = new_vector_space!{a};' for better error messages
    let a = new_vector_space!{};
    let b = new_vector_space!{};

    let x = a.new_vector(…);
    let y = a.new_vector(…);
    let z = b.new_vector(…);

    let u = x + y; // ok
    let v = x + z; // forbidden
}

```

* * *

> [@burakumin](#):
>
> One can only apply arithmetic operations to square matrices if their sizes matches. Const generic can be used if you know this size at compile time but if you’re loading them from files or db the size may only be known at runtime.

This last example sounds like a use for "standard" dependent types. I'm not sure the variable needs to be included.

---

<div class="post-metadata">

**Author:** ![mcy](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/mcy/32/6512_2.png) [@mcy](https://internals.rust-lang.org/u/mcy)\
**Post date:** [July 25, 2018, 9:27pm UTC](https://internals.rust-lang.org/t/variable-dependent-types/8064/3 "2018-07-25T21:27:48Z")

</div>

I’m suspicious of type information that is determined at runtime. There’s a lot of people who excitedly mutter about dependent types but I question what the monomorphization strategy is. Something like

```rust
// how do you momomorphize this without erasure (ew)
// or runtime monomorphization? (ewww)
fn add_zero<let V: VSpace, let W: VSpace>(v: Vector<V>) -> Vector<{V + W}> {
    v + W.zero()
}

```

I’m not convinced that a low-level language like Rust with a tiny `std` can deal with this kind of thing- the only languages I’ve seen with dependent types have monstrous runtimes and GC.

---

<div class="post-metadata">

**Author:** ![canndrew](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/canndrew/32/1676_2.png) [@canndrew](https://internals.rust-lang.org/u/canndrew)\
**Post date:** [July 26, 2018, 12:10am UTC](https://internals.rust-lang.org/t/variable-dependent-types/8064/4 "2018-07-26T00:10:36Z")

</div>

> [@mcy](#):
>
> I’m not convinced that a low-level language like Rust with a tiny `std` can deal with this kind of thing- the only languages I’ve seen with dependent types have monstrous runtimes and GC.

How about Idris? Idris compiles to C, it has a GC but I don't see why that's strictly necessary.

---

<div class="post-metadata">

**Author:** ![mcy](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/mcy/32/6512_2.png) [@mcy](https://internals.rust-lang.org/u/mcy)\
**Post date:** [July 26, 2018, 1:07am UTC](https://internals.rust-lang.org/t/variable-dependent-types/8064/5 "2018-07-26T01:07:36Z")

</div>

I don’t know Idris’s internals- my fear is that there may be costs that can’t be paid at compile time if a type has runtime-dependent components. Here’s a better example of what I’m worried about:

```rust
fn foo(x: A) -> B<x> { .. }

```

At least, I don’t see the benefits of something like this that `const` generics (as proposed right now, they’re not even their final form).

---

<div class="post-metadata">

**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:** [July 26, 2018, 3:44am UTC](https://internals.rust-lang.org/t/variable-dependent-types/8064/6 "2018-07-26T03:44:23Z")

</div>

> [@mcy](#):
>
> I’m suspicious of type information that is determined at runtime. There’s a lot of people who excitedly mutter about dependent types but I question what the monomorphization strategy is. Something like
> 
> ```rust
> // how do you momomorphize this without erasure (ew)
> // or runtime monomorphization? (ewww)
> fn add_zero<let V: VSpace, let W: VSpace>(v: Vector<V>) -> Vector<{V + W}> {
> v + W.zero()
> }
> 
> ```

This depends on how `Vector` is defined. If you have something like:

```rust
struct Vector<T, let N: usize> {
    vec: ::std::vec::Vec<T>,
}

```

then `N` should have no impact on monomorphization (assuming we don't let `N` affect the choice of some associated type). I think you can get far with restricting things this way. This talk seems relevant:

[![](https://img.youtube.com/vi/lJB5MhYJ4Js/maxresdefault.jpg "Parametric Quantifiers for Dependent Type Theory") ](https://www.youtube.com/watch?v=lJB5MhYJ4Js)

> [@mcy](#):
>
> I don’t know Idris’s internals- my fear is that there may be costs that can’t be paid at compile time if a type has runtime-dependent components.

Here's a paper:

- [Practical Erasure in Dependently Typed Languages](https://eb.host.cs.st-andrews.ac.uk/drafts/dtp-erasure-draft.pdf)

Also relevant:

- [Erasure By Usage Analysis — Idris 1.3.3 documentation](http://docs.idris-lang.org/en/latest/reference/erasure.html)
- [http://citeseerx.ist.psu.edu/viewdoc/summary;jsessionid=1F796FCF0F2C4C535FC70F62BE2FB821?doi=10.1.1.62.3849](http://citeseerx.ist.psu.edu/viewdoc/summary;jsessionid=1F796FCF0F2C4C535FC70F62BE2FB821?doi=10.1.1.62.3849)

---

<div class="post-metadata">

**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:** [July 26, 2018, 8:52pm UTC](https://internals.rust-lang.org/t/variable-dependent-types/8064/7 "2018-07-26T20:52:05Z")

</div>

> [@ExpHP](#):
>
> but you can easily simulate it with locally-defined marker structs. In fact, I’m not even sure whether this has any less expressive power:

Thanks @ExpHP. This is a very intriguing solution. Actually I didn't know you could define types locally inside functions. It shares some aspects with what I'd like to express but it is not as expressive. In your example `Tag` implementations can only provide information known at compile time. They cannot for example contain the vector space dimension if this one is defined at runtime.

One could think about solving the previous issue by letting the `Vector<>` type handle the dimension, for example by changing the signature to `new(dim : usize)`. Now a consumer is indeed allowed to encode the distinction between two distinct `VectorSpace<>` in the type system and to give them distinct dimensions. However he is not _forced_ to do it. He can as well declare:

```rust
let a = VectorSpace::<MySingleTag>::new(2);
let b = VectorSpace::<MySingleTag>::new(3);

```

This makes the whole idea far less appealing. Nothing prevents the user to create some `a` and `b` that actually represent incompatible data and still make this distinction invisible in the type system. Then as a provider of an hypothetical `vectorspace` crate, when I want to provide `impl Add for Vector` I cannot rely on the desired invariant that vectors with the same tag _should necessarily have the same dimension_.

> [@mcy](#):
>
> I’m suspicious of type information that is determined at runtime. There’s a lot of people who excitedly mutter about dependent types but I question what the monomorphization strategy is. Something like

> [@Centril](#):
>
> If you have something like [...] then `N` should have no impact on monomorphization (assuming we don’t let `N` affect the choice of some associated type)

I was considering something similar to what @Centril is suggesting: no impact on monomorphization. Dependency to variables should be a pure compilation concept just like const or lifetimes. `Vector<vectorspace>` is then compiled as a single type.

---

<div class="post-metadata">

**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:** [July 26, 2018, 9:36pm UTC](https://internals.rust-lang.org/t/variable-dependent-types/8064/8 "2018-07-26T21:36:59Z")

</div>

> [@mcy](#):
>
> ```rust
> // how do you momomorphize this without erasure (ew)
> // or runtime monomorphization? (ewww)
> fn add_zero<let V: VSpace, let W: VSpace>(v: Vector<V>) -> Vector<{V + W}> {
> v + W.zero()
> }
> 
> ```

@mcy : I suppose that `V + W` represents the direct sum of vector spaces? If yes I'm not considering something as powerful. The idea was to rely on variables only where `V + W` could either be a value or an expression depending on the point of view. The idea of using expressions crossed my mind but it seems to be a far more complicated issue.

---

<div class="post-metadata">

**Author:** ![ExpHP](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/exphp/32/6208_2.png) [@ExpHP](https://internals.rust-lang.org/u/ExpHP)\
**Post date:** [July 26, 2018, 9:49pm UTC](https://internals.rust-lang.org/t/variable-dependent-types/8064/9 "2018-07-26T21:49:04Z")

</div>

> [@burakumin](#):
>
> Now a consumer is indeed allowed to encode the distinction between two distinct `VectorSpace<>` in the type system and to give them distinct dimensions. However he is not forced to do it.

`VectorSpace::new` can be made `doc(hidden)` or renamed to something scarier-sounding, and the macro can be pushed forward as the proper way to generate them. Because it encapsulates the struct in a block (the second `{` hiding in the `=> {{`), the macro is incapable of producing two spaces with the same type.

If you want to be able to rely on this assumption even in unsafe code, `new` can be made `unsafe` as well.

---

<div class="post-metadata">

**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:** [July 27, 2018, 9:16pm UTC](https://internals.rust-lang.org/t/variable-dependent-types/8064/10 "2018-07-27T21:16:40Z")

</div>

> [@ExpHP](#):
>
> If you want to be able to rely on this assumption even in unsafe code, `new` can be made `unsafe` as well.

@ExpHP That is indeed a possibility but I found it dubious to consider macros as valid safe wrappers around unsafe code.

Another downside of your method is that the Tag trait feels like a very ad hoc solution (semantically it does not represent anything) and more importantly it must be anticipated in the design of the actual context type (=`VectorSpace` in the current example). If you are considering the `CollectionSlice` example in the opening post, I wouldn't expect all pre-existing collections types to include such a mechanism but I would still like to be able to define such slices in a child crate.

Anyway I must aknowledge this pattern goes further than what I would have expected to be doable with current Rust. I'll try to make additional experiments.

@Centril I've started to read your reference and it does seem relevant but even with some familiarity with Haskell I found the syntax of Idris quite difficult to decipher. Just a vague question: is there any type unification possible in this context? If yes how and when can they determine that `Palindrome (makeList x y z)` and `Palindrome [1, 2, 3]` are or aren't the same type?

---

<div class="post-metadata">

**Author:** ![ExpHP](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/exphp/32/6208_2.png) [@ExpHP](https://internals.rust-lang.org/u/ExpHP)\
**Post date:** [July 27, 2018, 10:42pm UTC](https://internals.rust-lang.org/t/variable-dependent-types/8064/11 "2018-07-27T22:42:12Z")

</div>

The Tag trait was unnecessary, but it _could_ mean something semantically if you wanted to add methods to the tag types (a common use case I have is an associated fn `name() -> &'static str` that is used in some custom Debug impls).

---

<div class="post-metadata">

**Author:** ![keean](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/keean/32/1599_2.png) [@keean](https://internals.rust-lang.org/u/keean)\
**Post date:** [August 1, 2018, 5:48am UTC](https://internals.rust-lang.org/t/variable-dependent-types/8064/12 "2018-08-01T05:48:37Z")

</div>

I think the “Phantom Type” solution is the right one to do this statically.

If you want to do it at run time why not just use ‘if’ statements to test at runtime?

The problem with dependent types is that they case a failure just like a type-system compile time failure at runtime. Is that really the user experience you want? If you use plain old ‘if’ statements to catch the conditions you want to avoid at runtime then you can fail gracefully or give meaningful errors.

Really the question you are asking is can the compiler prove my code cannot ever call the matrix operation with inappropriate types. As soon as runtime polymorphism is concerned the compiler cannot make that guarantee.

There are static solutions using refinement types that can help, what they do is they can force you to put the ‘if’ statement in to get the code to compile. So if the vector operation is called with runtime polymorphic arguments, so the compiler cannot statically prove the function preconditions, you will need to insert an ‘if’ statement to check the precondition to get it to pass type-checking. I think this is the best solution, because there is no hidden cost, you can see any checks that you need to add in your code, and they type-checker will prevent any runtime errors, and enforce the invariant you want.

---

<div class="post-metadata">

**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 1, 2018, 6:02pm UTC](https://internals.rust-lang.org/t/variable-dependent-types/8064/13 "2018-08-01T18:02:08Z")

</div>

> [@keean](#):
>
> If you want to do it at run time why not just use ‘if’ statements to test at runtime?

I suppose I'm the addressee.

> [@keean](#):
>
> The problem with dependent types [...]

What I had in mind is apparently distinct from the academic standard concept of dependent types. I'm definitely not an expert here but my comprehension from the few links provided by @Centril is that type unification for such dependent type depends on runtime values whereas I was considering some alternative idea that only need check at compilation time: type dependent on variables. My idea was that if you define:

```rust
let x = ...;
let y = x.clone();

let u = Foo<x>::new(...);
let v = Foo<y>::new(...);

```

variables `u` and `v` are _not_ of the same type even if `x == y`.

> [@keean](#):
>
> Really the question you are asking is can the compiler prove my code cannot ever call the matrix operation with inappropriate types. As soon as runtime polymorphism is concerned the compiler cannot make that guarantee.

Not sure what you're calling runtime polymorphism here. If it is just the usual stuff (`dyn Trait` or any form of OOP dynamic binding) I've never proposed that. In the example I considered for matrices, something would certainly need to check somewhere during runtime the actual dimension of loaded matrices. But it certainly does make a difference if you are checking this compability for a bunch of matrices once and then encode it in the type system (provided the type system can express this information) or if you have to check compatibility of operands every time some arithmetic operation is involved.

> [@keean](#):
>
> There are static solutions using refinement types that can help, what they do is they can force you to put the ‘if’ statement in to get the code to compile. So if the vector operation is called with runtime polymorphic arguments, so the compiler cannot statically prove the function preconditions, you will need to insert an ‘if’ statement to check the precondition to get it to pass type-checking. I think this is the best solution, because there is no hidden cost, you can see any checks that you need to add in your code, and they type-checker will prevent any runtime errors, and enforce the invariant you want.

It seems to me this have similarities with what I was actual proposing. But again I'm not an expert. I don't know what are refinement types for example.

---

<div class="post-metadata">

**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 1, 2018, 9:58pm UTC](https://internals.rust-lang.org/t/variable-dependent-types/8064/14 "2018-08-01T21:58:34Z")

</div>

> [@burakumin](#):
>
> Just a vague question: is there any type unification possible in this context? If yes how and when can they determine that `Palindrome (makeList x y z)` and `Palindrome [1, 2, 3]` are or aren’t the same type?

I'm by no means an expert on the type theory of dependent types... But... Dependently typed languages have some varying rules for unification... For example, to unify `Palindrome (makeList x y z)` and `Palindrome [1, 2, 3]` the compiler could run (by reductions / normalization) both sides and determine that they are structurally equal (think `#[structural_match]`) (see definitional equality, [Equality](http://adam.chlipala.net/cpdt/html/Equality.html)).

To ensure that such unification is sound and is erasable, many dependently typed languages will require such type level expressions to be both pure and total (they can't diverge by any mechanism such as panics or infinite loops). A notable exception is Dependent Haskell (which hasn't been fully implemented yet, but you can read about it in Richard Eisenberg's thesis, [[1610.07978] Dependent Types in Haskell: Theory and Practice](https://arxiv.org/abs/1610.07978))

Where the compiler can't determine that two types are equal by itself since the languages type theory of definitional equality is , you usually have some library-encodable mechanism for propositional equality of types by which you can massage proofs yourself:

```haskell
data a :~: b :: k -> k -> * where
    Refl :: a :~: a

http://hackage.haskell.org/package/base-4.9.1.0/docs/Data-Type-Equality.html

data (=) : a -> b -> Type where
   Refl : x = x

http://docs.idris-lang.org/en/latest/proofs/pluscomm.html

data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x

http://agda.readthedocs.io/en/v2.5.2/language/built-ins.html#equality

```

Some more links:

- [type theory - Equality in Coq and in a paper of Awodey - Stack Overflow](https://stackoverflow.com/questions/50073679/equality-in-coq-and-in-a-paper-of-awodeyT)
- [http://kodu.ut.ee/~varmo/tday-andu/chapman-slides.pdf](http://kodu.ut.ee/~varmo/tday-andu/chapman-slides.pdf)
- [http://www.cse.chalmers.se/~peterd/papers/DependentTypesAtWork.pdf](http://www.cse.chalmers.se/~peterd/papers/DependentTypesAtWork.pdf)
- [refl - Rust](https://docs.rs/refl/0.1.2/refl/)
- [identity - Rust](https://docs.rs/identity/0.0.6/identity/)

Now, you can also add in more axioms into the language such as the commutativity of addition for `usize`. This all depends on what primitive types exist in the language and so on. Typically, the more axioms a type theory has, the more it can do for you and the less you will need to prove yourself.

> [@keean](#):
>
> I think the “Phantom Type” solution is the right one to do this statically.

I don't agree; Using `PhantomData` pervasively for type level programming typically leads to encoding of monstrosities such as [singletons: A framework for generating singleton types](https://hackage.haskell.org/package/singletons-2.2) (N.B. Eisenberg who authored this package agrees that this is a bad approach and that it is a hack).

> [@keean](#):
>
> The problem with dependent types is that they case a failure just like a type-system compile time failure at runtime.

They don't have to. As previously mentioned, most dependently typed languages ensure termination and thus you can't fail (diverge) at run-time. Now, given user input, most programs will have some notion of "failure" such as when an incorrect input is given by the user, but this is normal program behavior and not logic bugs.

> [@keean](#):
>
> Really the question you are asking is can the compiler prove my code cannot ever call the matrix operation with inappropriate types. As soon as runtime polymorphism is concerned the compiler cannot make that guarantee.

For the same reason as I've noted above this does not seem true.

> [@burakumin](#):
>
> I’m definitely not an expert here but my comprehension from the few links provided by @Centril is that type unification for such dependent type depends on runtime values

That does not necessarily entail that type checking must wait until the actual runtime values are known; for example, if you have two abstract values `x: usize` and `y: usize`, then the type checker could unify `x + y` and `y + x` even tho the value of `x` and `y` are not known at run-time.

> [@burakumin](#):
>
> variables `u` and `v` are _not_ of the same type even if `x == y` .

If the user has no recourse to prove this manually and the type system can't do this for us automatically, then such a system does not seem particularly useful.

> [@burakumin](#):
>
> I don’t know what are refinement types for example.

Refinement types are a type system feature with which you can refine existing base types by a predicate. For example, you may state that `let foo : {x: usize | even(x)} = make_even_number();` and then the type of `foo` is all even `usize`s. In contrast, dependent types are usually built up by-construction.

See:

- [terminology - Dependent types vs refinement types - Computer Science Stack Exchange](https://cs.stackexchange.com/questions/21728/dependent-types-vs-refinement-types)
- [Difference between Dependent type , refinement type and Hoare Logic - Computer Science Stack Exchange](https://cs.stackexchange.com/questions/54957/difference-between-dependent-type-refinement-type-and-hoare-logic)

Thinking a bit more on the topic of monomorphization, it seems to me that what we really want to avoid is a situation such as:

```agda
data Bool = True | False

-- These types have different memory representations...
data TypeA = ...  
data TypeB = ...

pickType : Bool -> Type
pickType True = TypeA
pickType False = TypeB

```

We can get the same situation with:

```rust
// These types have different memory representations...
struct TypeA(Vec<&'static str>);
struct TypeB;

trait Func { type Output; }

struct Input<let cond: bool> { ... }

impl Func for Input<{true}> { type Output = TypeA; }
impl Func for Input<{false}> { type Output = TypeB; }

fn pick_type(cond: bool) -> <Input<{cond}> as Func>::Output {
    match cond {
        true => TypeA(vec!["foo", "bar", ..]),
        false => TypeB,
    }
}

```

It seems to me that we want to prevent the pattern matching on types that is occuring at the implementations of `Func for Input<{x}>`. Two ways come to mind to prevent such pattern matching:

1. Ensure that `x` is polymorphic in the input and that you can't specialize on `let` in impls.
2. Ensure that `let` parameters and associated types can't be combined in implementations.

I think that if you ensure either 1. or 2. you will avoid having runtime values affect the memory layout of types.

---

<div class="post-metadata">

**Author:** ![keean](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/keean/32/1599_2.png) [@keean](https://internals.rust-lang.org/u/keean)\
**Post date:** [August 1, 2018, 11:07pm UTC](https://internals.rust-lang.org/t/variable-dependent-types/8064/15 "2018-08-01T23:07:22Z")

</div>

> I don’t agree; Using PhantomData pervasively for type level programming typically leads to encoding of monstrosities such as [singletons: A framework for generating singleton types](https://hackage.haskell.org/package/singletons-2.2) 1 (N.B. Eisenberg who authored this package agrees that this is a bad approach and that it is a hack).

You can certainly add some syntactic sugar and some helper functions to make it nicer, but this is the underlying representation that you would use. We used a lot of phantom types in the HList paper. The realisation after writing that paper, and the follow up on OOHaskell, was that you don't actually want to write all the boilderplate, but that the techniques are logically sound. In effect it is working in the "types that depend on types" corner of the lambda-cube. Using polymorphic-recursion you can even reify values to types, like in this Haskell example:

```Haskell
class T t where
    count :: t -> Int

instance T () where
    count () = 0

instance T t => T [t] where
    count [x] = 1 + count x

f :: T t => Int -> t -> Int
f x t | x == 0 = count t
f x t | x >= 1 = f (x - 1) [t]

main = do
    v <- getLine
    putStrLn (show (f (read v :: Int) ()))

```

Consider we have a refinement type like `Int < 23`, now consider we get a normal integer from stdin, and we then try and assign this integer to a variable of type `Int < 23`. If the value entered by the user is greater than 22, then the program will fail with a type-system error at runtime, and we do not really have any good mechanisms for catching type-errors at runtime.

```rust
let v : Int < 23
let x = userInput
v = x // can be a badly typed expression at runtime.

```

What we can do is use path-dependent types to do this:

```rust
let v : Int < 23
let x = userInput
if x < 23 {
    v = x // with path-dependent types x has type 'Int < 23' here
} else {
    print "integer too small" // x has type 'Int >= 23' here
}

```

So we can use path-dependent types to prevent runtime errors from IO. However we can see that the `if` test has to look very similar to the type refinement. If we have something like:

```rust
if mandelbrot_converges(x,x) {
   v = x
}

```

Now we have given the compiler the task of proving or disproving that whether mandelbrot set converges at co-ordinates (x, x) is the same as being less than 23. In effect we end up having to prove general function equivalence, which is unsolvable.

---

<div class="post-metadata">

**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 2, 2018, 12:49am UTC](https://internals.rust-lang.org/t/variable-dependent-types/8064/16 "2018-08-02T00:49:15Z")

</div>

> [@keean](#):
>
> In effect it is working in the “types that depend on types” corner of the lambda-cube.

I'm suggesting that we eventually (and by eventually I mean in plenty of years -- we should start with GADTs and such things first...) move out of that corner and enter a limited subset of λP2 (not λPω because of the lack of HKTs) such that we can encode a function:

```rust
fn replicate<T: Clone>(len: usize, elem: T) -> Vector<T, {len}> {
    ...
}

```

as well as:

```rust
struct Sigma<T, H: Func> {
    fst: T,
    // We still need to prevent picking types with
    // different memory layouts based on `fst` here.
    snd: H::Proj<{fst}>,
}

```

of course, when you encode such a thing, we can't erase `len` at runtime, but I find that desirable in this case. Imposing rules 1 & 2 in my previous comment should prevent us from having memory layouts depend on run-time values.

> [@keean](#):
>
> If the value entered by the user is greater than 22, then the program will fail with a type-system error at runtime, and we do not really have any good mechanisms for catching type-errors at runtime.

The solution is to prevent the unification of `v : Int < 23` and `userInput : Int` until we have a proof that `userInput : Int < 23` which your second example illustrates.

As for catching type-errors at runtime (not suggesting that we do this for Rust, since it would probably be a bad fit...), Haskell has this: [7.13.&nbsp;Deferring type errors to runtime](https://downloads.haskell.org/~ghc/7.6.2/docs/html/users_guide/defer-type-errors.html). It is not necessarily a good approach, but it exists 😉

> [@keean](#):
>
> However we can see that the `if` test has to look very similar to the type refinement.

Yes, but this is also a trivial example... If we say something like:

```rust
fn replicate<T: Clone, let n: Int>(elem: T) -> Vec<T, {n}> { .. }

let n = userInput : Int;
let v : Vec<Vec<String, {23}>, {n}>;

let x = userInput : Int;
if x == _ {
    // We know that:
    // v : Vec<Vec<String, {23}>, {n}>;
    // We know that:
    // replicate(replicate("foo".to_owned())) : Vec<Vec<String, {?0}>, {?1}>;
    // We unify ?0 with 23
    // We unify ?1 with n
    v = replicate(replicate("foo".to_owned()));
} else {
    diverge();
}

```

Of course, you need to make this inference happen (which Idris / Agda should be capable of at least), but even this is simple yet the test does not look at all similar to me.

> [@keean](#):
>
> Now we have given the compiler the task of proving or disproving that whether mandelbrot set converges at co-ordinates (x, x) is the same as being less than 23. In effect we end up having to prove general function equivalence, which is unsolvable.

So the compiler does not have the axiom of function extensionality (and we presumably don't add the univalence axiom so we can't encode it as a lemma either...) and inference will give up when faced with solving that... The user will have to use manual proofs using library encoded propositional equality / refl as is usually done in Idris / Agda / friends...

---

<div class="post-metadata">

**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 3, 2018, 11:17am UTC](https://internals.rust-lang.org/t/variable-dependent-types/8064/17 "2018-08-03T11:17:04Z")

</div>

> [@Centril](#):
>
> If the user has no recourse to prove this manually and the type system can’t do this for us automatically, then such a system does not seem particularly useful.

@Centril. Thanks for all the information.

Nevertheless, the previous sentence sounds like a fallacy. You seem to deduce from _"Any extension of the type system of Rust that can express dependent types would be particularly useful."_ that _"Any extension of the type system of Rust that cannot express dependent types is necessarily useless."_ I don't plan to engage in a debate on the design / benefit / inconvenient of the idea I had in mind compared to dependent types because @ExpHP's solution, though a bit ad hoc, meets my current needs reasonably well. But I still see much value for multiple problems (some mentioned in the OP) in having some `Foo<let x : Bar>` type where all that counts is the variable used (for which the compiler could reason about), not the value it represents (which might only be known at runtime and even more strikingly which could change during the execution flow).

---

<div class="post-metadata">

**Author:** ![tupshin](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/tupshin/32/2573_2.png) [@tupshin](https://internals.rust-lang.org/u/tupshin)\
**Post date:** [August 3, 2018, 11:41am UTC](https://internals.rust-lang.org/t/variable-dependent-types/8064/18 "2018-08-03T11:41:08Z")

</div>

> [@burakumin](#):
>
> ```rust
> let x = ...;
> let y = x.clone();
> 
> let u = Foo<x>::new(...);
> let v = Foo<y>::new(...);
> 
> ```
> 
> variables `u` and `v` are _not_ of the same type even if `x == y` .
> 
> ![](https://sea2.discourse-cdn.com/flex016/user_avatar/internals.rust-lang.org/keean/40/1599_1.png) keean:

This is sounding a lot like Scala's path dependent types.

> <https://stackoverflow.com/questions/2693067/what-is-meant-by-scalas-path-dependent-types>

> **[fpdt\_post.pdf](https://lampwww.epfl.ch/~amin/dot/fpdt_post.pdf)**
>
> 290.94 KB

---

<div class="post-metadata">

**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 3, 2018, 1:36pm UTC](https://internals.rust-lang.org/t/variable-dependent-types/8064/19 "2018-08-03T13:36:14Z")

</div>

> [@burakumin](#):
>
> You seem to deduce from _“Any extension of the type system of Rust that can express dependent types would be particularly useful.”_ that _“Any extension of the type system of Rust that cannot express dependent types is necessarily useless.”_

Not at all; In fact, I have several type system extensions orthogonal in mind that I have in mind and will eventually propose...

> [@burakumin](#):
>
> But I still see much value for multiple problems (some mentioned in the OP) in having some `Foo<let x : Bar>` type where all that counts is the variable used (for which the compiler could reason about), not the value it represents (which might only be known at runtime and even more strikingly which could change during the execution flow).

... but if we are going to have dependent types, then unification seems vital to it being usable enough to warrant the increase in complexity. If all you have is that you can refer to variables and fields of those in scope, then you can at most encode things like:

```rust
let u = Foo<a + b>::new();
let v = Foo<a + b>::new();
let v = u; // OK, these types unify.

```

However, not even this will work:

```rust
let u = Foo<a + b>::new();
let v = Foo<b + a>::new();
let v = u; // Nope.

let u = Foo<(a + b) + c>::new();
let v = Foo<a + (b + c)>::new();
let v = u; // Nope.

```

Further, keep in mind that we're adding const generics, a form of value-dependent types limited to compile time values. It would be quite inconsistent to have unification in const generics but not for runtime-value-dependent-types if we ever add the latter.

> [@burakumin](#):
>
> I don’t plan to engage in a debate on the design / benefit / inconvenient of the idea I had in mind compared to dependent types because @ExpHP’s solution, though a bit ad hoc, meets my current needs reasonably well.

Fair enough 🙂 I'm happy to end the discussion to here if you don't want to continue.

---

<div class="post-metadata">

**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 3, 2018, 8:42pm UTC](https://internals.rust-lang.org/t/variable-dependent-types/8064/20 "2018-08-03T20:42:39Z")

</div>

> [@tupshin](#):
>
> This is sounding a lot like Scala’s path dependent types.

From what I have read so far it does not seem related. The feature explained in this paper does not seem to give you the possibility to express that `leo.Food` and `simba.Food` should be different types. on the contrary if `leo` and `simba` are actually both instances of `Lion` these types will be the same (`Meat`). This is not what was proposed here.

> [@Centril](#):
>
> Fair enough 🙂 I’m happy to end the discussion to here if you don’t want to continue.

I didn't mean that there was no point in going on with this discussion. Sorry if I gave you this impression. I am interested in discussing whatever extension of the type system that might be useful. Just that now that I know how to move on with my pet projects, I was just worried about extending a thread that potentially no one else would care about.

> [@Centril](#):
>
> However, not even this will work:
> 
> ```rust
> let u = Foo<a + b>::new();
> let v = Foo<b + a>::new();
> let v = u; // Nope.
> 
> ```

I'm aware it won't work, that dependent types would apparently allow this piece of code and that they are a more natural extension of const generics. 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:

```rust
let u = Foo<a>::new();
a.modify()
let v = Foo<a>::new();
let equal = v == u; // valid

```

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. They must be mathematical values with no inner state, which suits Haskell (and I suppose Idris and Agda) very well. But Rust is certainly not this kind of language, right ? It deals with states all the time. 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).

[Next page](https://internals.rust-lang.org/t/variable-dependent-types/8064.md?page=2)