6 ms·

Very interesting to see that Rust's "const generics" can emulate some of the flagship use cases of dependently typed programming such as having the length of an

Very interesting to see that Rust's "const generics" can emulate some of the flagship use cases of dependently typed programming such as having the length of an array be part of it's static type!

mhh__ 6y ago
Isn't dependant types actually about being able to reason about the runtime value rather than at compile time i.e. D and C++ definitely don't have dependant types, or at least exciting kind.
- dathinab 6y ago
  > In computer science and logic, a dependent type is a type whose definition depends on a value. (source Wikipedia) So rusts const generics are (very limited) dependent types. C++ templates on the other hand you could argue are not types (but templates), but that is nit-picking. Weather or not dependent types are can be runtime evaluated often is a separate question then weather or not a language has dependent types. EDIT: The following part is partial nonsense, very POV dependent. I wanted to delete it but that wouldn't be right, so I just added this note. Through not allowing run-time creation of dependent types makes them much more limited in usability. But then allowing it requires either reflections (still likely very limited/slow/etc.), or part of the type being stored as a "magic" field of the type instance (fast but is that still a dependent type?), or a interpreted language).
  - yakubin 6y ago
    Are you saying you consider std::array<int, 5> in C++ to be a dependent type? I'm pretty sure it's not right. I'm pretty sure that the "value" in that quote is, implicitly, a "runtime value", or "value of a variable", similar to how we often say "type" without saying "type of a variable". This "5" isn't the value of a variable, it's just an expression. If you continue on to the next paragraph on this Wikipedia page, you will read, first: > The return type of a dependent function may depend on the value (not just type) of one of its arguments. For instance, a function that takes a positive integer n may return an array of length n, where the array length is part of the type of the array. second: > A dependent pair may have a second value of which the type depends on the first value. Sticking with the array example, a dependent pair may be used to pair an array with its length in a type-safe way. Generally, it's the same nomenclature as with the explanation of static vs dynamic type systems: in static type systems, types are attributes of variables, functions and expressions, whereas in dynamic type systems types are attributes of values. And in the static type system of C, 5 has type int, because it's an expression. It representing a value is secondary. A side effect of it is: you can write a compile-time constant in C that will overflow its type, because the type is assigned based on the lexical category, not on the value. As far as I understand, in a dependent type system it should be possible to implement a resizable array "std::vector<int, n>", where n is the length of the array (a variable), then write a "concat" function which concatenates two such arrays, and whose return (static) type depends on the lengths of the arrays passed as arguments. This is different than parametric polymorphism, such as the one that C++ has, since we can't know at compile-time all the possible lengths of arrays that we're going to get at runtime. Idris example here: https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.html#vectors https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.h... If someone has a better understanding of the topic, I'd be delighted to be shown wrong.
    - jcelerier 6y ago
      > As far as I understand, in a dependent type system it should be possible to implement a resizable array "std::vector<int, n>", where n is the length of the array (a variable), then write a "concat" function which concatenates two such arrays, and whose return (static) type depends on the lengths of the arrays passed as arguments. worksforme https://gcc.godbolt.org/z/x9GjE7KGM https://gcc.godbolt.org/z/x9GjE7KGM (ok, except the "resizeable" bit - but since we're doing functional programming we want immutable data structures, no ? :p)
      - yakubin 6y ago
        "n" is not a variable in your example. It's still just syntactic sugar for templates, where the n needs to be known statically. Even without the "resizable" bit, you still limit this function to operating on arrays of sizes known statically, which is a severe limitation, making the whole thing impractical.
  - mhh__ 6y ago
    > C++ templates on the other hand you could argue are not types (but templates), but that is nit-picking. Not only is it nitpicking, it seems wrong even in an academic sense of the term. Whether the template itself is a type or not probably depends on what theoretical language you use to discuss it. The template is monomorphized into a new type per instantiation, yes, but the moment it actually has a number in it it's a type. In D the template can quite happily accept pretty much anything as a parameter (particularly structs i.e. better code quality), and I'm surprised other languages don't allow this. Why have a bunch of template parameters on a line when you can just program the way you normally would.
    - steveklabnik 6y ago
      > I'm surprised other languages don't allow this. Rust doesn't (arbitrary values, anyway, const generics is the start of this being possible) because we don't have templates, we have generics. I agree if you're going with a template-based system, it makes a lot of sense to accept whatever, but if you aren't, then things are more complicated.
      - mhh__ 6y ago
        I think the typechecking here should be possible for rust in the sense that it's just a value of a known type (this isn't like C++ hacks). https://d.godbolt.org/z/Tb5jKv4ns https://d.godbolt.org/z/Tb5jKv4ns
        steveklabnik 6y ago
        It's possible, (and I think might even work on nightly? Don't have the time to check right this second) but is just a lot more work to support than in a template-based system, that's all. We'll get there!
