Re:Haskell Problems for a New Decade
by pron on Tuesday February 04, 2020 @07:48PM
(#22242917)
> Not all non-research uses of dependent types are impractical.
That's like saying that a tank could get you to work, so some of its uses are practical for civilians. Does the weight of dependent types justify such disproportionate applicability?
> You could use many of the same arguments you’re making against dependent types against most programming language features. Why should a language have generics? Or first-class functions? Or even any kind of static typing whatsoever?
And those arguments would be just true, except that industry languages adopted those features many years after they've been tried in research languages and shown their worth, while industry languages didn't adopt other features (or perhaps haven't yet), because they didn't prove to be the right solutions to big problems. It's perfectly fine to adopt many ideas that are open research questions, but if you do so you can't deny that your goal is research.
> I think we should rather be discussing whether dependent types are useful for relatively simple applications, like providing type-safe database access or REST APIs in a library, rather than looking at them as tools for proving functional correctness.
No, because that's the inverted implication, or "tank" problem again. Just because a tank can get you to work doesn't mean that it should. If you want to achieve goal A, and feature B achieves it, i.e. B => A, you cannot conclude from that that you should adopt B. You're assuming A and B => A and concluding B. That just doesn't follow.
The question we're asking is whether A => B. We're not asking whether dependent types can be put to some practical use -- that's what researchers ask. We engineers ask what solution to our problem we should adopt (usually the least costly one).
That's like saying that a tank could get you to work, so some of its uses are practical for civilians. Does the weight of dependent types justify such disproportionate applicability?
> You could use many of the same arguments you’re making against dependent types against most programming language features. Why should a language have generics? Or first-class functions? Or even any kind of static typing whatsoever?
And those arguments would be just true, except that industry languages adopted those features many years after they've been tried in research languages and shown their worth, while industry languages didn't adopt other features (or perhaps haven't yet), because they didn't prove to be the right solutions to big problems. It's perfectly fine to adopt many ideas that are open research questions, but if you do so you can't deny that your goal is research.
> I think we should rather be discussing whether dependent types are useful for relatively simple applications, like providing type-safe database access or REST APIs in a library, rather than looking at them as tools for proving functional correctness.
No, because that's the inverted implication, or "tank" problem again. Just because a tank can get you to work doesn't mean that it should. If you want to achieve goal A, and feature B achieves it, i.e. B => A, you cannot conclude from that that you should adopt B. You're assuming A and B => A and concluding B. That just doesn't follow.
The question we're asking is whether A => B. We're not asking whether dependent types can be put to some practical use -- that's what researchers ask. We engineers ask what solution to our problem we should adopt (usually the least costly one).