yet I need to add a $! to the recursive call of isum to get a truly iterative ??? Wait a minute Patai. How would you do that? I'm only beginner I thought I can only add strict "!" to data parameters. But to make isum function strict would be helpful. Thanks On Mon, Nov 3, 2008 at 7:36 PM, Don Stewart wrote:

patai_gergely:

...

Hi everyone,

I was experimenting with simple accumulator functions, and found that an apparently tail recursive function can easily fill the stack. Playing around with ghc and jhc gave consistently unpleasant results. Look at this program:

%%%%%%%%%%%

-- ghc: no, ghc -O3: yes, jhc: no isum 0 s = s isum n s = isum (n-1) (s+n)

-- ghc: no, ghc -O3: no, jhc: yes (because gcc -O3 is clever) rsum 0 = 0 rsum n = n + rsum (n-1)

main = case isum 10000000 0 {- rsum 10000000 -} of 0 -> print 0 x -> print x

%%%%%%%%%%%

I would expect the analysis to find out that the result of the function is needed in every case (since we are matching a pattern to it), yet I need to add a $! to the recursive call of isum to get a truly iterative function. It's interesting how ghc and jhc seem to diverge, one favouring the "iterative" version, the other the "recursive" one (although it only works because gcc figures out that the function can be expressed in an iterative way).

Of course this is a real problem when I'm trying to write an actual program, since it means I can be bitten by the laziness bug any time... Is there any solution besides adding strictness annotations? Can I expect the compiler to handle this situation better in the foreseeable future?

I think its sensible not to rely on an analysis to infer the correct reduction strategy for your code. Make the strictness explict, and your code will be more portable and more robust.

Also, write in some type annotations. Particularly for atomic types like Int, these give the strictness analyser yet more information to work with.

-- Don _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On Mon, Nov 3, 2008 at 2:35 PM, Don Stewart wrote:

Consider this program,

isum 0 s = s isum n s = isum (n-1) (s+n)

main = case isum 10000000 0 {- rsum 10000000 -} of 0 -> print 0 x -> print x

Now, isum is *not* strict in 's', [...]

Of course, we make this strict in a number of ways:

* Turning on optimisations:

I am confused about your usage of "strict". Optimizations are not supposed to change semantics, so I don't know how it is possible to make a function strict by turning on optimizations. This function was always strict in s, given a strict numeral type. By induction on n: isum 0 _|_ = _|_ isum (n+1) _|_ = isum n (s+_|_) = isum n _|_ = _|_ For negative n, it either wraps around to positive in which case the above analysis applies, or it does not halt, which is strict (in the same way "const _|_" is strict). Luke

lrpalmer:

On Mon, Nov 3, 2008 at 2:35 PM, Don Stewart wrote:

...

Consider this program,

isum 0 s = s isum n s = isum (n-1) (s+n)

main = case isum 10000000 0 {- rsum 10000000 -} of 0 -> print 0 x -> print x

Now, isum is *not* strict in 's', [...]

Of course, we make this strict in a number of ways:

* Turning on optimisations:

I am confused about your usage of "strict". Optimizations are not supposed to change semantics, so I don't know how it is possible to make a function strict by turning on optimizations. This function was always strict in s, given a strict numeral type. By induction on n:

isum 0 _|_ = _|_ isum (n+1) _|_ = isum n (s+_|_) = isum n _|_ = _|_

For negative n, it either wraps around to positive in which case the above analysis applies, or it does not halt, which is strict (in the same way "const _|_" is strict).

"Optimisations" enable strictness analysis. -- Don

On Mon, 3 Nov 2008, Luke Palmer wrote:

On Mon, Nov 3, 2008 at 2:54 PM, Don Stewart wrote:

...

"Optimisations" enable strictness analysis.

I was actually being an annoying purist. "f is strict" means "f _|_ = _|_", so strictness is a semantic idea, not an operational one. Optimizations can change operation, but must preserve semantics.

But I'm not just picking a fight. I'm trying to promote equational reasoning over operational reasoning in the community, since I believe that is Haskell's primary strength.

Maybe I missed the point, but the optimization seems correct to me. Without optimization and its (strictness) analysis the program would still output the correct answer - given that the stack is sufficiently large. Optimization simply makes this program run using much less space. Right?

