3 ms·

> Provided that you think that the only significant drawback is the learning curve. No, you misread me. I acknowledge other significant drawbacks, such as imm

by tome 11y ago

> Provided that you think that the only significant drawback is the learning curve. No, you misread me. I acknowledge other significant drawbacks, such as immaturity of tooling and infrastructure. > I think that the PFP abstraction itself is a drawback, and that you can get most of Haskell's benefits (leaving aside their real-world value for a moment) without it. OK, that would be great! I am genuinely interested in understanding how to do that. I would love to see PFP as a drawback and obtain its benefits without requiring its rigors. So far I have failed to understand your ideas about how to do that and I can only continue to see PFP as a massive boon. > In particular, I think that you cannot point at any real-world benefits of the Haskell approach over, say, the OCaml approach, and that's even before applying things like effect systems to OCaml. (One of) the real-world benefit(s) is that I can write a substantial part of a program and know from inspecting only a single line (its type signature) what effects it performs. How can OCaml give me that benefit? > What you don't get to do is say, "Haskell leads to code with significantly fewer serious bugs" while at the same time not show any evidence that it does. The reason you don't get to do that is that such a claim is one with serious (theoretical and financial) implications, and strong claims require strong evidence (or at least some more convincing evidence than what we have). I think that says more about how you interpret informal comments on the internet than it does about those making the comments. > > Furthermore, I wouldn't trust any empirical research on languages any more than I would trust empirical research on cholesterol > OK, but you're saying that I should go full vegan based on even less than that. Interesting. Where did I say you should go (the equivalent of) "full vegan"? > > It's not ideal, but it's also not wrong. > How do you know it's not wrong? At least, it is not known to be wrong. > But let me refine this. [... snipped useful elucidation ...] > At this point in time, all we can say about Haskell is this: some people greatly enjoy Haskell's programming paradigm; some people report possibly significant but not big gains in the handful of medium-to-large production projects where the language has been used. So far the approach is showing some (though not great) promise and requires further consideration. Entirely agreed. I think my gripe with you at this point is that you read too much in to people's informal claims and cause unnecessary aggravation by derailing threads. It's quite clear that you could actually contribute constructively, so I wish you would. Please can you explain in detail how I can get the benefits of PFP without its drawbacks?

pron 11y ago
> I would love to see PFP as a drawback and obtain its benefits without requiring its rigors. > (One of) the real-world benefit(s) is that I can write a substantial part of a program and know from inspecting only a single line (its type signature) what effects it performs. How can OCaml give me that benefit? That's a property, not a real-world benefit. It's like saying that one of the real-world benefits of Haskell is that its logo is green. In any case, don't know about OCaml, but in Java I just click a button, and get the call tree for the method (or, inversely, get the reverse tree for all methods eventually calling printf). More to the point, see some of Oleg Kiselyov's work on type systems for continuations here: http://okmij.org/ftp/continuations/ http://okmij.org/ftp/continuations/ > I think that says more about how you interpret informal comments on the internet than it does about those making the comments. I think that you should decide whether this is a serious discussion or grandstanding. > Where did I say you should go (the equivalent of) "full vegan"? Maybe you didn't say that I should, but you did say that it's better to be vegan (i.e. make a very significant "lifestyle" change without any evidence to its effectiveness). > At least, it is not known to be wrong. That's true. But I wouldn't go around telling people that being vegan has great health benefit if all we know is that it's not been found to kill you. > I would love to see PFP as a drawback and obtain its benefits without requiring its rigors. So far I have failed to understand your ideas about how to do that and I can only continue to see PFP as a massive boon. OK, but first, a few things: 1/ I don't know if by "rigors" you meant difficulties or rigorousness, but if the latter, then I don't see why you conflate rigor with the pure-functional abstraction. Most formally verified, safety-critical software is written in languages that are far more rigorous than Haskell, yet are not pure-functional. Which leads us to 2/ these are not "my ideas"; if correctness is your goal (as it seems to be), most languages guaranteeing correctness do not espouse the PFP abstractions. Haskell, Coq, Idris and Agda are used far less than other approaches to ensuring software correctness. Finally, 3/ I'd like to be careful when I say "benefits", because we don't know whether they are true benefits, neutral or even detrimental to software at large. All I can say that in this context, when I say "benefits" I mean things that I (and you) believe to be positive and see as potentially advantageous in the "real world". Now, I will give you two examples (of languages used more than Haskell/Coq etc.) for "correct" languages, both of them are very rigorous in the sense of being completely formal, yet they do not suffer from PFP's downsides mainly by being measurably much easier to learn/teach/adopt. They are not generally applicable, but neither is Haskell. The first is the set of synchronous langauges, now used by the industry to design safety-critical realtime software, as well as a lot of hardware. Instead of PFP, it relies on what's known as the "synchronous hypothesis". It has been proven over three decades, as an effective, practical method of writing verifiably correct software by "plain" engineers in hundreds of critical real-world systems. You can read more about it here[1]. A generalization of the approach is called Globally Asynchronous, Locally Synchronous, or GALS, and I believe it has the potential of being a great, more widely applicable way of writing software in a way that lends itself to careful reasoning. The second (you probably saw it coming), is TLA+. It's not a programming language, so I won't compare it to Haskell but to Coq. Unlike Coq, TLA+ does not rely on PFP, or Curry-Howard (neither do other verification tools, like Isabelle) but goes a step further in not being typed at all. It is not functional yet fully mathematical ("referentially transparent"), and its main advantage is that while having the same "proving strength" as Coq when it comes to verifying algorithms[2] while taking days to learn instead of months, and not requiring any mathematical background more than what any engineer already has. I guess that the answer to "how?" would be "in a manner bearing a lot of resemblance to the synchronous hypothesis". There are, of course, other formal approaches (like CSP), but synchronous programming in particular has had a lot of success in the industry. If you want to know about (typed) monads vs. continuations, and their relationship to typed effects, I'll refer you again to my blog post on the subject: http://blog.paralleluniverse.co/2015/08/07/scoped-continuations/ http://blog.paralleluniverse.co/2015/08/07/scoped-continuati... and to Oleg Kiselyov's work, which I've linked to above. [1]: http://link.springer.com/chapter/10.1007%2F978-3-319-11737-9_15 http://link.springer.com/chapter/10.1007%2F978-3-319-11737-9... [2]: Coq may be more powerful when proving general mathematical theorems, but Coq was designed as a general theorem prover, while TLA+ is a language for verifying software in particular.

