Hacker News new | past | comments | ask | show | jobs | submit login

My biggest wish for Rust right now is dependent types, I find myself wanting them in almost everything I write to ensure it is correct for all possible inputs. It could also improve performance eliminating out of bounds checks in many places.

I recall someone mentioning in a RFC that it was on a distant wishful thinking roadmap. I hope it is.

We had an RFC for Pi types [1] but in the ended, decided it was too much, too soon [2]. The "const generics" RFC [3] adds a minimal, forward-compatible from of this, and is on track to land this year.

1: https://github.com/rust-lang/rfcs/issues/1930

2: https://github.com/rust-lang/rfcs/pull/1657#issuecomment-268... and https://github.com/rust-lang/rfcs/pull/1931#issuecomment-304...

3: https://github.com/rust-lang/rfcs/blob/master/text/2000-cons...

We may or may not end up with them someday, but we need experience with RFC 2000 first.

Holy crow! As someone who remembers when the rust-lang/rfcs repo was created, I can't believe we're over 2000 RFCs submitted!

Issues and PRs are the same thing in GitHub internals, and the RFC number is the PR number. There haven’t been 2000 accepted PRs :)

You're right. I've spent too much time in GitLab, where they are counted separately :). And, besides, I forgot about the PRs to fix typos and so forth.

Is there anything you could do with dependant types that you can't do with a number of types wrapped in an enum? A dependently typed variable should have the same memory footprint of an enum, right? Do you just want a different syntax, or am I missing something?

With dependent types you can perform arithmetic at the type level. This lets you have functions that, e.g., take an array of length n and an array of length m and return an array of length n + m. Ideally, this would let you write programs that are provably correct with no runtime bounds checking.

I just read up on type arithmetic and I guess this is still whooshing over my head, because I can't see what this changes. I can have a function take two vectors of enums and return a new vector with the combined length. I can do operations based on the types of values held by variants in enums, matching only the possible variants. I don't see what can't be done as efficiently with an enum, but I'm very open to being ignorant and clueless.

If you have a function that returns the first n elements of a vector, how do you make sure there are enough elements? Most languages would either insert a runtime check or throw an exception at runtime. With a dependently typed language, you can do the check statically. This means knowing the provenance of n and the vector itself and doing a compile time proof that n can never exceed the length of the vector.

Okay, I see how that sort of check could be useful. I don't think it's impossible to do without dependant types in principle, but Rust isn't doing it AFAIK, and I see your point.

Not very likely so far. Adding dependent types to the sort of uniqueness- and 'lifetime'/region-based typing that's used in Rust is very much a matter of research.

Can you give an example where you would use dependent types?

Critical embedded systems for avionics and robotics systems frequently deal with values that must be within a certain range. Runtime bounds checking can be too expensive in these environments and dependent types would allow for provably correct bounded integers without checks. That is actually a problem I am dealing with right now in some MIL-STD-1553 data bus code.

While I was at NASA I was advocating for using Rust instead of C/C++ and FORTRAN and many people were interested because of the safety/performance aspects. I think it would take some serious ground from them in that area with dependent types also.

Just to elaborate a bit more, the use of optional values rather than NULL is really a special case dependent types. It's saying that no type can contain a non-value. For another example, imagine subtracting something from an unsigned int. You need to ensure that the value never goes below zero If you have an expression like 'x - 1', then the compiler needs to ensure that x is always > 0.

The nice thing about this kind of static analysis for critical systems is that there are often extreme consequences if a runtime check fails. What do we do for the nuclear power control system when we detect an error? Crash? Shut down the system? But the system is not functioning properly. How do we know that we can safely shut it down? These are pretty horrible things to consider. It's much better to be able to say analytically that the situation can not happen.

I once worked in a high energy physics lab, though. There is always memory corruption to contend with, so you'll never be free of runtime errors ;-)

In the space of safety-critical software systems with tight constraints, Ada has typically been the go-to language. Together with the verification sub-language, SPARK, it can prove things like array bounds (and I assume integer bounds) are respected, without runtime checks. See e.g. https://www.adacore.com/gems/gem-68

The formal verification method used by SPARK is industry-proven (for decades). Dependent types are for the most part still an academic curiosity struggling to find industrial application. Of course they may very well do that, one day. But today, if you're working on safety-critical systems, I hope you take a close look at Ada+SPARK.

A classic example in Rust is to be generic over arrays. Arrays encode their length as part of the type; [T; N] is the type of an array of Ts that’s N elements long. In other words:

  fn foo<T>(array: [T; ?]) {
How do you define ? to work on any length?

When the RFC I referenced above is implemented, you’d write

  fn foo<T, const N>(array: [T; N]) {
and now you can call this function on arrays of varying lengths.

(In today’s Rust you’d use a slice instead, but that’s the simplest example I can give.)

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact