5 ms·

I thought dependent types were types that depended on a value? What they are proposing are types that depend on types or compile time constants.

zozbot234 2y ago
The problem is combining the "const generic" and "expression" part. If your "compile time constants" can actually be complex expressions, you arguably end up with the same kind of generality as dependent types. This is true even for expressions that are only evaluated in a compile-time context, since dependently-typed languages do "everything" at compile time anyway, they don't have a phase distinction where you can talk about "runtime" being separate.
- galangalalgol 2y ago
  Ah, yeah! I get it now. So c++ is a dependently typed language. That is hilarious. I want lisp syntax in c++29. That said, too many features are blocked on const generic expressions, so I think they are going to have to bite that off. There is already talk about migrating proceduralacros to be something more like normal rust, this moght fit in with that.
  - Rusky 2y ago
    C++ is not a dependently typed language, for the same reason that templates do not emit errors until after they are instantiated. All non-type template parameters get fully evaluated at instantiation time so they can be checked concretely. A truly dependently typed language performs these checks before instantiation time, by evaluating those expressions abstractly. Code that is polymorphic over values is checked for all possible instantiations, and thus its types can actually depend on values that will not be known until runtime. The classic example is a dynamic array whose type includes its size- you can write something like `concat(vector<int, N>, vector<int, M>) -> vector<int, N + M>` and call this on e.g. arrays you have read from a file or over the network. The compiler doesn't care what N and M are, exactly- it only cares that `concat` always produces a result with the length `N + M`.
    - zozbot234 2y ago
      > performs these checks before instantiation time Notably Rust type-based generics do this, a key difference wrt. C++ templates. (You can use macros if you want checks after instantiation, of course.)
    - groos 2y ago
      I'm not sure what "dependently typed" means but in C++20 and beyond, concepts allow templates to constrain their parameters and issue errors for the templates when they're specialized, before the actual instantiation happens. E.g., a function template with constraints can issue errors if the template arguments (either explicit or deduced from the call-site) don't satisfy the constraints, before the template body is compiled. This was not the case before C++20, where some errors could be issued only upon instantiation. With C++20, in theory, no template needs to be instantiated to validate the template arguments if constraints are provided to check them at specialization-time.
      - Rusky 2y ago
        This is the wrong side of the API to make C++20 dependently typed. Concepts let the compiler report errors at the instantiation site of a template, but they don't do anything to let the compiler report errors with the template definition itself (again before instantiation time). To be clear this distinction is not unique to dependent types, either. Most languages with some form of generics or polymorphism check the definition of the generic function/type/etc against the constraints, so the compiler can report errors before it ever sees any instantiations. This just also happens to be a prerequisite to consider something "dependently typed."
    - jcelerier 2y ago
      the only thing needed here is to be able to lift N & M from run-time to the type system (which in C++ as it stands exists only at compile-time). For "small" values of N&M that's doable with switches and instantiations for instance.
      - Rusky 2y ago

zozbot234 2y ago

The problem is combining the "const generic" and "expression" part. If your "compile time constants" can actually be complex expressions, you arguably end up with the same kind of generality as dependent types. This is true even for expressions that are only evaluated in a compile-time context, since dependently-typed languages do "everything" at compile time anyway, they don't have a phase distinction where you can talk about "runtime" being separate.

galangalalgol 2y ago
Ah, yeah! I get it now. So c++ is a dependently typed language. That is hilarious. I want lisp syntax in c++29. That said, too many features are blocked on const generic expressions, so I think they are going to have to bite that off. There is already talk about migrating proceduralacros to be something more like normal rust, this moght fit in with that.
- Rusky 2y ago
  C++ is not a dependently typed language, for the same reason that templates do not emit errors until after they are instantiated. All non-type template parameters get fully evaluated at instantiation time so they can be checked concretely. A truly dependently typed language performs these checks before instantiation time, by evaluating those expressions abstractly. Code that is polymorphic over values is checked for all possible instantiations, and thus its types can actually depend on values that will not be known until runtime. The classic example is a dynamic array whose type includes its size- you can write something like `concat(vector<int, N>, vector<int, M>) -> vector<int, N + M>` and call this on e.g. arrays you have read from a file or over the network. The compiler doesn't care what N and M are, exactly- it only cares that `concat` always produces a result with the length `N + M`.
  - zozbot234 2y ago
    > performs these checks before instantiation time Notably Rust type-based generics do this, a key difference wrt. C++ templates. (You can use macros if you want checks after instantiation, of course.)
  - groos 2y ago
    I'm not sure what "dependently typed" means but in C++20 and beyond, concepts allow templates to constrain their parameters and issue errors for the templates when they're specialized, before the actual instantiation happens. E.g., a function template with constraints can issue errors if the template arguments (either explicit or deduced from the call-site) don't satisfy the constraints, before the template body is compiled. This was not the case before C++20, where some errors could be issued only upon instantiation. With C++20, in theory, no template needs to be instantiated to validate the template arguments if constraints are provided to check them at specialization-time.
    - Rusky 2y ago
      This is the wrong side of the API to make C++20 dependently typed. Concepts let the compiler report errors at the instantiation site of a template, but they don't do anything to let the compiler report errors with the template definition itself (again before instantiation time). To be clear this distinction is not unique to dependent types, either. Most languages with some form of generics or polymorphism check the definition of the generic function/type/etc against the constraints, so the compiler can report errors before it ever sees any instantiations. This just also happens to be a prerequisite to consider something "dependently typed."
  - jcelerier 2y ago
    the only thing needed here is to be able to lift N & M from run-time to the type system (which in C++ as it stands exists only at compile-time). For "small" values of N&M that's doable with switches and instantiations for instance.
    - Rusky 2y ago