David Menendez-2 wrote:

...

On Mon, 3 Nov 2008, Luke Palmer wrote:

I was actually being an annoying purist. "f is strict" means "f _|_ = _|_", so strictness is a semantic idea, not an operational one.

I think Luke was commenting on the terminology, not the optimization. We have a tendency to say "lazy" when we mean "non-strict" and "strict" when we mean "eager".

Good point. If it sheds light on such elusive, important distinctions then this incorrigible pedantry can only be encouraged. -- View this message in context: http://www.nabble.com/Problems-with-strictness-analysis--tp20301967p20319740... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.

Thanks everyone for the answers. I understood the underlying mechanism, and I did see that turning on optimisation helps, as I said in the comments. I just wasn't aware that this analysis is not turned on by default, my bad for not reading the FM. So the final verdict is that type and strictness annotations are unavoidable when it comes to improving performance. This is no big surprise. My only problem is that if I try to write a program without thinking about performance first and not bothering with annotations as long as "it works", I end up with something that's practically impossible to profile as the costs spread everywhere. I'd be curious to hear about "best practices" to avoid this, while also getting the most out of type inference and various analyses to cut down on developer effort. How should I approach writing a large application in Haskell? Gergely -- http://www.fastmail.fm - IMAP accessible web-mail

On Tue, 2008-11-04 at 12:18 +0100, Patai Gergely wrote:

Thanks everyone for the answers. I understood the underlying mechanism, and I did see that turning on optimisation helps, as I said in the comments. I just wasn't aware that this analysis is not turned on by default, my bad for not reading the FM.

So the final verdict is that type and strictness annotations are unavoidable when it comes to improving performance. This is no big surprise. My only problem is that if I try to write a program without thinking about performance first and not bothering with annotations as long as "it works", I end up with something that's practically impossible to profile as the costs spread everywhere. I'd be curious to hear about "best practices" to avoid this, while also getting the most out of type inference and various analyses to cut down on developer effort. How should I approach writing a large application in Haskell?

Strictness annotations aren't optimizations. As Luke Palmer pointed out, making something strict is a change in semantics. Similarly for type annotations; either they do nothing or they restrict the type which certainly has semantic ramifications. Neither strictness nor type annotations should be viewed as something "outside of" your program. They are a part of your program. At any rate, for the particular issues you've mentioned in this thread I'd recommend not writing code you "know" is bad in the first place, in much the same way that Scheme programmers usually write code tail recursively from the start. They don't write code (non tail) recursively and then "profile" to find the hotspots. There are a few well-known problematic patterns in Haskell that can be relatively easily recognized and remedied. Those should be dealt with as you write the code. Note that here I'm talking about issues like stack overflow; you shouldn't rely on strictness analysis to avoid stack overflow, but it is fine to rely on strictness analysis for things like unboxing and such. Basically, if you don't do "stupid stuff", such as well-known anti-patterns or obviously inefficient things, then you should typically get reasonable performance with maybe a few things that the profiler can help you with. If you are specifically going for performance, then there are techniques and approaches geared toward that.

Achim Schneider schrieb:

Derek Elkins wrote:

...

well-known anti-patterns

I'm wondering why there are so miraculously well-known. Could it be the dedicated wiki page titled "DONTDOTHAT!!!one!" that lists them all?

There was http://www.haskell.org/haskellwiki/Things_to_avoid which has been renamed to the more friendly "Haskell programming tips"

On Wed, Nov 5, 2008 at 4:33 AM, Achim Schneider wrote:

I know that I, coming from a C/Scheme POV, in the beginning attributed much magic to Haskell's inner workings and assumed, because of the general wizardly air of the whole language, avg to run in O(n) time and constant resp. O(n) space.

Haskell's great strength is its equational semantics. I would like Haskell programmers to think equationally, mathematically, rather than operationally, when writing Haskell programs. If I were to teach a course in Haskell, I would like to launch off of denotational semantics, hopefully without ever having to say "lazy evaluation". (It's a pipe dream, of course, but you get the idea) However, this strength is also a weakness when we want to analyze the efficiency of programs. The denotational semantics of Haskell say nothing about time or space complexity, and give us no tools to reason about it. A Haskell interpreter which randomly rewrites terms until it happens upon a normal form is considered correct (or rather, "correct with probability 1" :-). How can we support analysis of time and space complexity without expanding ourselves into the complicated dirty world of operational thinking? Luke

