[Haskell-cafe] Re: FW: Haskell

[Chris Smith]

I've just got a minute, so I'll answer the factual part.

Andrew Bagdanov wrote:
> I thought that in a pure functional language any evaluation order was
> guaranteed to reduce to normal form.  But then it's been a very, very
> long time since I studied the lambda calculus...

If you don't have strong normalization, such as is the case with Haskell, 
then you can look at the language as being a restriction of the pure 
untyped lambda calculus.  In that context, you know that: (a) a given 
expression has at most one normal form, so that *if* you reach a normal 
form, it will always be the right one; and (b) normal order evaluation 
(and therefore lazy evaluation) will get you to that normal form if it 
exists.  Other evaluation strategies may or may not reach the normal 
form, even if the expression does have a normal form.

You may be thinking of typed lambda calculi, which tend to be strongly 
normalizing.  Unlike the case with the untyped lambda calculus, in sound 
typed lambda calculi every (well-typed) term has exactly one normal form, 
and every evaluation strategy reaches it.  However, unrestricted 
recursive types break normalization.  This is not entirely a bad thing, 
since a strongly normalizing language can't be Turing complete.  So real-
world programming languages tend to provide recursive types and other 
features that break strong normalization.

I'm sure there are others here who know this a lot better than I.  I'm 
fairly confident everything there is accurate, but I trust someone will 
correct me if that confidence is misplaced.

-- 
Chris Smith