Hacker News Reader

Comment by alexashka | Hacker News Reader

Dependent types are a solution in search of a problem.

Widespread adoption comes from an easy to use, backed by big name, solution to a problem people have been having.

Typescript is a good example - it came with VS Code integration out of the box, and some decent tutorials. It solves the problem of catching dumb type mismatch bugs at compile time, gives jump-to-definition, auto-complete and doesn't cost anything, it's opt-in.

Those are killer usability features!

Dependent types give type theorists a place to try interesting things. That's about it so far.

Regarding invariant annotations - people call those tests :)

View on HN

Dependent types are an active area of research. They are one of several different avenues of research into program verification.

The problem is that both their proponents and detractors (as well as those of other verification approaches) confuse research and practice. Think of the field as early stages of pharmaceutical research; experiments in the lab show some promise as well as obstacles, but it's too early to tell which of the approaches, if any, would be able to work at a large scale in field conditions. As long as we don't confuse research and practice we can follow, enjoy and evaluate research on its own terms, rather than judging it based on criteria that may not be relevant at this stage. This is not to say that we cannot point out risks to field adoption, but research is research.

I, too, have my doubts about dependent types, but it's unfair to judge them harshly at this stage, when nobody knows how best to use them.

Maybe the typical "pedestrian" problems, like lists having non-zero length, or numbers being in a given range, can be checked statically with simpler means that full-on dependent types?

E.g. safe resource deallocaion problem can be seen as a dependent-type problem (only let an initialized resource into a deallocator), but is usually solved with sort-of linear types, or even simpler (though more crude) means.

Reply on news.ycombinator.com