4 ms·

They add significant complexity to the language and are intended to help with correctness. Not exactly -- they're intended to help with reasoning about the str

They add significant complexity to the language and are intended to help with correctness. Not exactly -- they're intended to help with reasoning about the structure of programs and hopefully reject the obviously wrong ones. Correctness would still require a more formal system of validation. Whether this is more easily achieved in a language like Haskell is still an open question. The LiquidHaskell team and Synquid project are both very interesting. In a Haskell program the compiler trivially rejects programs that fail to provide a branch for a missing case. I can reason about the scope of what a function can do (and what it cannot) based on it's type information. I can reason about an equation in familiar terms of substitution and composition. Types don't automatically ensure my program is correct, for some vague notion of correctness. Either way, it's not a language that's designed to solve a problem for practitioners If I am right to assume that practitioners are programmers then I have to disagree with the premise here. I am not a researcher. I write software for factories to help real people I've met face to face solve real problems. I have solved pragmatic, real-world problems by writing programs with Haskell and it was a productive, novel experience. The feature I recently shipped to production has migrated nearly a million schema-less JSON documents to a well-defined schema, continuously back-fills the new table from an AWS Lambda function when we receive data in the old format, and was largely only possible to do in such a short amount of time because of the features of Haskell's type system. I haven't had a single bug report or failure in 5 months to boot. To compare: every single Javascript service we've shipped to production in the last three years, despite all of the testing, validation, and effort we put in to getting it right has at least one production error within three months. Tolerance for these failures has to be built into everything we do. Haskell is not only suited for research. It is used in Facebook and Github. It has plenty of industrial uses and is definitely designed for and with the aid of practitioners. It's development is largely supported by volunteers: practitioners and researchers alike. It may not be popular but all it takes is one startup to choose it as their basis to change the conversation. The Viaweb team chose Lisp, arguably as obscure as Haskell at the time, and did great work. As for dependent types the why is simple: we can express richer specifications in the type system. It would enable Haskell to use a uniform language for terms and types. For programmers the simplest, minimal example are sized vectors as types. You can pass around a vector in Haskell that is sized so that out-of-bounds access is not possible. However the size of the vector is opaque at the type level. With a dependently-typed vector you could specify the bounds of the vector your algorithm supports which further reduces cases where a programmer mistakenly uses your function for unbounded inputs. This is only the minimal example but dependently typed languages scale up from there: there are research languages that have implemented full-on interactive theorem provers and libraries that can encode the whole of mathematical research and knowledge in them: Lean and mathlib. I firmly believe this is where programming is going to go. Dependently typed languages are the next step. I started writing a guide for interested hackers to get started writing real, working programs in a research-heavy dependently-typed programming language called Lean which you can find here: https://agentultra.github.io/lean-for-hackers/ https://agentultra.github.io/lean-for-hackers/ I suggest giving it a shot before condemning Haskell so easily. There's a lot of promise here. And in my experience, selling Haskell is a lot easier than selling formal verification, fwiw. Hardly anyone uses TLA+ compared to Haskell. And I spend a fair amount of time and energy trying to sell both.

