[Re-adding caml-list: I thought this conversation about let-polymorphism
might be of wider interest.]

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.
>