Add dependent types

[zaoqi]

No description provided.

[RustyYato]

You need to give more information than that. Why should we add dependent types? They are a very complex addition the language, and so we need a very good motivation for adding them. Would const-generics be enough of an extension? If so you can track that here #2000 and here

[Centril]

RFC #2000 is an accepted proposal for the addition of a measure of dependent typing for types dependent on compile-time values. Beyond that, we have no current plans to add run-time dependent typing.

[natewind]

Why should we add dependent types?

Because they’d let us enforce function contracts in compile time without turning everything into an optional and paying the runtime cost. For example, (/) takes a non-zero as its second argument, so passing unchecked input there should be a compile-time error (to convert an int into a non-zero int, you have to pass it though a check).

It’s kind of like a generalization of the borrow checker, it’s very much in the spirit of Rust (compiler forcefully stopping a silly human from making stupid mistakes), and it would prevent a whole class of bugs — everything but logical bugs, I think. Basically, dependent types together with optionals (Result) help us get rid of non-total functions entirely.

[RustyYato]

For example, (/) takes a non-zero as its second argument,

This is a bad example, as this can be done with normal types like NonZeroI32. I am aware of the nice things that dependent types can bring, but I don't think that it would be sufficiently more useful than const-generics (when that lands).

More to the point, what can you do with dependent types that you can't do with const-generics?

[natewind]

First, NonZeroI32 is deprecated since 1.26.0. Second, does it force you to add checks? Judging by the description, it’s just an axiom (a promise to the compiler), which is only an edge case (basically to encode some hardware contracts in MC), not what you’d want most of the time.

I am aware of the nice things that dependent types can bring

It’s not just “nice things”. It’s virtually the final solution to panics.

More to the point, what can you do with dependent types that you can't do with const-generics?

Can you use them to force the user of your function to check something about the arguments before passing them (unless they’re known at compile time)? For example, when dividing two numbers you got from IO? Or when addressing a vector by index, and both its size and the index depend on IO, can you force the caller to make sure the index is less than the size, without a runtime overhead?

[Lokathor]

https://doc.rust-lang.org/core/num/struct.NonZeroI32.html ? It doesn't say deprecated anywhere on that page.

[RustyYato]

Can you use them to force the user of your function to check something about the arguments before passing them (unless they’re known at compile time)? For example, when dividing two numbers you got from IO? Or when addressing a vector by index, and both its size and the index depend on IO, can you force the caller to make sure the index is less than the size, without a runtime overhead?

There is no way to both have checks and avoid runtime overhead. That simply doesn't make sense.

First, NonZeroI32 is deprecated since 1.26.0. Second, does it force you to add checks? Judging by the description, it’s just an axiom (a promise to the compiler), which is only an edge case (basically to encode some hardware contracts in MC), not what you’d want most of the time.

NonZeroI32 and friends were stabilized in 1.34.0, there is no plans to deprecate them. I'm not sure what you are refering to when you say they are deprecated in 1.26.0.

It does add a check if you use NonZeroI32::new, but there is an unsafe variant that doesn't do checks.

It’s not just “nice things”. It’s virtually the final solution to panics.

Yes, with dependent types you could get rid of all panics. But that's only if you want to add the immense annotation burden that comes along with dependent types. I don't know if this is a good tradeoff. I've looked into languages like Idris, which have dependent types as a first class item, and it works for them because the syntax of the Idris gets out of your way really fast. But Rust doesn't do this. Rust tries to annotate every important detail, and this means the annotation burden in Rust is far greater than other dependently typed languages.

You can get rid of all panics right now in Rust, by just having all fallible functions, but this has numerous other problems. But, I don't think getting rid of panics is a viable or even worthy goal. Panics exist for when things go horribly wrong, and there will always be a need for such tools.

When writing performance sensitive code, it is useful to put in debug_asserts everywhere you make an assumption, so that you can test those assumptions in debug mode, and they will be assumed in release mode. Such code wouldn't even think about dependent types, because it would force unnecessary checks that are unacceptable.

For code that is less concerned with performance, dependent types can help. But I don't know if they can help more than const generics. For example, with const-generics you can write bounded integers,

