Llama Light: a simple implementation of Caml
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20100830 (20:49) 
From:  Jeremy Bem <jeremy1@g...> 
Subject:  Re: [Camllist] Llama Light: a simple implementation of Caml 
[Readding camllist: I thought this conversation about letpolymorphism might be of wider interest.] The "stability" property you mention is nice, but of course if you don't have letpolymorphism 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 settheoretic sematics than the usual typetheoretic properties). Maybe I'm splitting hairs...overall it still seems reasonable to me to exclude letpolymorphism 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 lambdacalculus. 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. Letbinding is the simpler of those. >