5 ms·

Can you elaborate upon in which domains that power is worth it? And when it is not?

• tel 12y ago
  As a polarizing example—proof assistants use dependent typing. Their goal is to express interesting mathematical theorems as types and then finding typechecking programs constitutes as proof of those theorems. They absolutely want power and richness over inference---you probably wouldn't want to write a program with an inferable type anyway. It would be too boring.