|
|
|
|
|
|
by anon_d
2738 days ago
|
|
|
Right now the only thing that seems clear is that dependent typing adds significant mental burden on the programmer to more thoroughly specify types, and to do so absolutely correctly It's basically the opposite of this. If a language has dependent types, you can continue to use it in the same way as a language with does not have dependent types. BUT, there's a lot of programming patterns that previously couldn't be implemented in a type-safe way, that now can be. This also gives a ton of opportunities for libraries to implement abstractions that weren't expressible before. Dependent types are not that complicated, actually, and they don't add any burden to programs that don't use them. |
|
|