Syntactically you can easily imagine a language without let
. Immediately, we can produce this in Haskell by simply relying on where
if we wanted. Beyond that are many possible syntaxes.
Semantically, you might think that let could translate away to something like this
let x = e in g ==> (\x -> g) e
and, indeed, at runtime these two expressions are identical (modulo recursive bindings, but those can be achieved with fix
). Traditionally, however, let
has special typing semantics (along with where
and top-level name definitions... all of which being, effectively, syntax sugar for let
).
In particular, in the Hindley-Milner type system which forms the foundation of Haskell there's a notion of let
-generalization. Intuitively, it regards situations where we upgrade functions to their most polymorphic form. In particular, if we have a function appearing in an expression somewhere with a type like
a -> b -> c
those variables, a
, b
, and c
, may or may not already have meaning in that expression. In particular, they're assumed to be fixed yet unknown types. Compare that to the type
forall a b c. a -> b -> c
which includes the notion of polymorphism by stating, immediately, that even if there happen to be type variables a
, b
, and c
available in the envionment, these references are fresh.
This is an incredibly important step in the HM inference algorithm as it is how polymorphism is generated allowing HM to reach its more general types. Unfortunately, it's not possible to do this step whenever we please—it must be done at controlled points.
This is what let
-generalization does: it says that types should be generalized to polymorphic types when they are let
-bound to a particular name. Such generalization does not occur when they are merely passed into functions as arguments.
So, ultimately, you need a form of "let" in order to run the HM inference algorithm. Further, it cannot just be syntax sugar for function application despite them having equivalent runtime characteristics.
Syntactically, this "let" notion might be called let
or where
or by a convention of top-level name binding (all three are available in Haskell). So long as it exists and is a primary method for generating bound names where people expect polymorphism then it'll have the right behavior.