Currently reading up on Idris. Dependent types are really cool! Imagine you take an vec of len 2, and a vec of len 3. In Idris the type system is able to express that the return type is a vector that has the length of the two combined! Super interesting https://en.wikipedia.org/wiki/Idris_(programming_language) …
Wait, wait — so am I understanding you correctly then Rust already has this right? I somehow thought it would depend on adding higher kinded types first somehow, haha.
-
-
Type functions are the “simplest” step. Then you add higher kinded polymorphism and dependent types to that. Rust only went the first step
-
Ahh okay, that makes sense! Thanks for the explanation
End of conversation
New conversation -
-
-
Rust has type functions but not yet ones that can have values as inputs. You can write Foo<i32, String> but not Foo<5, String>
-
Ahh cool! Gotcha :D
- 1 more reply
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.