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) …
I'm thinking the right mental model for this is: "what if a type was a primitive". E.g. you can pass a type into a function, and make it produce a new type. Aka "type functions". (Okay, that's as far as I've made sense of it).
-
-
This may not make sense yet but.. a type function is any type that is generic (e.g. Vec is a type function). Dependent types is when you have type functions that can take *values* - the types depend on the values
-
For example, a Vec<T, Len> is a function of (type, integer) -> type
- 3 more replies
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.