Re: [Haskell-cafe] Robert Harper on monads and laziness
2011/5/3 Manuel M T Chakravarty c...@cse.unsw.edu.au: Interestingly, today (at least the academic fraction of) the Haskell community appears to hold the purity of the language in higher regard than its laziness. I find Greg Morissett's comment on Lennart Augustsson's article pro lazy evaluation very interesting: http://augustss.blogspot.com/2011/05/more-points-for-lazy-evaluation-in.html#c7969361694724090315 What I find interesting is that he considers (non-)termination an effect, which Haskell does not manage to control like it does other types of effects. Dependently typed purely functional languages like Coq (or Agda if you prefer ;)) do manage to control this (at the cost of replacing general recursion with structural recursion) and require you to model non-termination in a monad (or Applicative functor) like in YNot or Agda's partiality monad (written _⊥) which models just non-termination. I have the impression that this separation of the partiality effect provides a certain independence of evaluation order which neither ML (because of side-effects) nor Haskell (because of non-strict semantics) manage to provide. Such an independence seems very useful for optimization and parallel purposes. Dominique ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Robert Harper on monads and laziness
On Tue, May 3, 2011 at 1:32 AM, Manuel M T Chakravarty c...@cse.unsw.edu.au wrote: ... Interestingly, today (at least the academic fraction of) the Haskell community appears to hold the purity of the language in higher regard than its laziness. As someone who implemented Haskell with quite a bit less laziness, I'm inclined to agree. That said, I think it's easy to underestimate just how much of the structure of the language really encourages a lazy evaluation strategy. One example: where blocks scope over groups of conditional RHSs. This is very handy, in that we can bind variables that are then used in some, but not all, of the disjuncts. Grabbing the first example that comes to hand from my own code: tryOne (gg, uu) e | not (consistent uu) = (gg', uu) | uu==uu' = (gg, uu) | otherwise = (gg', uu') where gg' = gg `addEquation` e uu' = uu `addEquation` e This kind of thing happens all over the place in Haskell code -- it's a very natural coding style -- but if you want to preserve purity it's tough to compile without laziness. -Jan-Willem Maessen ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Robert Harper on monads and laziness
On Tue, May 3, 2011 at 2:26 AM, Dominique Devriese
dominique.devri...@cs.kuleuven.be wrote:
What I find interesting is that he considers (non-)termination an
effect, which Haskell does not manage to control like it does other
types of effects. Dependently typed purely functional languages like
Coq (or Agda if you prefer ;)) do manage to control this (at the cost
of replacing general recursion with structural recursion) and require
you to model non-termination in a monad (or Applicative functor) like
in YNot or Agda's partiality monad (written _⊥) which models just
non-termination.
Dependent typing isn't really necessary. Only totality. Of course,
there's some agreement that dependent types help you get back some of
the power you'd lose by going total (by helping you write precise
enough types for your programs to be accomplished in the more limited
recursive manner).
I have the impression that this separation of the partiality effect
provides a certain independence of evaluation order which neither ML
(because of side-effects) nor Haskell (because of non-strict
semantics) manage to provide. Such an independence seems very useful
for optimization and parallel purposes.
Total lambda calculi tend to yield the same results irrespective of
evaluation strategy. I guess that's useful for optimization, because
you can apply transformations wherever you want without worrying about
changing the definedness of something (because everything is
guaranteed to be well defined regardless of your evaluation strategy).
I don't see how it obviates strictness analysis, though. For instance:
sumAcc a (x:xs) = sumAcc (a + x) xs
sumAcc a [] = a
... case sumAcc 0 l of { n - ... }
Even in a total language, accumulating lazy thunks is likely to be
inefficient for when we go to use the accumulator, whereas one can
also construct examples (even in a total and inductive fragment) where
lazy evaluation will be superior. So you need to do analysis to
determine which things should be strict and which should be lazy for
efficiency, even if you aren't obligated to do it to determine whether
your optimizations are semantics-preserving.
-- Dan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Robert Harper on monads and laziness
I completely agree that laziness enables a number of nice coding idioms and, as Lennart described so eloquently, it does facilitate a combinator-based coding style among other things: http://augustss.blogspot.com/2011/05/more-points-for-lazy-evaluation-in.html (Note that even Bob admits that this is an advantage.) What I meant is that if asked what is more important about Haskell, its laziness or purity, I think most people would pick purity. (But then it's a strange decision to make as laziness implies a need for purity as discussed.) Manuel Jan-Willem Maessen: On Tue, May 3, 2011 at 1:32 AM, Manuel M T Chakravarty c...@cse.unsw.edu.au wrote: ... Interestingly, today (at least the academic fraction of) the Haskell community appears to hold the purity of the language in higher regard than its laziness. As someone who implemented Haskell with quite a bit less laziness, I'm inclined to agree. That said, I think it's easy to underestimate just how much of the structure of the language really encourages a lazy evaluation strategy. One example: where blocks scope over groups of conditional RHSs. This is very handy, in that we can bind variables that are then used in some, but not all, of the disjuncts. Grabbing the first example that comes to hand from my own code: tryOne (gg, uu) e | not (consistent uu) = (gg', uu) | uu==uu' = (gg, uu) | otherwise = (gg', uu') where gg' = gg `addEquation` e uu' = uu `addEquation` e This kind of thing happens all over the place in Haskell code -- it's a very natural coding style -- but if you want to preserve purity it's tough to compile without laziness. -Jan-Willem Maessen ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Robert Harper on monads and laziness
Yes, I'm following it too, and it seems to me that Harper just allows his dislike for Haskell to take advantage of his judgement. Monads as a way to deal with laziness are a very common misconception. Отправлено с iPhone May 2, 2011, в 11:54, Ketil Malde ke...@malde.org написал(а): I'm following Harper's blog, Existential Type¹, which I find to be an enjoyable and entertainingly written tirade about the advantages of teaching functional programming - specifically ML - to students. Of course, he tends to be critical of Haskell, but it's nice to get some thought provoking opinion from somebody who knows a bit about the business. Recently, he had a piece on monads, and how to do them in ML, and one statement puzzled me: There is a particular reason why monads had to arise in Haskell, though, which is to defeat the scourge of laziness. My own view is/was that monads were so successful in Haskell since it allowed writing flexible programs with imperative features, without sacrificing referential transparency. Although people are quick (and rightly so) to point out that this flexibility goes way beyond IO, I think IO was in many ways the killer application for monads. Before IO, we had very limited functionality (like 'interact' taking a 'String - String' function and converting it into an exectuable program) to build real programs from. Laziness does require referential transparency (or at least, it is easier to get away with the lack of RT in a strict language), so I can see that he is indirectly correct, but RT is a goal in itself. Thus, I wonder if there are any other rationale for a statement like that? -k ¹ http://existentialtype.wordpress.com/ -- If I haven't seen further, it is by standing in the footprints of giants ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Robert Harper on monads and laziness
On 2011-05-02 03:54, Ketil Malde wrote: There is a particular reason why monads had to arise in Haskell, though, which is to defeat the scourge of laziness. I wonder if there are any other rationale for a statement like that? He spends one paragraph dismissing the usefulness of referential transparency You cannot easily convert between functional and monadic style without a radical restructuring of code. ... you are deprived of the useful concept of a benign effect I imagine that he considered how he prefers ML the way it is, without base libraries thoroughly rewritten to support purity. If purity and RT aren't the reason why Haskell uses monads, what's left? Laziness does have disadvantages. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Robert Harper on monads and laziness
2011/5/2 Ketil Malde ke...@malde.org: There is a particular reason why monads had to arise in Haskell, though, which is to defeat the scourge of laziness. My own view is/was that monads were so successful in Haskell since it allowed writing flexible programs with imperative features, without sacrificing referential transparency. [...] Laziness does require referential transparency (or at least, it is easier to get away with the lack of RT in a strict language), so I can see that he is indirectly correct, but RT is a goal in itself. Thus, I wonder if there are any other rationale for a statement like that? I agree with your analysis. Throughout his different articles, I think Harper partly has a point when he says that laziness brings certain disadvantages (like e.g. complex memory and CPU behaviour) to Haskell (although I disagree with some of his other arguments here). However, like you say, he misses the ball by amalgamating laziness with referential transparency, where the first probably requires the second but not vice versa. This allows him to simply dismiss both, which is convenient for his apparent conclusion that ML is strictly better than Haskell, since referential transparency and purity are (in my view) one of the things ML lacks most when compared to Haskell. His only other argument against referential transparency and purity seems to be his mentioning of benign effects, which is weak for two reasons: first, benign effects are clearly not what typical ML programs use non-purity for and second, benign effects can be supported much more conservatively using Haskell's unsafePerformIO. Dominique ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Robert Harper on monads and laziness
On Mon, May 2, 2011 at 9:29 AM, Dominique Devriese dominique.devri...@cs.kuleuven.be wrote: I agree with your analysis. Throughout his different articles, I think Harper partly has a point when he says that laziness brings certain disadvantages (like e.g. complex memory and CPU behaviour) to Haskell (although I disagree with some of his other arguments here). However, like you say, he misses the ball by amalgamating laziness with referential transparency, where the first probably requires the second but not vice versa. This allows him to simply dismiss both, which is convenient for his apparent conclusion that ML is strictly better than Haskell, since referential transparency and purity are (in my view) one of the things ML lacks most when compared to Haskell. His only other argument against referential transparency and purity seems to be his mentioning of benign effects, which is weak for two reasons: first, benign effects are clearly not what typical ML programs use non-purity for and second, benign effects can be supported much more conservatively using Haskell's unsafePerformIO. Or, instead of unsafePerformIO, runST. Saying that we should allow effects everywhere because there are benign effects is like saying that we should allow GOTOs everywhere because there are some benign GOTOs. By allowing these benign things we also open a can of worms of malign things. Cheers, -- Felipe. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Robert Harper on monads and laziness
On 02/05/11 17:54, Ketil Malde wrote: I'm following Harper's blog, Existential Type¹, which I find to be an enjoyable and entertainingly written tirade about the advantages of teaching functional programming - specifically ML - to students. Of course, he tends to be critical of Haskell, but it's nice to get some thought provoking opinion from somebody who knows a bit about the business. Recently, he had a piece on monads, and how to do them in ML, and one statement puzzled me: There is a particular reason why monads had to arise in Haskell, though, which is to defeat the scourge of laziness. My own view is/was that monads were so successful in Haskell since it allowed writing flexible programs with imperative features, without sacrificing referential transparency. Although people are quick (and rightly so) to point out that this flexibility goes way beyond IO, I think IO was in many ways the killer application for monads. Before IO, we had very limited functionality (like 'interact' taking a 'String - String' function and converting it into an exectuable program) to build real programs from. Laziness does require referential transparency (or at least, it is easier to get away with the lack of RT in a strict language), so I can see that he is indirectly correct, but RT is a goal in itself. Thus, I wonder if there are any other rationale for a statement like that? -k ¹ http://existentialtype.wordpress.com/ Interesting how I have been authoring and subsequently using monads in scala for several years and it is strictness that gets in the way more than anything. http://github.com/scalaz/scalaz/ I have been teaching functional programming for quite a while, both in universities and outside of academia, and I am of the opinion that Haskell's suitability in first place has no close second place. I wonder why I am wrong, but this post (and previous) is hardly persuasive. -- Tony Morris http://tmorris.net/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Robert Harper on monads and laziness
Tony Morris: Interesting how I have been authoring and subsequently using monads in scala for several years and it is strictness that gets in the way more than anything. Just to make sure that I understand you correctly. You are saying that when you use monads in Scala, then strictness makes that more awkward than necessary. (I assume that you are *not* saying that strictness is the most awkward language feature of Scala.) Why is that? Manuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Robert Harper on monads and laziness
For a historical perspective, I highly recommend The Definitive Account of the History of Haskell: http://research.microsoft.com/en-us/um/people/simonpj/papers/history-of-haskell/index.htm Section 7 clearly and directly cites the desire to have pure I/O as the motivation for adopting monads. As you are saying that doesn't directly contradict the statement of Bob that you cite. In fact, Section 3.2 of the above paper supports the opinion that purity is a consequence of choosing to be lazy, but it also claims that the combination of power and beauty of a pure language motivated the language designers. Interestingly, today (at least the academic fraction of) the Haskell community appears to hold the purity of the language in higher regard than its laziness. Manuel Ketil Malde: I'm following Harper's blog, Existential Type¹, which I find to be an enjoyable and entertainingly written tirade about the advantages of teaching functional programming - specifically ML - to students. Of course, he tends to be critical of Haskell, but it's nice to get some thought provoking opinion from somebody who knows a bit about the business. Recently, he had a piece on monads, and how to do them in ML, and one statement puzzled me: There is a particular reason why monads had to arise in Haskell, though, which is to defeat the scourge of laziness. My own view is/was that monads were so successful in Haskell since it allowed writing flexible programs with imperative features, without sacrificing referential transparency. Although people are quick (and rightly so) to point out that this flexibility goes way beyond IO, I think IO was in many ways the killer application for monads. Before IO, we had very limited functionality (like 'interact' taking a 'String - String' function and converting it into an exectuable program) to build real programs from. Laziness does require referential transparency (or at least, it is easier to get away with the lack of RT in a strict language), so I can see that he is indirectly correct, but RT is a goal in itself. Thus, I wonder if there are any other rationale for a statement like that? -k ¹ http://existentialtype.wordpress.com/ -- If I haven't seen further, it is by standing in the footprints of giants ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
