3 ms·
It's a practical need. It allows for the compiler to enhance your productivity by stopping mistakes and errors as soon as possible. For instance, you can't eve
by valenterry 4y ago
It's a practical need. It allows for the compiler to enhance your productivity by stopping mistakes and errors as soon as possible.
For instance, you can't even write a generic "window slide" function support dynamic window length without this typelevel logic. Except of course if you don't mind your program to blow up on a mistake or write excessive tests for every piece of your code.
- kaba0 4y agoWell, can it spot race conditions? Or will it suddenly solve the halting problem? Safety is not a binary value. Dependent types can increase safety, though they do come with a significant cost, which may very well be spent on additional testing, indeed.
- valenterry 4y ago> Safety is not a binary value Exactly. Encoding logic in types doesn't have to fix all problems all the time. It's sufficient if advantages outweight the costs.