3 ms·
Rust has some libraries that can do dependent typing too, based on macros. For example: https://youtube.com/watch?v=JtYyhXs4t6w https://youtube.com/watch?v=JtYy
by satvikpendem 9mo ago
Rust has some libraries that can do dependent typing too, based on macros. For example: https://youtube.com/watch?v=JtYyhXs4t6w https://youtube.com/watch?v=JtYyhXs4t6w
Which refers to https://docs.rs/anodized/latest/anodized/ https://docs.rs/anodized/latest/anodized/
- hmry 9mo agoVery 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] }
- satvikpendem 9mo agoSadly I'm not sure Rust will ever get those sorts of features.
- hmry 9mo agoThey'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)