struct Int<const LOWER: i128, const UPPER: i128>(u128);

Later once we get more integrated const generics (in where clauses) we can do one step further.

trait IntInner {
    type Inner;
}

struct Int<const LOWER: i128, const UPPER: i128>(<Self as IntInner>::Inner);

impl<const LOWER: i128, const UPPER: i128> IntInner for Int<{LOWER}, {UPPER}>
where
    { UPPER - LOWER < (1 << 8) }
{
    type Inner = u8;
}

impl<const LOWER: i128, const UPPER: i128> IntInner for Int<{LOWER}, {UPPER}>
where
    { UPPER - LOWER >= (1 << 8) }
    { UPPER - LOWER < (1 << 16) }
{
    type Inner = u16;
}

/// ...

It may not look exactly like this, but this should be possible with extended const-generics

Now tell me, where does const-generics fall short for your use case?

[burdges]

There exist numerous languages for formal verification, but few gain any traction and much more work is needed before they become friendly.

An approach might be an optional type system extensions that avoid complicating or slowing down rustc itself, and need not be run for every build, so vaguely like procmacros but extracting much deeper information from type checking.. and thus chalk must come first. I'd think type system extensions could reject otherwise valid rust programs but should not bypass rustc's existing type checking. I've no idea if such type system extensions could only analyze the existing types, if they could suggest types like the bounds for Int above, or if they could even track additional data about bindings, almost like some value-level trait-like thing, aka real dependent types.

Anything like this should probably wait for chalk, but if someone wants to do a PhD around this topic then maybe chat with either the RustBelt project or Karthikeyan Bhargavan.

[natewind]

There is no way to both have checks and avoid runtime overhead. That simply doesn't make sense.

Yes, it does. There are 2 ways to call a non-total function with arguments unknown at compile time: to check the arguments beforehand or to make the function return an optional.

Sometimes the latter is better; it depends on the semantics of the function and on the way the arguments are checked. If it’s a part of what the function does anyway, no need to duplicate the work.

But often you can easily check if the arguments are correct, and calling the function with wrong ones makes no sense (as with division). In this case, returning an optional would introduce additional overhead compared to forcing the users of the function to do the checks. But they should do those checks anyway, even if the compiler can’t make them, so those only introduce overhead compared to unsafe code that shouldn’t exist.

Contracts also propagate. You don’t need to prove the same thing twice. And functions don’t just have preconditions, they can provide guarantees about their return values too, which could mean fewer checks for functions that use return values of other functions.

I'm not sure what you are referring to when you say they are deprecated in 1.26.0.

Sorry, Google directed me to a wrong page.

It does add a check if you use NonZeroI32::new

Hmm, it does look nice, provided rustc optimizes that optional away (by combining the check inside new and pattern-matching outside into one). I’m not sure it does though...

But that's only if you want to add the immense annotation burden that comes along with dependent types. I don't know if this is a good trade-off.

It’s not a trade-off, it’s additional expressiveness for free. Both the domain and the range of a function are already an essential part of its interface, it’s just that usually they’re only expressed in documentation or — worse — in programmer’s mind. Moving such things into the actual code and enforcing them statically is strictly better.

Unless you mean spelling out types everywhere... But Rust does have type deduction, right?..

Rust tries to annotate every important detail, and this means the annotation burden in Rust is far greater than other dependently typed languages.

Point taken. I don’t have an opinion on what is the proper solution here, because I’m a C++/Haskell programmer and I haven’t got time to learn Rust yet (I just fanboy over it in advance and really care about its development).

You can get rid of all panics right now in Rust, by just having all fallible functions

That would be the same thing but worse because no unwinding. What I’m talking about is getting rid of unplanned termination. All possible cases should be handled.

But, I don't think getting rid of panics is a viable or even worthy goal.

Yes, it is! If a panic happens, it usually means you forgot to check for something. It’s not something you can or should solve in runtime, it’s a design-time problem. That’s why, unlike C++, Rust doesn’t have catch (as far as I know).