by tome 11y ago

pron 11y ago

> I would love to see PFP as a drawback and obtain its benefits without requiring its rigors. > (One of) the real-world benefit(s) is that I can write a substantial part of a program and know from inspecting only a single line (its type signature) what effects it performs. How can OCaml give me that benefit? That's a property, not a real-world benefit. It's like saying that one of the real-world benefits of Haskell is that its logo is green. In any case, don't know about OCaml, but in Java I just click a button, and get the call tree for the method (or, inversely, get the reverse tree for all methods eventually calling printf). More to the point, see some of Oleg Kiselyov's work on type systems for continuations here: http://okmij.org/ftp/continuations/ http://okmij.org/ftp/continuations/ > I think that says more about how you interpret informal comments on the internet than it does about those making the comments. I think that you should decide whether this is a serious discussion or grandstanding. > Where did I say you should go (the equivalent of) "full vegan"? Maybe you didn't say that I should, but you did say that it's better to be vegan (i.e. make a very significant "lifestyle" change without any evidence to its effectiveness). > At least, it is not known to be wrong. That's true. But I wouldn't go around telling people that being vegan has great health benefit if all we know is that it's not been found to kill you. > I would love to see PFP as a drawback and obtain its benefits without requiring its rigors. So far I have failed to understand your ideas about how to do that and I can only continue to see PFP as a massive boon. OK, but first, a few things: 1/ I don't know if by "rigors" you meant difficulties or rigorousness, but if the latter, then I don't see why you conflate rigor with the pure-functional abstraction. Most formally verified, safety-critical software is written in languages that are far more rigorous than Haskell, yet are not pure-functional. Which leads us to 2/ these are not "my ideas"; if correctness is your goal (as it seems to be), most languages guaranteeing correctness do not espouse the PFP abstractions. Haskell, Coq, Idris and Agda are used far less than other approaches to ensuring software correctness. Finally, 3/ I'd like to be careful when I say "benefits", because we don't know whether they are true benefits, neutral or even detrimental to software at large. All I can say that in this context, when I say "benefits" I mean things that I (and you) believe to be positive and see as potentially advantageous in the "real world". Now, I will give you two examples (of languages used more than Haskell/Coq etc.) for "correct" languages, both of them are very rigorous in the sense of being completely formal, yet they do not suffer from PFP's downsides mainly by being measurably much easier to learn/teach/adopt. They are not generally applicable, but neither is Haskell. The first is the set of synchronous langauges, now used by the industry to design safety-critical realtime software, as well as a lot of hardware. Instead of PFP, it relies on what's known as the "synchronous hypothesis". It has been proven over three decades, as an effective, practical method of writing verifiably correct software by "plain" engineers in hundreds of critical real-world systems. You can read more about it here[1]. A generalization of the approach is called Globally Asynchronous, Locally Synchronous, or GALS, and I believe it has the potential of being a great, more widely applicable way of writing software in a way that lends itself to careful reasoning. The second (you probably saw it coming), is TLA+. It's not a programming language, so I won't compare it to Haskell but to Coq. Unlike Coq, TLA+ does not rely on PFP, or Curry-Howard (neither do other verification tools, like Isabelle) but goes a step further in not being typed at all. It is not functional yet fully mathematical ("referentially transparent"), and its main advantage is that while having the same "proving strength" as Coq when it comes to verifying algorithms[2] while taking days to learn instead of months, and not requiring any mathematical background more than what any engineer already has. I guess that the answer to "how?" would be "in a manner bearing a lot of resemblance to the synchronous hypothesis". There are, of course, other formal approaches (like CSP), but synchronous programming in particular has had a lot of success in the industry. If you want to know about (typed) monads vs. continuations, and their relationship to typed effects, I'll refer you again to my blog post on the subject: http://blog.paralleluniverse.co/2015/08/07/scoped-continuations/ http://blog.paralleluniverse.co/2015/08/07/scoped-continuati... and to Oleg Kiselyov's work, which I've linked to above. [1]: http://link.springer.com/chapter/10.1007%2F978-3-319-11737-9_15 http://link.springer.com/chapter/10.1007%2F978-3-319-11737-9... [2]: Coq may be more powerful when proving general mathematical theorems, but Coq was designed as a general theorem prover, while TLA+ is a language for verifying software in particular.