4 ms·
Dependent types allow for more nuanced statements made by types. You can for instance have a lists that are sorted in ascending order as a type, or implement me
by Warwolt 4y ago
Dependent types allow for more nuanced statements made by types. You can for instance have a lists that are sorted in ascending order as a type, or implement messaging protocols at the type level where you can only construct a reply in the message exchange if you've received the correct preceding message.
It's very cool, but it's very expensive to compile, which is why it's still research stuff, I believe.
- kaba0 4y agoNot only “compile expensiveness”, but you quite literally have to prove your types in the program, which is seldom easy. E.g. if you were to write a merge sort, and have it in the type that it will output a sorted array, you will have a very hard time actually proving it correct, akin to algorithm analysis. Though to be fair most dependent typed languages allows for types without proofs, and having it in the type that an array is sorted for example can be valuable even without formal verification.