Comment by satvikpendem
5 days ago
Rust has some libraries that can do dependent typing too, based on macros. For example: https://youtube.com/watch?v=JtYyhXs4t6w
Which refers to https://docs.rs/anodized/latest/anodized/
5 days ago
Rust has some libraries that can do dependent typing too, based on macros. For example: https://youtube.com/watch?v=JtYyhXs4t6w
Which refers to https://docs.rs/anodized/latest/anodized/
Very cool and practical, but specs aren't dependent typing. (I actually think specs are probably more useful than dependent types for most people)
Dependent typing requires:
- Generic types that can take runtime values as parameters, e.g. [u8; user_input]
- Functions where the type of one parameter depends on the runtime value of another parameter, e.g. fn f(len: usize, data: [u8; len])
- Structs/tuples where the type of one field depends on the runtime value of another field, e.g. struct Vec { len: usize, data: [u8; self.len] }
Sadly I'm not sure Rust will ever get those sorts of features.
They've gone the Haskell route of adding a billion features to a non-dependent type system instead.
Not that I blame them, nobody has figured out practical dependent typing yet. (Idris is making good progress in the field though)