- steveklabnik 6y ago
  I am a bit under-educated about the exact specifics here, but I should note that this feature was originally literally dependent types. * https://github.com/rust-lang/rfcs/pull/1657 https://github.com/rust-lang/rfcs/pull/1657 * https://github.com/rust-lang/rfcs/issues/1930 https://github.com/rust-lang/rfcs/issues/1930 * https://github.com/rust-lang/rfcs/pull/2000 https://github.com/rust-lang/rfcs/pull/2000 (the design that was accepted, in the end) (I am not actually 100% sure if rfc 2000 meets the by-the-book definition of "dependent types", my copy of Pierce has been collecting dust. Really gotta study up more on this stuff.)
  - mhh__ 6y ago
    Honestly I'm not totally sure either, however even if const-generics were technically dependant types enough to be called them with a straight face then I'm not sure if you get the benefits of them e.g. the textbook example seems to be static reasoning about the length of the result of appending two vectors of fixed but unknown lengths. The current proposal just seems like a convenient but theoretically shallow approximation of that due to the requirement of the const-parameter being known at compile time. One roundabout way of doing this - which is very much possible in D but not worth doing because you can't really do useful work with it for the most part due to pain - is that if you extend (say) const-generics to work with basically anything evaluable at compile time, you can build up a data structure to represent and hold true some predicate about a runtime value in a type (as a template/generic parameter), then define how these combine under binary operations (trivial so far in D at least, impossible in C++, no idea about Rust - monomorphization differences aside), then use this datastructure for evil and profit (like giving invariants to the optimizer). I would like to see how far the aforementioned idea can go, however it quickly becomes "write a compiler at compile time" or worse "write an SMT solver at compile time", both of which do not thrill me.
    - steveklabnik 6y ago
      That's why the feature flag was "min_const_generics", we do plan on extending it more in the future, but you have to start somewhere, and even this tiny, tiny slice gives a lot of power.
- Jhsto 6y ago
  I feel like the real question here is what will the semantics of a programming language with dependent types look like without enforcing of GADTs all the way, and whether it will work. That is, thanks to GADTs functional languages with dependent types -- in a sense -- make traditional runtime look like static since the type is non-constant while the checking is static (meaning, dependent operations over a variable returns a variable with redefined type, not possible now in Rust). This seems to be the main difference for now, as Rust the type is constant. Yet, this might very well be enough for practical usefulness -- with GADTs all the way you can reason about nice properties such as termination (sometimes) and certain mathematical interest such as generalisations of programming, but this is likely uninteresting for most. Rust might very well apply the same kind of golden middle road to dependent types as it did for linearity via affine types. Will be interesting how this evolves further!
planetis 6y ago
I have used them in another language and in practise, itsnt really a useful feature. Say you implement a fixed point type or a matrix, more often than not you end up needing arithmetic ops between different "resolutions" or matrix dimensions. That blows both how many generic functions you write and the generic instatiations. In the end you are better of with moving the parameters in runtime.
- humanafterall 6y ago
  I think you can get the benefits of type safety while still using type inference or macros to avoid type impl explosion

