2010/11/3 Petr Pudlak
However, from the typing point of view, it makes quite a difference. It is an integral part of the Hindley-Milner type inference algorithm, which is used by many functional languages. Consider the following two expressions:
f = (\x -> x x) (\y -> y) g = let x = \y -> y in x x
The function "f" is not typable in the Hindley-Milner type system, while "g" is is (and its type is "a -> a"). The reason is that in the first case (f), the typing system tries to assign a single type to "x", which is impossible (one would have to unify types "a" and "a -> b"). In the second case (g), the typing system assigns "x" a polymorphic type schema forall a.a -> a which can be instantiated to both "a -> a" (the second "x") and "(b -> b) -> (b -> b)" (the first "x"), and then applied together. I'd say that "let ... in ..." is a core feature of the language that gives us parametric polymorphism.
Although this decision is not without problems. See the recent paper "Let should not be generalised" [1] -- ryan [1] Let should not be generalised, Dimitrios Vytiniotis, Simon Peyton Jones, and Tom Schrijvers; submitted to TLDI 2010. http://research.microsoft.com/en-us/um/people/simonpj/papers/constraints/ind...