Panics exist for when things go horribly wrong, and there will always be a need for such tools.

Sure, when you run out of memory or when a cosmic ray strikes the disk. When some externalities not expressed in the language violate your cozy abstract world, not when it’s your own mistake.

so that you can test those assumptions in debug mode, and they will be assumed in release mode

This is both tedious and unsafe because there are no guarantees. That’s actually another argument in favour of dependent types: to replace virgin debugging with chad static analysis. Math always beats empiricism if it’s realistically computable x)

Such code wouldn't even think about dependent types, because it would force unnecessary checks that are unacceptable.

It’s the opposite. Dependent types let you get rid of unnecessary checks because they propagate. They only require the checks you need anyway because you don’t know anything about IO (unless there are hardware contracts, but that’s what axioms are for).

For example, with const-generics you can write bounded integers

That’s awesome, we can port bounded::integer to Rust! Although, does Rust have some kind of opt-in implicit casts to allow widening the range automatically?..

Either way, it’s good but not enough.

Now tell me, where does const-generics fall short for your use case?

If I understand correctly, const generics are the Rust equivalent of non-type template parameters in C++. Those are powerful, but they’re not enough to implement full-on dependent types in any usable form, only special cases like bounded::integer.

[natewind]

There exist numerous languages for formal verification, but few gain any traction and much more work is needed before they become friendly.

Sure, it’s an area of active research, and I’m not saying dependent types should be added to Rust tomorrow. I just think they should be somewhere on the roadmap. Let Idris and Haskell explore the topic and then absorb the best of what they come up with.

An approach might be an optional type system extensions that avoid complicating or slowing down rustc itself, and need not be run for every build, so vaguely like procmacros but extracting much deeper information from type checking.. and thus chalk must come first. I'd think type system extensions could reject otherwise valid rust programs but should not bypass rustc's existing type checking.

Yeah, something like that. BTW, is it possible for rustc to not recompile individual functions that weren’t changed?

I've no idea if such type system extensions could only analyze the existing types, if they could suggest types like the bounds for Int above, or if they could even track additional data about bindings, almost like some value-level trait-like thing, aka real dependent types.

I’m not sure about the specifics either, although I have a few vague ideas.

Anything like this should probably wait for chalk, but if someone wants to do a PhD around this topic then maybe chat with either the RustBelt project or Karthikeyan Bhargavan.

Sounds tempting, but first I’d have to finish my bachelor’s degree and then get a master’s degree, and I’m not a fan of academic education x) And by the time online education inevitably takes over and they start giving out degrees through exams, somebody will already have done it.

[comex]

For what it's worth, with a powerful enough type system you can sort of simulate dependent types, along the lines of Haskell's singletons. Parts of it are possible in Rust as-is: I tried it once, but gave up after running into too many limitations. But we could get a lot farther with some relatively modest language additions, things that are also useful for other purposes:

• Trait-parametric polymorphism (ability to use traits as generic parameters)
• Generic closures, plus
• Expanded HRTBs, so a function can accept a generic closure as an argument (e.g. F: for<T> FnOnce(T))

(And const generics, but those are already in the works.)

Edit:

• Exhaustiveness checks for set of mutually exclusive impls would also help, since they would make it easier to do computation in the type system.

If anyone wants to see dependent types, I suggest trying to get those features in first, to unlock experimentation. :)

[urosn]

I would like to see Dependent Types because they will enable software verification. I think that it is very important for the future of this language. (Speed + correct-by-construction).

Btw, somehow you should enable infix notation for easier writtings of monads, arrows, etc.

[DestyNova]

It would be easier to start with refinement types as in Liquid Haskell, which are much more restricted than dependent types which can have arbitrary computation in the type (as I understand it... not an expert). Liquid Haskell, and a few other proof checking languages like F* and zz, cleverly avoid implementing lots of verification logic by generating a set of constraints which are passed to an SMT solver like z3.

With these systems you can do really nice things like specifying that a function takes two vectors which must be the same size. You can generally avoid runtime checks since the proofchecker can prove at compile time that the function will never be called with two differently-sized lists. And if it can't automatically prove that (this probably happens a lot), you have to add more annotations or conditional logic that allows the proof to succeed.

