[Haskell-cafe] Re: FW: Haskell
cdsmith at twu.net
Tue Apr 1 19:43:48 EDT 2008
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.
More information about the Haskell-Cafe