pron 7y ago
> working programs in a research-heavy dependently-typed programming language called Lean which you can find here I have used Lean. It's nice and intersting, but not really a useful tool for software correctness intended for use by engineers. You can do some very interesting math with it, though. > As for dependent types the why is simple: we can express richer specifications in the type system. Sure, but why? Expressing richer specifications in the type systems also has a significant cost. A language whose goal is not research would likely spend years considering whether this is a good idea or not. > I suggest giving it a shot before condemning Haskell so easily. There's a lot of promise here. I have, and I don't think it's bad, I just don't particularly like it, for the same reasons some people don't particularly like Python or Java. I certainly don't think you can't use it for practical applications, but its evolution is, without a doubt, guided by research goals. And when it comes to promise, I don't know how many decades one can reasonably believe that. Haskell doesn't even spread in companies that are already using it, unlike languages that have contributed a significant bottom-line advantage, and it shows virtually no growth after 25 years, in many of them it was highly hyped. I have absolutely no problem with people who like it. Programming language preference is a matter of personal taste; I like Java, Clojure, Eve, ML and Zig, not crazy about Haskell, and dislike Scala, and others like Haskell and dislike the languages I like; it's perfectly reasonable and expected, like taste in music. But you cannot claim it's a language designed for practitioners and yet have its features guided by research questions.
- agentultra 7y ago
  Thanks for being generous with my long post. > Sure, but why? I already explained why. Why do you even care about Haskell at all? > Expressing richer specifications in the type systems also has a significant cost. And everything that has a cost should have a benefit or we would abandon the whole enterprise. The simply typed lambda calculus will be 80 years old this year, in June. What was Church going after when he published it to the Journal of Symbolic logic? If you go back and read it he was trying to make sense of the lambda calculus. That calculus gave us one branch of computing as we know it but it was not sufficiently expressive enough to make logical statements about different classes of functions: not all functions that have the same shape have the same meaning. In a similar fashion not all programs are created equal. Given a set of functional requirements by a person we can probably independently write programs that satisfy them. Type theory is simply a means for us to reason about these programs. Whether you write your program that enables you to verify the internal correctness of your programs with respect to the type system used to check it or not doesn't matter one bit to the user of the system. To the programmer however, it can matter a great deal. Of the programs we could write in languages that don't allow us to verify the correctness of our programs with respect to a particular type theory all we can say is: when I evaluated the program with these inputs at this time, it worked. We can be reasonably certain it will continue to work and it will likely work on more inputs. Of the programs we write in a language that does allow us to verify the program is logically consistent and sound with respect to a particular type theory is that it is consistent. We would still be obligated to prove that the program meets the specified requirements. But we don't have to worry about whether we forgot to handle a branch, access data that isn't there, over write data we didn't intend to... and a whole slew of things that do plague us in languages without such tools. We can instead focus our effort on proving that we meet the requirements which is a much smaller and more tractable problem. As an engineer I don't see the reason why theory and research must be separate. I see my work as sitting between both worlds: theory informs application which in turn gives me more problems to inform the direction to go. > I just don't particularly like it, for the same reasons some people don't particularly like Python or Java. That's fair, I don't particularly like Java either. But I don't go into threads about Java and ask Java developers why they bother with it. Some of the challenges posted by Stephan are legitimately interesting challenges for Haskell programmers. A dependently typed Haskell would, ironically, make Haskell a more simple language and allow us to continue pushing type-driven programming further for many of the benefits I've described. Many of the benefits to these issues have been described in the article. > it shows virtually no growth after 25 years I beg to differ. Even after 10 years it has shown a lot of growth. TFA opens with celebrating the advances made in the last decade. The reason why Haskell isn't as popular as many mainstream languages, if it's so great, is network effects. Javascript is as popular as it is because it was the only language available for a long, long time on a platform many people wanted to write software for. Ruby would not even be on the radar if it wasn't for it's killer app: Rails. I dabbled in Ruby before Rails came along -- it was super obscure -- but no matter how good it was without Rails it would have languished in obscurity, I think. Some languages became popular by sheer force: Java was a solution in search of a problem and Oracle had a war chest to make sure people thought about it. I recall a time with Python was incredibly rare and obscure and had similar network effects to over-come. Haskell doesn't have a company or group of companies pumping millions of dollars into its development, is not a platform exclusive, and so far hasn't had a killer application where it excelled over other incumbents (except perhaps in compilers). It also doesn't help that many programmers continue to persist FUD about Haskell for reasons I don't understand. Similar to how people feel justified for being contemptuous of Javascript or PHP I suppose. However if Haskell was the platform-exclusive language of the web for several decades I think this conversation would be completely different. Haskell is a fine language and the reasons for working on effect systems are good ones and I'm excited to see the results. If you don't get why then try harder to understand the work or find something constructive to say about it. The people working on it are brilliant and have good, practical reasons for it.

pron 7y ago

