3 ms·

Will this make Rust's type system dependently typed like Agda or Idris?

• 3r8Oltr0ziouVDM 5y ago
  No, const generics only work with compile-time constants.
• lmkg 5y ago
  Const Generics are a form of dependent typing, but a heavily restricted one. This will loosen some restrictions, increasing what can be done with dependent types, but still a far cry from languages with "full" dependent types.
• ReleaseCandidat 5y ago
  No. To have dependent types the values the types depend on must be runtime constants, not compile time constants.
  • zozbot234 5y ago
    Strictly speaking, dependently-typed languages don't even have a clear-cut phase separation between "compile time" and "run time" (other than via "code extraction" to a non-dependently typed language as an add-on feature). It's clear however that the Rust const-generics 'MVP' is quite far from the flexibility of full dependent types.