The "stability" property you mention is nice, but of course if you don't have let-polymorphism then you get a different handy rewrite, namely the equivalence of

let x = e1 in e2 and (fun x -> e2) e1

no? I was surprised when I first realized this didn't hold in ML.

In your last paragraph, you seem to elide the distinction between monomorphic and polymorphic let, implying that both are the bottom rung of the type hierarchy...but I'm proposing that polymorphic let is already an extension of a simpler system. Does polymorphic let not seem "richer" than lambda to you? It certainly seems to me to affect the metatheory (although recently I've been thinking more about set-theoretic sematics than the usual type-theoretic properties).

Maybe I'm splitting hairs...overall it still seems reasonable to me to exclude let-polymorphism from Llama Light, considering that the goal is be a minimal base system, and this one appears to be perfectly practical. I can't tell whether you disagree with this.

-Jeremy

On Mon, Aug 30, 2010 at 4:06 PM, bluestorm <bluestorm.dylc@gmail.com> wrote:

On Mon, Aug 30, 2010 at 7:03 PM, Jeremy Bem <jeremy1@gmail.com> wrote:
> Right...thanks for the refresher. I suppose I should implement this, as
> technically it is not "ML" until I do. I'm still wondering why this is
> considered an essential and desirable feature.

One reason it is interesting is that it gives you the following
stability property,
wich is good for refactoring (both by humans and by copmuters) for example :

let x = e1 in e2 is equivalent to e2{x <- e1} (e2 in wich
all free occurences of x are replaced by e1)

If let isn't polymorphic, then for example let id x = x in (id 1, id
2) doesn't work out.

There are other cases where polymorphism may be useful locally. For
example in Haskell, the ST monad use polymorphism to encode an
information about the use of effects in your code : if all effect are
used locally (so the function is "observationally pure", or
"referentially transparent", while still using side effects inside),
the result will be polymorphic in the state parameter of the ST monad.
If it's not, we know a side effect has escaped, and the type system
forbids you from "running" the monad.

> If one can make local polymorphic definitions, why
> not local types and local exceptions?

In OCaml you can have local types and exceptions through the "let
module = .. in .." construct.

Note however that, on a "richness of the type system" scale, they're
much higher in the hierarchy. Binders on value (lambda and let) are
features of the simple lambda-calculus. Binding on types is a much
more advanced feature, as it belongs to System F. Binders on module
and functors (let module = ... in ..) is even richer, as it translates
in system Fomega. It may not make a lot of difference to the
programmer, but the metatheory needed to support each of these
extension is quite different. Let-binding is the simpler of those.