> working programs in a research-heavy dependently-typed programming language called Lean which you can find here I have used Lean. It's nice and intersting, but not really a useful tool for software correctness intended for use by engineers. You can do some very interesting math with it, though. > As for dependent types the why is simple: we can express richer specifications in the type system. Sure, but why? Expressing richer specifications in the type systems also has a significant cost. A language whose goal is not research would likely spend years considering whether this is a good idea or not. > I suggest giving it a shot before condemning Haskell so easily. There's a lot of promise here. I have, and I don't think it's bad, I just don't particularly like it, for the same reasons some people don't particularly like Python or Java. I certainly don't think you can't use it for practical applications, but its evolution is, without a doubt, guided by research goals. And when it comes to promise, I don't know how many decades one can reasonably believe that. Haskell doesn't even spread in companies that are already using it, unlike languages that have contributed a significant bottom-line advantage, and it shows virtually no growth after 25 years, in many of them it was highly hyped. I have absolutely no problem with people who like it. Programming language preference is a matter of personal taste; I like Java, Clojure, Eve, ML and Zig, not crazy about Haskell, and dislike Scala, and others like Haskell and dislike the languages I like; it's perfectly reasonable and expected, like taste in music. But you cannot claim it's a language designed for practitioners and yet have its features guided by research questions.

agentultra 7y ago
Thanks for being generous with my long post. > Sure, but why? I already explained why. Why do you even care about Haskell at all? > Expressing richer specifications in the type systems also has a significant cost. And everything that has a cost should have a benefit or we would abandon the whole enterprise. The simply typed lambda calculus will be 80 years old this year, in June. What was Church going after when he published it to the Journal of Symbolic logic? If you go back and read it he was trying to make sense of the lambda calculus. That calculus gave us one branch of computing as we know it but it was not sufficiently expressive enough to make logical statements about different classes of functions: not all functions that have the same shape have the same meaning. In a similar fashion not all programs are created equal. Given a set of functional requirements by a person we can probably independently write programs that satisfy them. Type theory is simply a means for us to reason about these programs. Whether you write your program that enables you to verify the internal correctness of your programs with respect to the type system used to check it or not doesn't matter one bit to the user of the system. To the programmer however, it can matter a great deal. Of the programs we could write in languages that don't allow us to verify the correctness of our programs with respect to a particular type theory all we can say is: when I evaluated the program with these inputs at this time, it worked. We can be reasonably certain it will continue to work and it will likely work on more inputs. Of the programs we write in a language that does allow us to verify the program is logically consistent and sound with respect to a particular type theory is that it is consistent. We would still be obligated to prove that the program meets the specified requirements. But we don't have to worry about whether we forgot to handle a branch, access data that isn't there, over write data we didn't intend to... and a whole slew of things that do plague us in languages without such tools. We can instead focus our effort on proving that we meet the requirements which is a much smaller and more tractable problem. As an engineer I don't see the reason why theory and research must be separate. I see my work as sitting between both worlds: theory informs application which in turn gives me more problems to inform the direction to go. > I just don't particularly like it, for the same reasons some people don't particularly like Python or Java. That's fair, I don't particularly like Java either. But I don't go into threads about Java and ask Java developers why they bother with it. Some of the challenges posted by Stephan are legitimately interesting challenges for Haskell programmers. A dependently typed Haskell would, ironically, make Haskell a more simple language and allow us to continue pushing type-driven programming further for many of the benefits I've described. Many of the benefits to these issues have been described in the article. > it shows virtually no growth after 25 years I beg to differ. Even after 10 years it has shown a lot of growth. TFA opens with celebrating the advances made in the last decade. The reason why Haskell isn't as popular as many mainstream languages, if it's so great, is network effects. Javascript is as popular as it is because it was the only language available for a long, long time on a platform many people wanted to write software for. Ruby would not even be on the radar if it wasn't for it's killer app: Rails. I dabbled in Ruby before Rails came along -- it was super obscure -- but no matter how good it was without Rails it would have languished in obscurity, I think. Some languages became popular by sheer force: Java was a solution in search of a problem and Oracle had a war chest to make sure people thought about it. I recall a time with Python was incredibly rare and obscure and had similar network effects to over-come. Haskell doesn't have a company or group of companies pumping millions of dollars into its development, is not a platform exclusive, and so far hasn't had a killer application where it excelled over other incumbents (except perhaps in compilers). It also doesn't help that many programmers continue to persist FUD about Haskell for reasons I don't understand. Similar to how people feel justified for being contemptuous of Javascript or PHP I suppose. However if Haskell was the platform-exclusive language of the web for several decades I think this conversation would be completely different. Haskell is a fine language and the reasons for working on effect systems are good ones and I'm excited to see the results. If you don't get why then try harder to understand the work or find something constructive to say about it. The people working on it are brilliant and have good, practical reasons for it.