2 ms·

Dependent types are not just useful for proving correctness properties, and in fact I think dependent types in Haskell are not really intended to prove really c

Dependent types are not just useful for proving correctness properties, and in fact I think dependent types in Haskell are not really intended to prove really complex properties, like the full functional correctness of a compiler. Hence, I think the use of Coq or Agda proofs as an example of impracticality is a strawman argument. You might need a research team and several years to show the correctness of an operating system in Coq. You do not need that to have type-safe database access or statically checked matrix sizes. Not all non-research uses of dependent types are impractical. 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? Should Java not have added lambdas because it already had anonymous inner classes? You can clearly get by just fine in a lot of business applications without some of these features. 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. It’s not so clear that dependent types are too complex a solution there, especially if you look at a library like Servant, which already uses some advanced type system features, and which is actually a really practical library that is probably used in production applications as well. A library like Servant might be able to expressed more clearly with dependent types than with a hodgepodge of type system extensions. I think that wanting type-safe REST API access is already an order of magnitude more practical than model checking kernel code.

pron 7y ago
> 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).

pron 7y ago

> 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).