On Wed, Nov 5, 2008 at 1:24 AM, Claus Reinke wrote:

...

How can we support analysis of time and space complexity without expanding ourselves into the complicated dirty world of operational thinking?

equational /= denotational

Nonetheless, Haskell has equational semantics which are derived from its denotational ones. But when I said "equational semantics" I really meant something more like "equations" :-).

operational /= bad

Sometimes, denotational is too abstract, offering no guidelines on behaviour, just as abstract machine based operational thinking is too concrete, hiding the insights in a flood of details. Sometimes, operational semantics based on directed equations give you the best of both worlds: equational reasoning and behavioural guidelines, both at a suitably "clean" and abstract level.

By directed equations you mean unidirectional rewrite rules? But I'd like to back up a bit. I may have been too quick to assign the judgement "dirty" to operational thinking. I am not asking this question as a complaint, as a challenge on the language, or as any other such rhetorical device: my question is earnest. I would like to know or to develop a way to allow abstract analysis of time and space complexity. On my time working with Haskell, I've developed a pretty accurate "intuition" about the performance of programs. It is some meld of thinking in terms of the lazy evaluation mechanism, some higher-level rules of thumb about when new thunks are allocated, and probably some other stuff hiding in the depths of my brain. I know it, but I am not satisfied with it, because I can't formalize it. I wouldn't be able to write them down and explain to a fellow mathematician how I reason about Haskell programs. The example being discussed in this thread is a good one: sum [1..10^8] + length [1..10^8] With Haskell's semantics, we know we can write this as: let xs = [1..10^8] in sum xs + length xs But it causes a change in memory *complexity*, so in some sense these two sentences are not equal. What is the theory in which we can observe this fact? Is it possible to give a simple denotational semantics which captures it?

...

equational /= denotational

Nonetheless, Haskell has equational semantics which are derived from its denotational ones. But when I said "equational semantics" I really meant something more like "equations" :-).

Unlike Standard ML, for instance, Haskell does not have standard semantics - a persistent embarrassment. There are semantics for fragments, but no guarantee that any of them will match any part of the language, let alone its implementations. One can base equational semantics on denotational semantics, but that is not the only way, hence the two are not equal. I was trying to point out the missing part, where equations are are useful for operational reasoning, beyond simple denotations.

...

Sometimes, operational semantics based on directed equations give you the best of both worlds: equational reasoning and behavioural guidelines, both at a suitably "clean" and abstract level.

By directed equations you mean unidirectional rewrite rules?

Yes. Think of rewriting (replacing old with new) as a general form of operational semantics.Within this form, there is a wide range of possibilities, including rewriting abstract machine states and rewriting source-level programs. Somewhere near the latter, there is a "most abstract" form of operational semantics for a language, one for which every other form adds details that are not inherent in the language, but are artifacts of the formalisation (details of the abstract machine, or details of the mathematical domain, or ..).

But I'd like to back up a bit. I may have been too quick to assign the judgement "dirty" to operational thinking. I am not asking this question as a complaint, as a challenge on the language, or as any other such rhetorical device: my question is earnest. I would like to know or to develop a way to allow abstract analysis of time and space complexity.

