| > Why then do you think at a certain point they start hurting Oh, it's just a guess, but partly because of Haskell and its success at being continuously rejected by the industry for two decades now (it was touted as the next big thing when I was at university over 15 years ago). There have been few if any languages of Haskell fame that have clearly tried to break out of academia and have had so little use in the industry. And the problem is less with types themselves but with the referential-transparency-everywhere and non-strict-evaluation approach. The result is that Haskell allows -- nay, demands -- a lot of reasoning about the program upfront at the expense of reasoning about it as it runs, with a debugger and a profiler (because of the complicated execution model). I also think Haskell places an unreasonable burden of thinking about the types vs. the algorithm an domain. As to Scala, because it's such a "multi-paradigm" language, it's pretty hard to know exactly how it's used in the industry. There are certainly those that use it anywhere between Haskell-like with scalaz to Java-like only without having to write constructors and getters (in fact, Spark is written, I believe, closer in the latter style). But even if Scala is to be counted as an advocate for rich typing, its success record is pretty spotty (and, again, I wouldn't blame that necessarily on the type system). I could, of course, be very wrong. One thing is certain: what a type system can do is a comp-sci question; how useful it is is a psychological question, and trying to argue about the usefulness of type systems (or any programming approach) as if it were a mathematical problem is just silly. > We've certainly never reached that "certain point" where they start hurting. I think Haskell is beyond that point, although I still believe a language with a type system as sophisticated as Haskell's might not be (because getting more for the same price might be worth it). By that I mean that Haskell types -- just like the article said -- waste a lot of mental power in the wrong places (i.e. on proving trivial stuff). I don't know what that imagined language would look like, but it would probably have some effect types (and like the author of the article has noted, there's a huge difference between being able to simulate effect systems and effect systems controlling actual effects). |
When you are encoding your logic in types the distinction between types and "the algorithm and domain" is very blurred if not the exact same thing. I wouldn't want to be programming in any other language if I knew very little about the domain.