[Haskell-cafe] Non-recursive let [Was: GHC bug? Let with guards loops]

[oleg at okmij.org]

Alberto G. Corona wrote:
> I think that a non-non recursive let could be not compatible with the pure
> nature of Haskell.

I have seen this sentiment before. It is quite a mis-understanding. In
fact, the opposite is true. One may say that Haskell is not quite pure
_because_ it has recursive let.

Let's take pure the simply-typed lambda-calculus, or System F, or
System Fomega. Or the Calculus of Inductive Constructions. These
calculi are pure in the sense that the result of evaluation of each
expression does not depend on the evaluation strategy. One can use
call-by-name, call-by-need, call-by-value, pick the next redex at
random or some other evaluation strategy -- and the result will be
just the same. Although the simply-typed lambda-calculus is quite
limited in its expressiveness, already System F is quite powerful
(e.g., allowing for the list library), to say nothing of CIC. In all
these systems, the non-recursive let

        let x = e1 in e2
is merely the syntactic sugar for
        (\x. e2) e1

OTH, the recursive let is not expressible. (Incidentally, although
System F and above express self-application (\x.x x), a fix-point
combinator is not typeable.) Adding the recursive let introduces
general recursion and hence the dependence on the evaluation
strategy. There are a few people who say non-termination is an
effect. The language with non-termination is no longer pure.