So you want to reason about the way from the original program to its outputs, not just about the outputs. You can cling to denotations, by extending mere values with information about the computation leading to those values, but why not reason about the computation directly. In logic terms, you want to talk about the proof, not just about the truth of your theorems. In functional language terms, you want to talk about reductions, not just about normal forms. This works well for pure lambda calculus, and has been extended to cover other aspects of Haskell implementations, such as call-by-need lambda calculus as a way for evaluation of non-strict programs with sharing. The call-by-need lambda calculus John Maraist and Martin Odersky and Philip Wadler Journal of Functional Programming, 1998 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.44.5259 The idea is to use "let" to represent sharing, and to refine the reduction rules to take this into account: instead of substituting parameters into function bodies, parameter bindings are kept in "let"-bindings, where their evaluation is shared (only values can be substituted, so substitution is preceded by evaluation, when needed). The resulting reductions are quite a bit more involved than without sharing, because all reductions take place within a context (those "let"-bindings). But that is quite close to what happens in a compiled graph reduction implementation: those "let"-bindings represent the heap, the nested contexts correspond to stack. (there are of course optimizations and representation changes that affect performance, but the former are themselves expressed as rewrite rules, and the latter can be accounted for by refining the rewrite system, when such details are needed - luckily, that isn't often the case)

On my time working with Haskell, I've developed a pretty accurate "intuition" about the performance of programs. It is some meld of thinking in terms of the lazy evaluation mechanism, some higher-level rules of thumb about when new thunks are allocated, and probably some other stuff hiding in the depths of my brain. I know it, but I am not satisfied with it, because I can't formalize it. I wouldn't be able to write them down and explain to a fellow mathematician how I reason about Haskell programs.

The example being discussed in this thread is a good one:

sum [1..10^8] + length [1..10^8]

With Haskell's semantics, we know we can write this as:

let xs = [1..10^8] in sum xs + length xs

But it causes a change in memory *complexity*, so in some sense these two sentences are not equal. What is the theory in which we can observe this fact? Is it possible to give a simple denotational semantics which captures it?

Why do you insist on denotational semantics for reasoning about evaluation? Denotational semantics are best when all you care about are values. Have a look at that paper, or the earlier version http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.2287 There is also John Launchbury, A Natural Semantics for Lazy Evaluation,1993 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.35.2016 which used an explicit heap to capture sharing (the later use of "let" made it possible to talk about sharing without adding any constructs not in the language). Either of these, if extended with the necessary primitives, should distinguish your two terms: in the former, sharing of the long list never arises (so the computations are independent), in the latter, that sharing is never lost (so evaluating one sub-term will evaluate the shared xs, which are kept around until the other sub-term gets to consuming them) . Claus

Luke Palmer wrote:

The example being discussed in this thread is a good one:

sum [1..10^8] + length [1..10^8]

With Haskell's semantics, we know we can write this as:

let xs = [1..10^8] in sum xs + length xs

But it causes a change in memory *complexity*, so in some sense these two sentences are not equal. What is the theory in which we can observe this fact? Is it possible to give a simple denotational semantics which captures it?

There's actually been a good deal of work on trying to mathematize this sort of issue, under the name of linear logic[1]. The problem with classical equational reasoning is that it doesn't capture the notion of "resources" or the "sharing" thereof. The two expressions are not the same because the first has two [1..10^8] resources it can use up, whereas the later only has one. Depending on the balance between sharing temporal work vs minimizing memory overhead, sometimes it's okay to add sharing and other times it's okay to remove it, but in general both options are not available at once. It's pretty easy to capture issues of economy with LL, though making a rewriting system takes a bit more framework. I'm not sure to what extent LL has been explored as a semantic model for programs, but Clean[2] and Phil Wadler[3] have certainly done very similar work. [1] http://en.wikipedia.org/wiki/Linear_logic [2] http://www.st.cs.ru.nl/Onderzoek/Publicaties/publicaties.html [3] http://homepages.inf.ed.ac.uk/wadler/topics/linear-logic.html -- Live well, ~wren

Achim Schneider schrieb:

Henning Thielemann wrote:

...

There was http://www.haskell.org/haskellwiki/Things_to_avoid

which has been renamed to the more friendly "Haskell programming tips"

I was rather thinking of a list of performance pitfalls and laziness tarpits, starting with the all-famous

avg xs = sum xs + length xs

(/) instead of (+) ? In the old hawiki there was an article about that particular example ...

Nonsense, isum is strict in s. If s is bottom, isum will always return bottom. This is the definition of being strict. -- Lennart On Mon, Nov 3, 2008 at 10:35 PM, Don Stewart wrote:

frantisek.kocun:

...

yet I need to add a $! to the recursive call of isum to get a truly iterative ???

Wait a minute Patai. How would you do that? I'm only beginner I thought I can only add strict "!" to data parameters. But to make isum function strict would be helpful.

Consider this program,

isum 0 s = s isum n s = isum (n-1) (s+n)

main = case isum 10000000 0 {- rsum 10000000 -} of 0 -> print 0 x -> print x

Now, isum is *not* strict in 's', so without some additional hints or analysis, this won't be evaluated until the result of isum is required. It will build up a long change of (s + n) on the stack.

-O0 $ time ./A Stack space overflow: current size 8388608 bytes.

Of course, we make this strict in a number of ways:

* Turning on optimisations: -O2 $ time ./A 50000005000000 ./A 0.31s user 0.00s system 99% cpu 0.312 total

* Use an explict bang pattern on the 's' variable:

{-# LANGUAGE BangPatterns #-}

isum 0 s = s isum n !s = isum (n-1) (s+n)

-O0 $ time ./A 50000005000000 ./A 0.69s user 0.00s system 95% cpu 0.721 total

Note that by being explict about the strictness in 's' this program produces the desired result even with all optimisations disabled.

We can then turn on other optimisations:

-O2 -fvia-C -optc-O2 $ time ./A 50000005000000 ./A 0.31s user 0.00s system 101% cpu 0.313 total

And it just gets faster.

Now, we can also add an explicit type signature to constrain to a machine Int:

-O2 -fvia-C -optc-O2 $ time ./A 50000005000000 ./A 0.03s user 0.00s system 100% cpu 0.033 total

Meaing the final version is:

isum :: Int -> Int -> Int isum 0 s = s isum n !s = isum (n-1) (s+n)

So: if you rely on tail recursion on a particular variable, make sure it is enforced as strict. That's the simplest, most robust way to ensure the reduction strategy you want is used.

-- Don

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

wren ng thornton writes: [snick]

...

isum 0 s = s isum n s = isum (n-1) (s+n)

This is tail recursive, and will be optimized to an iterative loop;

[snick]

In terms of having a compiler 'smart enough', it's not clear that functions of this sort ought to be inferred strict simply because the accumulator is ultimately returned to the caller. Consider for example:

I thought this was strict as Luke Palmer has already pointed out. My understanding is that a compiler may be able to infer it is strict and then perform eager evaluation.

...

f 0 xs = xs f n xs = f (n-1) (replicate n n ++ xs)

Since (++) can indeed return partial answers, it's fine for the accumulator to be lazy. Indeed, making it strict harms performance significantly. Another example is when the accumulator is a function, as

Can this function be strict if (++)isn't? And if it isn't strict, why would it make sense to evaluate it eagerly? Dominic. PS This subject seems to come up often enough to be worth a wiki entry (maybe there already is one). I think we should also be careful with terminology (as Luke Palmer and David Menendez have pointed out. Maybe that could be included in the wiki entry.

wren ng thornton wrote:

If Haskell had strictness annotations as part of the type system, then there might be room for progress. We could imagine constructing separate polymorphic bodies for isum, one for each strictness variant of (+). Then, when isum is instantiated at types which define strict (+) we could use an optimized version of isum that forces evaluation at each step. Now the trick becomes how to control the explosion of generated code for all the combinatorially many strictness variants of types. For whole-program optimizing compilers, it should be relatively easy to keep the code bloat down, but for separate compilation it's not so straightforward. Chances are that any solution along this route would still require strictness annotations in order to do the right thing, only now we've lifted the annotations into the type language instead of leaving them in the term language.

Code explosion is actually what we want, as things like (+) are best if unboxed and inlined, to one of the thousands of machine instructions the target architecture offers for that operation (think x86, amd64, x87, mmx, sse, sse2...). As a side note, you made me think about y-combinators, stream fusion and lists of computations that can be rewritten to use the minimum number of y's possible/computable. It appears to have a lot in common with strictness/eagerness if you eg. think of [n..] as a fixpoint of the form y (\num_calls -> num_calls + n). FP semanticists will now cry "Heresy! Repeat after me: Pure is pure and impure is impure, always and ever", so I rather shut up and think before I make even less sense. -- (c) this sig last receiving data processing entity. Inspect headers for copyright history. All rights reserved. Copying, hiring, renting, performance and/or quoting of this signature prohibited.

I tried your example in GHC 6.10 and isum appears to work fine. The type of 10000000 gets defaulted to Integer, a specialized version of isum for Integer is then created, the strictness analyzer determines that isum is strict in s, and the code generator produces a loop. (If you want to look at the assembly code, it's easier if you make the type Int.) Thanks for checking it. I'll be curious to see any improvements the new version brings, but this sounds promising already.

Gergely -- http://www.fastmail.fm - The way an email service should be