Very interesting to see that Rust's "const generics" can emulate some of the flagship use cases of dependently typed programming such as having the length of an array be part of it's static type!

mhh__ 6y ago

Isn't dependant types actually about being able to reason about the runtime value rather than at compile time i.e. D and C++ definitely don't have dependant types, or at least exciting kind.

dathinab 6y ago
> In computer science and logic, a dependent type is a type whose definition depends on a value. (source Wikipedia) So rusts const generics are (very limited) dependent types. C++ templates on the other hand you could argue are not types (but templates), but that is nit-picking. Weather or not dependent types are can be runtime evaluated often is a separate question then weather or not a language has dependent types. EDIT: The following part is partial nonsense, very POV dependent. I wanted to delete it but that wouldn't be right, so I just added this note. Through not allowing run-time creation of dependent types makes them much more limited in usability. But then allowing it requires either reflections (still likely very limited/slow/etc.), or part of the type being stored as a "magic" field of the type instance (fast but is that still a dependent type?), or a interpreted language).
- yakubin 6y ago
  Are you saying you consider std::array<int, 5> in C++ to be a dependent type? I'm pretty sure it's not right. I'm pretty sure that the "value" in that quote is, implicitly, a "runtime value", or "value of a variable", similar to how we often say "type" without saying "type of a variable". This "5" isn't the value of a variable, it's just an expression. If you continue on to the next paragraph on this Wikipedia page, you will read, first: > The return type of a dependent function may depend on the value (not just type) of one of its arguments. For instance, a function that takes a positive integer n may return an array of length n, where the array length is part of the type of the array. second: > A dependent pair may have a second value of which the type depends on the first value. Sticking with the array example, a dependent pair may be used to pair an array with its length in a type-safe way. Generally, it's the same nomenclature as with the explanation of static vs dynamic type systems: in static type systems, types are attributes of variables, functions and expressions, whereas in dynamic type systems types are attributes of values. And in the static type system of C, 5 has type int, because it's an expression. It representing a value is secondary. A side effect of it is: you can write a compile-time constant in C that will overflow its type, because the type is assigned based on the lexical category, not on the value. As far as I understand, in a dependent type system it should be possible to implement a resizable array "std::vector<int, n>", where n is the length of the array (a variable), then write a "concat" function which concatenates two such arrays, and whose return (static) type depends on the lengths of the arrays passed as arguments. This is different than parametric polymorphism, such as the one that C++ has, since we can't know at compile-time all the possible lengths of arrays that we're going to get at runtime. Idris example here: https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.html#vectors https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.h... If someone has a better understanding of the topic, I'd be delighted to be shown wrong.
  - jcelerier 6y ago
    > As far as I understand, in a dependent type system it should be possible to implement a resizable array "std::vector<int, n>", where n is the length of the array (a variable), then write a "concat" function which concatenates two such arrays, and whose return (static) type depends on the lengths of the arrays passed as arguments. worksforme https://gcc.godbolt.org/z/x9GjE7KGM https://gcc.godbolt.org/z/x9GjE7KGM (ok, except the "resizeable" bit - but since we're doing functional programming we want immutable data structures, no ? :p)
    - yakubin 6y ago
      "n" is not a variable in your example. It's still just syntactic sugar for templates, where the n needs to be known statically. Even without the "resizable" bit, you still limit this function to operating on arrays of sizes known statically, which is a severe limitation, making the whole thing impractical.
