WHNF versus HNF (was: Optimizing unamb by determining the "state" of a thunk?)

I'm having difficulty to understand the difference between WHNF and HNF. Is this explanationhttp://encyclopedia2.thefreedictionary.com/Weak+Head+Normal+Form the correct one? Or is WHNF and HNF equivalent in Haskell land? The GHC documentation of seq says: Evaluates its first argument to head normal form, and then returns its second argument as the result. Let's try in GHCi *Main> let f = trace "\\x" $ \x -> ((trace "\\y" $ \y -> trace "y" y + trace "x" x) $ trace "2" 2) *Main> f `seq` () \x () *Main> That did not evaluate anything inside the body of the first lambda, so according to the article, seq reduces to weak head normal form, not hnf...

Am Mittwoch 22 April 2009 23:57:08 schrieb Peter Verswyvelen:
I'm having difficulty to understand the difference between WHNF and HNF.
Is this explanation<http://encyclopedia2.thefreedictionary.com/Weak+Head+Normal+For m> the correct one? Or is WHNF and HNF equivalent in Haskell land?
The GHC documentation of seq says: Evaluates its first argument to head normal form, and then returns its second argument as the result.
Let's try in GHCi
*Main> let f = trace "\\x" $ \x -> ((trace "\\y" $ \y -> trace "y" y + trace "x" x) $ trace "2" 2) *Main> f `seq` () \x () *Main>
That did not evaluate anything inside the body of the first lambda, so according to the article, seq reduces to weak head normal form, not hnf...
Yes, error in the docs. seq evaluates to WHNF, not HNF (unless the two coincide).

On Wednesday 22 April 2009, Peter Verswyvelen wrote:
I'm having difficulty to understand the difference between WHNF and HNF.
Is this explanation<http://encyclopedia2.thefreedictionary.com/Weak+Head+Normal+For m> the correct one? Or is WHNF and HNF equivalent in Haskell land?
The GHC documentation of seq says: Evaluates its first argument to head normal form, and then returns its second argument as the result.
Let's try in GHCi
*Main> let f = trace "\\x" $ \x -> ((trace "\\y" $ \y -> trace "y" y + trace "x" x) $ trace "2" 2) *Main> f `seq` () \x () *Main>
That did not evaluate anything inside the body of the first lambda, so according to the article, seq reduces to weak head normal form, not hnf... Hi, Try:
Prelude Debug.Trace> (f 0) `seq` () \x \y y 2 x () -- Thanks! Marcin Kosiba

Peter Verswyvelen wrote:
The GHC documentation of seq says: Evaluates its first argument to head normal form, and then returns its second argument as the result.
I think this should be "weak head normal form". I don't think you have any means to evaluate under a binder in Haskell. The weak in weak head normal forms means that evaluation does not go "under" lambda binders. The head in weak head normal form means that evaluation does not take place in argument positions. Note that most programming languages evaluate to weak normal forms, because functions are only evaluated when they are called. So the head part is much more important then the weak part when explaining Haskell semantics, leading to sometimes omitting the weak part. Tillmann
participants (4)
-
Daniel Fischer
-
Marcin Kosiba
-
Peter Verswyvelen
-
Tillmann Rendel