On dropping @names

Andreas Rossberg rossberg at google.com
Thu Dec 6 07:29:27 PST 2012


On 5 December 2012 19:19, Claus Reinke <claus.reinke at talk21.com> wrote:
>> their operational generativity perhaps being a mismatch with their
>> seemingly static meaning in certain syntactic forms,
>
> This appears to be ungrounded. See below.

Personally, I also consider that a non-issue, but it was concern that
was raised.

>>> Implicit scoping in a language with nested scopes has never been a
>>> good idea (even the implicit var/let scopes in JS are not its strongest
>>> point). Prolog got away with it because it had a flat program structure
>>> in the beginning, and even that fell down when integrating Prolog-like
>>> languages into functional one, or when adding local sets of answers.
>>
>> Indeed. (Although I don't think we have implicit let-scopes in JS.)
>
> There are few enough cases (scope to nearest enclosing block unless there is
> an intervening conditional or loop construct,

If you mean something like

  if (bla) let x;

then that is not actually legal.

> to nearest for loop body if it
> appears in the loop header, to the right in a comprehension) that the
> difference might not matter.
> I would have preferred if let had not been modeled after var so much, but
> that is another topic.

It is as clean as it can get given JS. And you may be surprised to
hear that there are some voices who actually would have preferred a
_more_ var-like behaviour.

>>> So I'm not sure how your concerns are being addressed by
>>> merely replacing a declarative scoping construct by an explicitly
>>> imperative gensym construct?
>>
>> We have the gensym construct anyway, @-names were intended to be merely
>> syntactic sugar on top of that.
>
> Yes, so my question was how removing the sugar while keeping
> the semantics is going to address the concerns voiced in the meeting
> notes.

The concern was that the sugar has issues, not symbol semantics as such.


>> Scope extrusion semantics actually is equivalent to an allocation
>> semantics. The only difference is that the store is part of your term
>> syntax instead of being a separate runtime environment, but it does
>> not actually make it more declarative in any deeper technical sense.
>> Name generation is still an impure effect, albeit a benign one.
>
> For me, as a fan of reduction semantics, having all of the semantics
> explainable in the term syntax is an advantage!-) While it is simple to map
> between the two approaches, the nu-binders are more "declarative" in terms
> of simpler program equivalences: for gensym,
> one needs to abstract over generated symbols and record sharing
> of symbols, effectively reintroducing what nu-binders model directly.

The program equivalences are the same, up to annoying additional
congruences you need to deal with for nu-binders, which complicate
matters. Once you actually try to formalise semantic reasoning (think
e.g. logical relations), it turns out that a representation with a
separate store is significantly _easier_ to handle. Been there, done
that.

> gensym is more "imperative" in terms of the simplest implementation:
> create a globally unused symbol.

Which also happens to be the simplest way of implementing
alpha-conversion. Seriously, the closer you look, the more it all
boils down to the same thing.

>>> As Brendon mentions, nu-scoped variables aren't all that different
>>> from lambda-scoped variables. It's just that most implementations
>>> do not support computations under a lambda binder, so lambda
>>> variables do not appear to be dynamic constructs to most people,
>>> while nu binders rely on computations under the binders, so a
>>> static-only view is too limited.
>>
>> I think you are confusing something. All the classical name calculi
>> like pi-calculus or nu-calculus don't reduce/extrude name binders
>> under abstraction either.
>
> Not under lambda-binders, but under nu-binders - they have to.
>
> If was explaining that the static/dynamic differences that seem to make
> some meeting attendees uncomfortable are not specific to nu-scoped
> variables, but to implementation strategies. For lambda-binders, one can get
> far without reducing below them, but if one lifts that restriction,
> lambda-bound variables appear as runtime constructs, too, just as for
> nu-binders and nu-bound variables (gensym-ed names).

Not sure what you're getting at precisely, but I don't think anybody
would seriously claim that nu-binders are useful as an actual
implementation strategy.

/Andreas


More information about the es-discuss mailing list