- mhh__ 6y ago
  > C++ templates on the other hand you could argue are not types (but templates), but that is nit-picking. Not only is it nitpicking, it seems wrong even in an academic sense of the term. Whether the template itself is a type or not probably depends on what theoretical language you use to discuss it. The template is monomorphized into a new type per instantiation, yes, but the moment it actually has a number in it it's a type. In D the template can quite happily accept pretty much anything as a parameter (particularly structs i.e. better code quality), and I'm surprised other languages don't allow this. Why have a bunch of template parameters on a line when you can just program the way you normally would.
  - steveklabnik 6y ago
    > I'm surprised other languages don't allow this. Rust doesn't (arbitrary values, anyway, const generics is the start of this being possible) because we don't have templates, we have generics. I agree if you're going with a template-based system, it makes a lot of sense to accept whatever, but if you aren't, then things are more complicated.
    - mhh__ 6y ago
      I think the typechecking here should be possible for rust in the sense that it's just a value of a known type (this isn't like C++ hacks). https://d.godbolt.org/z/Tb5jKv4ns https://d.godbolt.org/z/Tb5jKv4ns
      - steveklabnik 6y ago
        It's possible, (and I think might even work on nightly? Don't have the time to check right this second) but is just a lot more work to support than in a template-based system, that's all. We'll get there!
steveklabnik 6y ago
I am a bit under-educated about the exact specifics here, but I should note that this feature was originally literally dependent types. * https://github.com/rust-lang/rfcs/pull/1657 https://github.com/rust-lang/rfcs/pull/1657 * https://github.com/rust-lang/rfcs/issues/1930 https://github.com/rust-lang/rfcs/issues/1930 * https://github.com/rust-lang/rfcs/pull/2000 https://github.com/rust-lang/rfcs/pull/2000 (the design that was accepted, in the end) (I am not actually 100% sure if rfc 2000 meets the by-the-book definition of "dependent types", my copy of Pierce has been collecting dust. Really gotta study up more on this stuff.)
- mhh__ 6y ago
  Honestly I'm not totally sure either, however even if const-generics were technically dependant types enough to be called them with a straight face then I'm not sure if you get the benefits of them e.g. the textbook example seems to be static reasoning about the length of the result of appending two vectors of fixed but unknown lengths. The current proposal just seems like a convenient but theoretically shallow approximation of that due to the requirement of the const-parameter being known at compile time. One roundabout way of doing this - which is very much possible in D but not worth doing because you can't really do useful work with it for the most part due to pain - is that if you extend (say) const-generics to work with basically anything evaluable at compile time, you can build up a data structure to represent and hold true some predicate about a runtime value in a type (as a template/generic parameter), then define how these combine under binary operations (trivial so far in D at least, impossible in C++, no idea about Rust - monomorphization differences aside), then use this datastructure for evil and profit (like giving invariants to the optimizer). I would like to see how far the aforementioned idea can go, however it quickly becomes "write a compiler at compile time" or worse "write an SMT solver at compile time", both of which do not thrill me.
  - steveklabnik 6y ago
    That's why the feature flag was "min_const_generics", we do plan on extending it more in the future, but you have to start somewhere, and even this tiny, tiny slice gives a lot of power.
Jhsto 6y ago
I feel like the real question here is what will the semantics of a programming language with dependent types look like without enforcing of GADTs all the way, and whether it will work. That is, thanks to GADTs functional languages with dependent types -- in a sense -- make traditional runtime look like static since the type is non-constant while the checking is static (meaning, dependent operations over a variable returns a variable with redefined type, not possible now in Rust). This seems to be the main difference for now, as Rust the type is constant. Yet, this might very well be enough for practical usefulness -- with GADTs all the way you can reason about nice properties such as termination (sometimes) and certain mathematical interest such as generalisations of programming, but this is likely uninteresting for most. Rust might very well apply the same kind of golden middle road to dependent types as it did for linearity via affine types. Will be interesting how this evolves further!

planetis 6y ago

I have used them in another language and in practise, itsnt really a useful feature. Say you implement a fixed point type or a matrix, more often than not you end up needing arithmetic ops between different "resolutions" or matrix dimensions. That blows both how many generic functions you write and the generic instatiations. In the end you are better of with moving the parameters in runtime.

humanafterall 6y ago
I think you can get the benefits of type safety while still using type inference or macros to avoid type impl explosion