It might be possible to emulate Liquid Haskell's approach of extending Haskell with static annotations. I'm learning LH now and don't know remotely enough Rust to attempt something similar at the moment, but I might try it out in a couple of months. Call it Liquid Rust 😆

[rjbergTU]

One case in which I think it could help is when memory sizes are involved.

Imagine an arbitrary piece of data with constant size. Let's say there is a dependent type Size<S> for types with a constant size, where S is a value of usize. Size<S> also implements a dependant type SizeAtMost<S2> for each S2 bigger than S. Now let's say I need to serialize this piece of data to a spot with finite memory, like a QR code.

Normally I would do runtime checking with size_of function somewhere to verify if the object I need to was small enough. But if I know the size of the data in advance, for example, if it is a constant message, I could skip that check. So I could have a function:

to_qr_code<T: SizeAtMost<{QR_SIZE}>>(obj: T) -> QrCode {
 // Some code here
}

which would not need an option or result to implement for this case. Whereas if it size was unknown, or dependent types where not available, I would need runtime checking with Results and such:

try_to_qr_code<T>(obj: T) -> Result<QrCode, QrError> {
   if size_of(obj) > QR_SIZE {
     Return Err(QrError::ObjectTooBig)
   }
   // Some code here.
}

[natewind]

That would also help use dynamic memory less in general.

[orenbenkiki]

Question: Is the following a form of "dependent types", and is the weaker form possible in Rust today?

Suppose I have:

pub struct Foo<X, Y, Z> {
    // Here I can use X, Y, Z as types:
    x: X, y: Y, z: Z
}

Then I can:

impl<X, Y, Z> Foo<X, Y, Z> {
    // Here I can also use X Y Z as types...
    fn set_x(&mut self, x: X) { self.x = x; }
}

Then suppose I have:

type MyFoo = Foo<u8, u16, u32>;

fn do_my_foo(my_foo: MyFoo) {
    // Here I can't use X, Y, Z as types.
    // What I want to write:
    // x: MyFoo::X = 0;
    // What I have to write:
    x: u8 = 0;

    my_foo.set_x(x);
}

This would be a very weak form of dependent types, I guess? Is this possible in Rust today, somehow? If not, has this been suggested/discussed at all, or is this seen as a special case of the much more complex dependent types issue and is not worth consideration on its own?

Speaking of the more general case, then in C++ templates, it is possible to manually add type aliases inside a struct (almost anywhere, really). This allows not only capturing the type parameters but also derived ("dependent") types. Rust-ish equivalent might look like:

pub struct Bar<Y, Z> { ... }
pub struct Foo<X, Y, Z> {
   type X = X;
   type Bar = Bar<Y, Z>;
   x: X, y: Y, z: Z
}

type MyFoo = Foo<u8, u16, u32>;
let x: MyFoo::X = 0;
let bar: MyFoo::Bar = ...;

Is something along these lines being considered?

[natewind]

This is not dependent types.

[hgomersall]

It seems the recent paper and presentation by @cfallin might have something to contribute to this discussion. The motivating case is outlined in that paper. From my perspective, the use case for dependent types is to statically associate handles for operating on a resource with that resource (a specific example: a handle to a DMA operation in which the operation can only take place on a given device).

[natewind]

The main use case for dependent types is getting rid of panics and infinite unproductive recursion.

[ron-wolf]

It seems like someone who worked on the standard library way back in 2016 also would have benefitted from dependent types:

// Since Rust doesn't actually have dependent types and polymorphic recursion,
// we make do with lots of unsafety.

(source, commit)

They don’t seem to be around anymore (I hope you prove me wrong, @gereeter 🙂 ), but I’d count this as a point towards dependent types. I’m not sure if I could summarize all the applications into a single pithy one-liner, but it sure does seem like dependent types have proven themselves useful across several domains. Whether they can be added to Rust in a clean fashion… well, Rust already has quite a bit of bloat, I’m sure a little more couldn’t hurt 😉

[programmerjake]

related:
https://github.com/magmide/magmide