I am really astonished to hear protection keys being thought
of as "brittle" under transformation: that is just the opposite
of what they are about!
Sorry to astonish you. :)
No problem!-) I was just afraid of the idea being misunderstood
or being associated with fear-inducing phrasing, either of which
can easily derail a discussion in which good ideas can otherwise
speak for themselves.
By the time we have agreed to what extent the concerns remain
valid or can be alleviated, the rest of the community may well
have stampeded away in panic! Not that this group necessarily
works that way, of course, just general human nature:-)
- Berkling's protection keys add flexibility to name-based
schemes, *removing* their brittleness under transformation;
it combines suitability for automated transformation
with readability for humans (in fact, both de Bruijn's
and the classical name-based scheme are special cases
of Berkling's)
Well, you're just asserting that Berkling's keys remove their
brittleness without evidence.
Ah, ok - I have been trying to summarize the idea on its own,
using evidence-by-logic rather than by-reference or by-example,
to avoid going through the history of Berkling style reduction
systems on this list (it has been a while, but I would be happy
to explain a bit if that would be of interest/appropriate here[*]).
From your other comments I infer that you understand how
the scheme works but also that you are still lumping together
the various related schemes that have been used in this context.
The latter might keep you from seeing what is different about
Berkling's scheme, and hence how the brittleness is removed,
by straightforward technical means (no magic or subjectivity).
Since this seems to be relevant information for a language-
specific design/spec discussion list talking about bindings, I'll
try to outline the process (even as a rough proof outline, it
beats more examples, as far as evidence is concerned). For
those of you not interested in reduction: the same issues
arise in refactoring. From memory (please excuse any errors):
Church's original lambda-K calculus was meant to pin
down the scoping issues that mathematicians and logicians
encountered; it had partially defined conversion rules (in
case of naming conflicts, the rules were simply not
applicable), so one had to choose a suitable sequence of
renamings (alpha rule) and conversion (beta rule) to
ensure that such conflicts and rule failures were avoided.
That is brittle in the strictest sense.
Later presentations of lambda-calculus mixed a bit of
renaming into conversion (either in beta reduction or in
substitution). That leads to uncontrolled renamings of
bound variables, to bypass the conflicts. That is not nice,
and it is brittle wrt programmer-chosen names.
Berkling's version just acknowledges that lambda calculus
is missing some of the terms that would allow to represent
the binding structures that can arise during conversion.
The consequence of having too few terms to represent
all intermediate results of reduction is that one either has
to avoid the conversion sequences that lead into those
holes (leading to partially defined reduction rules), or
one has to put the available terms to double use
(leading to conflicts between programmer intent and
implementation needs, as far as names are concerned).
Adding the missing terms gives the manoeuvring room
to define the conversion rules fully, without gaps and
without having to resort to renaming. So brittleness
under transformation, in both senses, is avoided.
De Bruijn's scheme doesn't help there: it has even fewer
terms than Church's (only a single term representing all
alpha-equivalent ones). Similar shortcomings seemed to
apply to most other related schemes I've seen - most of
them work technically but fail pragmatically.
Berkling's extra terms do not add error-prone complexity
in terms of binding structure, because other terms with
equivalent binding structure already exist in Church's
version. The extra terms are just designed in such a way
that both binding structure and programmer-chosen
names can be preserved during program transformations.
And I'm afraid I've seen enough evidence in my experience
to make me doubt your claim.
Does the above help? We have to be careful not to confuse
"the new thing is different" with "the new thing is brittle".
In this case, "the new system has more complex rules" can
actually mean "the new system is easier to use in practice",
because the new rules have fewer exceptions.
Just take a look at what happens to the definition of alpha-
conversion in a language with Berkling's keys. Traditionally,
when you alpha-convert a binding x, you can stop the
induction whenever you hit an inner binding (shadowing)
of x. Not so with your proposal: now you have to keep going
-- and decrement an accumulator argument to the algorithm
(not exactly obvious!) -- to look for "outer" references within
the inner binding.
Indeed. That is a direct consequence of adding the "missing"
terms (terms in which parts of the binding structure are
expressed through protection keys) - the old conversion
rules arise out of the new ones as (premature) optimizations
for the case that no protection keys are present at any stage.
But that the rules have to do more work to cover the additional
terms does not make the system "brittle" in any way - and it is
quite unambiguous what needs to be done.
Also, the shortcuts can be recovered as compile-time
optimizations: if your program starts out without protection
keys, the old rules still apply; and the new rules only introduce
protection keys if the old rules would have failed. So, if you
want to stay in the protection-free subset of the language,
you can do so. You do not have to pay if you don't use the
additional flexibility.
In fact, even the "extra work" is misleading: we could represent
the same binding structure by choosing different names, and
then the corresponding alpha-conversion/renaming would
have to do the same amount of work.
Example: if we enter a new function body, the outer 'this' is
not accessible directly, so any renaming of 'this' (if it were
feasible) could stop there; but since programmers have
adapted to that by renaming 'this' to 'that' or 'self' or ..,
we wouldn't be renaming 'this', we would be renaming
'that' or 'self' or .., and _that_ renaming would have to
'look for "outer" references within the inner binding'.
It needs a shift of perspective to see the old system as an
incomplete realization of the lambda-calculus ideas, but
once that is done, it seems clear why and how the old
system is brittle (missing terms, partially defined rules)
and how the new system is more complete/consistent.
I tend to mention de Bruijn not just because his scheme
predates Berkling's but because it helps people to
understand how protection keys work. However, since
you already understand that, I recommend that you
think about the differences to de Bruijn, rather than
the similarities; in particular, that shift-of-perspective
is a rewarding exercise!
Since it has been so long, allow me to refer to a younger
self:-) Section "2.2 lambda-calculi" in [1]. That was just
my own way of formalizing Berkling's system as part of
the introductory background for my own work.
As such, it lacks formal proofs and details, but Figures
2.2-2.5 spell out what you describe, and Theorem 2.1
outlines how Church's calculus emerges if one omits
terms involving protection keys. As an introduction,
it is way too brief to touch on the wider world of
Berkling's ideas[*], but it has the advantage of being
readily available online.
What does this mean in practice? It means that someone
refactoring at an outer level may be unaware that they've
affected the index of an inner reference by changing a
binding.
Then that is not a refactoring, is it?-) I see what you mean,
but you already have that problem if you add or remove
a binding now. As you said yourself: the binding structure
is just represented differently.
It means you lose some of the locality that you
get with traditional lexical scope.
<off topic>
It would actually be possible to recover even the bit of locality
that you refer to, but that would need a more drastic language
change (the non-locality comes because the protection keys
are attached directly to variable occurences, so adjusting
protection is non-local in the same sense as traditional
substitution is; the remedies for both non-localities work
along similar lines: propagate the information step-by-step
instead of all-at-once, move representations from meta-
language to object-language).
I doubt that this generalization would ever fly with pragmatic
programmers, but for language designers and implementers
it is interesting: if we make the protection key manipulation
explicit in the language (rather than the meta-language, as
most formalizations do), we can perform compile-time
optimizations on them (similar to compile-time garbage
collection or type-checking).
I seem to recall that I once tried to derive the more efficient
supercombinator reduction from the more general beta
reduction rules (if we make the protection key manipulations
explicit instead of pushing them right down to variable
occurrences, some of them cancel out, and never need
to be pushed into the expression).
</off topic>
A machine is much better at consistently shifting big
collections of integer indices without making a mistake.
Yes, also at managing scopes during refactoring. I prefer
tool support for refactoring (I was part of the team that built
such for Haskell98[2]), but given Javascript's nature, it would
be hard to prove any refactorings correct. So one will have
to resort to a combination of tool support and testing - still
preferable to manual refactoring (which most of us are
doing so far).
And refactoring tools can profit from having a programming
language in which program transformations can be expressed
without having to force renamings.
The problem is wider than 'this', 'this' just seems to be
the main use case where the problem surfaces in
Javascript practice at the moment.
And the reason for this is that |this| is implicitly bound.
Which, as I said in my last email, is a good motivation
for considering making it possible explicitly bind |this|.
I'm not against such attempts: thinking of 'this' as implicitly
bound is already much nicer than thinking of it as dynamically
bound, and being able to make the implicit binding explicit
(so that we can choose another name than 'this') would be
a nice option to have, even if protection keys had any chance.
However, any changes in that area would also touch the
core of what Javascript is about. There is no free lunch: if
the core language needs to be changed, that is going
to have wide-ranging effects. That does not mean that
such a change is not worth the cost.
Btw, have you ever wondered whether 'var'-bindings
are recursive?
This is a really basic question about JS, and not appropriate
for this list.
Ah, perhaps I was too implicit. Let me make the design issue
clearer, and how it relates to our discussion:
function Outer() {
var prefix = "Outer>";
function Inner () {
var prefix = prefix+"Inner>"; // this does not work;
// neither the outer nor the inner definition are
// accessible on the rhs, only the *uninitialized*
// inner binding
}
}
I know definition constructs in which the left-hand side is
available on the right-hand side (recursive value definitions
in other languages, function definitions in Javascript), and
I know definition constructs in which it isn't, but any previous
value is (assignment in Javascript, non-recursive definitions
in other languages); in all these constructs, either the current
or the previous definition is available on the right-hand side;
Javascript's 'var' is the only construct I know (apart from
memory-model bugs in Java, perhaps) in which the
left-hand side name is forced to be undefined on the
right-hand side; which means that neither the current nor
the previous definition are available on the right-hand
side, because the undefined state shadows both!
One could argue that the interim state (bound, but not
initialized) should not be exposed in an initializer, and I
would agree, but with protection keys, at least, this
should work:
var prefix = ^prefix+"Inner>"; // "Outer>Inner>"
I hope that explains why I raised this issue on this list?
.. I'm not talking
about automatic rewriting. All of these representations
of binding structure (names, de Bruijn indices, the "locally
nameless" approach, the Berkling representation you
describe) are different ways of representing graphs as
trees. For the sake of formal systems, they're all equally
expressive. The problem is that some of them are more
susceptible to human error than others.
While that is true, I did not find Berkling's system any more
error-prone than Church's in practice. As a student, I
implemented a small functional language - parser, compiler,
runtime system, based on the G-machine papers, in a
Berkling-style reduction language, and so did the other
students in that course - protection keys were not a problem
(that was a semester-long project, following on from another
semester-long introduction to functional programming, so
we had ample time and opportunity to play with the system).
I only have small-scale experience with non-Berkling lambda
calculi implementations, but I always found the automatic
renamings somewhere between confusing and annoying
(both as a user and as an implementer).
During our project implementing the Haskell Refactorer
HaRe[2], I often found the lack of protection keys in Haskell
limiting for our refactoring design choices - either we had
to initiate renamings that the programmer had not asked
for, to make the intended refactoring go through, or we
had to abandon the refactoring with an error message
indicating the naming conflict, asking the programmer
to do a rename first, then try again..
If protection keys were at all "brittle" in the face of
refactoring, none of his systems would ever have worked.
Nonsense-- there are all sorts of technologies that work
and are brittle. Ask me over a beer some time, and I'll name
a few. ;)
I assume some of them have been tested on students
or similarly suitable and unsuspecting subjects?-)
Quite contrary to being "brittle", protection keys introduce
the necessary flexibility that allows these systems to *avoid
breaking* the binding structure while automatically rewriting
the code.
I think the key to the misunderstanding here is the word
"automatically." Of course you can automatically refactor
just about any representation of variable binding. The
question with a given representation is whether it's sensitive
to small changes introduced by ordinary human refactoring
(i.e., the everyday experience of programming) and therefore
more error-prone.
"automatic rewriting" is something humans can do, too:
complex tasks can be made less error-prone by having a
consistent algorithm to follow, instead of one consisting
of simple rules with lots of exceptions.
For reference, and just as a subjective impression: students
would get protection key manipulation wrong, but they
would also get name capture wrong - the difference
seemed to be that explaining the latter took longer than
explaining the former. I would be tempted to generalize
that key manipulation errors tended to be problems of
execution, while name capture errors tended to be
problems of understanding, but I have no data to
back such intuition.
But the real answer to your question is that protection keys
do not introduce new problems here: in closed programs,
the same binding structures can be expressed without
protection keys, so all the small changes and sensitivities
already arise without them.
Of course, protection keys would give Javascript obfuscators
a new toy to play with, but they have ample toys already. So,
I am only referring to normal use in absence of reflection.
Claus
[1] http://community.haskell.org/~claus/publications/phd.html
[2] http://www.cs.kent.ac.uk/projects/refactor-fp/
( http://www.youtube.com/watch?v=4I7VZV7elnY )
[*] Only for those of you who wanted more references or
evidence of use:
I learned about Berkling's ideas mostly in Werner Kluge's
research group (only met Berkling when he visited Kluge).
Kluge tended to be more interested in how language
design influenced paradigm-specific implementations
(both abstract and real machines), but he is still the best
source of references and explanations about Berkling's
work. Kluge retired long ago, but has kept some of his
old pages around:
http://www.informatik.uni-kiel.de/inf/Kluge/
http://www.informatik.uni-kiel.de/~wk/papers_func.html
For a very brief history and some references, see the
related work section in Kluge's
"Abstract Lambda Calculus Machines"
2nd Central European Functional Programming School
CEFP 2007, LNCS 5161 (2008), pp. 112 -- 157
(available online from those urls). That last section is an
extract from one of Kluge's textbooks on the subject.
The PI-RED systems were the implementations of the
Kiel Reduction Language, based on Berkling's reduction
languages, so for reports on usage and implementation
of a Berkling-style language, you might find the online
versions of
"A User's Guide for the Reduction System PI-RED"
Kluge, W., Internal Report 9409, Dept. of Computer
Science, University of Kiel, Germany, 1994
"Using PI-RED as a teaching tool for functional
programming and program execution"
Kluge, W., Rathsack, C., Scholz, S.-B., Proc. Int. Symp.
on Functional Programming Languages in Education,
Nijmegen, The Netherlands, 1996, LNCS 1022, (1996),
pp. 231-250
"PI-RED+ An interactive compiling graph reducer
for an applied lambda-calculus"
Gaertner, D., Kluge, W. E., Journal of Functional
Programming Vol. 6, No. 5, (1996), pp. 723-756
relevant (availabe online via second url above).
_______________________________________________
es-discuss mailing list
es-discuss@mozilla.org
https://mail.mozilla.org/listinfo/es-discuss
