John-<br><br>I haven't looked at this in detail, but I should point out that one important class of use cases requires the presence of these exceptions. See <a href="http://gafter.blogspot.com/2006/10/concurrent-loops-using-java-closures.html">http://gafter.blogspot.com/2006/10/concurrent-loops-using-java-closures.html</a>. This kind of API is implemented by catching the unmatched nonlocal transfer exception and retrying the transfer in the correct thread.<br>
<br>Also, as Mark Mahieu has pointed out, function types are merely a syntactic shorthand for interface types. In order to take the approach you suggest, they would have to be something fundamentally different.<br><br>Regards,<br>
Neal<br><br><div class="gmail_quote">On Thu, Nov 20, 2008 at 10:27 AM, John Longley <span dir="ltr"><<a href="mailto:jrl@staffmail.ed.ac.uk">jrl@staffmail.ed.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<br>
Dear Java closures people,<br>
<br>
I very much appreciate your interesting and enterprising work on Javac.<br>
As a theoretically minded researcher in programming languages, I have a<br>
suggestion to offer regarding a possible scheme for static analysis of<br>
programs involving return/break/continue, so as to pre-empt<br>
UnmatchedNonlocalTransfer exceptions at runtime.<br>
<br>
My colleague Phil Wadler at Edinburgh University recently drew my attention<br>
to your work, suggesting that some of my own research ideas might find<br>
applications there. Having studied your proposal (v0.5), it does indeed seem<br>
plausible to me that this may be the case, so this message is a first attempt<br>
at trying to convey my thoughts in Java terminology. Of course, it's highly<br>
possible that you have thought through this kind of thing already - or that<br>
I've misunderstood or overlooked something important! - but in any case,<br>
I'd be very interested in discussing the issues further.<br>
<br>
If I've got it right, my proposal has the following characteristics:<br>
<br>
* It consists simply of a compile-time checkable restriction on programs of<br>
the Javac language exactly as proposed in the spec for v0.5. No additional<br>
annotations by the programmer are required.<br>
* Programs obeying the restriction will never throw an<br>
UnmatchedNonlocalTransfer exception at runtime.<br>
* The restriction doesn't rule out any standard Java programs (i.e. programs<br>
not involving closures).<br>
* The restriction doesn't seem to exclude any of the motivating examples<br>
of Java programs with closures that I have seen so far.<br>
* More tentatively, if the restrictions were adopted as part of the language<br>
spec, I believe this might also permit a simplification of the currently<br>
proposed system for tracking exceptions, yielding the same safety<br>
properties but requiring fewer exception-related annotations by the<br>
programmer. However, I won't go into details of this in the present note.<br>
<br>
I'll describe the idea here using Java terminology. However, I'm also hoping<br>
(soon!) to produce a draft paper presenting a toy language with formal typing<br>
rules etc. which illustrates the essential issues, along with a proof of the<br>
desired safety property for this language.<br>
<br>
So here goes. I'll concentrate here on the restriction insofar as it affects<br>
the use of "return", and then briefly comment on "break" and "continue".<br>
<br>
The restriction consists of two aspects:<br>
<br>
* A restriction on assignment expressions where the variable being<br>
assigned to is of function type. (Note however that *initializers* for<br>
variables of function type are not restricted, except as prescribed by<br>
the ordinary rules of Java, e.g. we can't have "return" if we're not<br>
within a method or constructor body.)<br>
* A restriction on "return" statements themselves.<br>
<br>
To describe the restrictions, the following notions are useful.<br>
First, we suppose that in some preprocessing phase, the compiler has<br>
annotated each occurrence of a method or constructor declaration with a<br>
unique *target label*, and moreover has annotated each occurrence<br>
of "return" with the appropriate target label as determined by lexical<br>
scoping (i.e. with the target label of the closest enclosing method or<br>
constructor declaration).<br>
<br>
By a *dynamic element*, we shall mean either a variable of function type<br>
or a target label. I don't think this is an especially good name (other<br>
suggestions welcome!), but the intuition is that a dynamic element can be<br>
"invoked" - by being applied in the case of a variable of function type,<br>
or by being jumped to in the case of a target label - causing a computation<br>
which might trigger (or itself be) an attempted transfer of control.<br>
By contrast, a variable of primitive type is not considered "dynamic" since<br>
there is nothing to "invoke". (It might seem odd that variables containing<br>
references to objects are *not* deemed to be dynamic - roughly, this is because<br>
a method invocation cannot *in itself* be responsible for a non-local transfer,<br>
except indirectly via some other dynamic element such as a field in the<br>
target object.)<br>
<br>
Every dynamic element has a *scope*: the scope of a variable is<br>
defined as usual, while the scope of a target label is deemed to be<br>
the whole of the corresponding method or constructor declaration.<br>
We define a partial order relation on dynamic elements as follows: y << x if<br>
the scope of x strictly contains that of y. (The important intuition here is<br>
"x may outlive y".) We also write y <<= x if the scope of x contains or is<br>
equal to that of y.<br>
<br>
We also have the usual notion of a variable appearing *free* in an<br>
expression e. In addition, we say a target label t appears *free* in e if<br>
e contains a return statement annotated with t and not "bound" by a<br>
method/constructor declaration annotated by t within e itself.<br>
<br>
We can now give an easy-to-understand but slightly crude first cut at our<br>
restrictions as follows (I'll improve on this below):<br>
<br>
* In an assignment expression x = e where x is of function type,<br>
no dynamic element y << x appears free in e.<br>
* In a statement return e annotated with target label t,<br>
no dynamic element y <<= t appears free in e.<br>
<br>
Thus, for example, the following four code fragments are forbidden:<br>
<br>
1. {=> int} x ; // a field declaration, say<br>
void m () {<br>
x = {=> return 5 ;}<br>
}<br>
// scope of target label narrower than that of x<br>
<br>
2. {=> int} x ;<br>
void m () {<br>
{=> int} y = {=> return 5 ;} ;<br>
x = y ;<br>
}<br>
// scope of y narrower than that of x<br>
<br>
3. return {=> return 5 ;}<br>
// both returns will have the same target label here<br>
<br>
4. {=> int} x = {=> return 5 ;} ;<br>
return x ;<br>
// scope of x is narrower than that of target label<br>
<br>
Whilst this version of our restriction suffices to guarantee safety of<br>
returns, it imposes some possibly annoying restrictions on the way the<br>
programmer has to write things. For example, under the above rules<br>
one cannot write<br>
<br>
{int => {=> int}} K = {n:int => {=> n}} ;<br>
{=> int} f ;<br>
{ {=> int} g = {=> 5} ;<br>
f = K.invoke (g.invoke()) ;<br>
}<br>
<br>
even though it is OK to write<br>
<br>
{int => {=> int}} K = {n:int => {=> n}} ;<br>
{=> int} f ;<br>
{ {=> int} g = {=> 5} ;<br>
int n = g.invoke() ;<br>
f = K.invoke(n) ;<br>
}<br>
<br>
which is not essentially different. Thus, the programmer would sometimes<br>
have to rewrite code in an unnatural style in order to conform to the<br>
above rules.<br>
<br>
The point about this example is that in the assignment<br>
<br>
f = K.invoke (g.invoke()) ;<br>
<br>
the occurrence of g is not "dangerous", because the subexpression<br>
g.invoke() is evaluated to a ground value (5) before the assignment is<br>
performed, so there is no way for the dynamic behaviour of g to find<br>
its way into that of f. One can take account of this via a slightly more<br>
fine-grained version of our restrictions as follows.<br>
<br>
Let's say a syntactic subexpression e' of e is *normal* if e' does not<br>
appear inside a closure literal in e (i.e. underneath a lambda).<br>
And say a dynamic element y *critically appears in* an expression e<br>
if there is an occurrence y_0 of y which is not contained in any normal<br>
subexpression e' of non-function type.<br>
<br>
Thus, in the above example, g appears in K.invoke (g.invoke()),<br>
though not critically. However, the appearance of g in {=> g.invoke()}<br>
*is* critical, because the invocation of the dynamic behaviour of g<br>
is delayed.<br>
<br>
With these notions in place, we may now relax our restrictions to the<br>
following (just by replacing "appears" by "critically appears"):<br>
<br>
* In an assignment expression x = e where x is of function type,<br>
no dynamic element y << x critically appears free in e.<br>
* In a statement return e annotated with target label t,<br>
no dynamic element y <<= t critically appears free in e.<br>
<br>
One further simple relaxation is worth mentioning. For an assignment x = e,<br>
the appearance of some y << x isn't dangerous if y is a variable and there<br>
is no intervening target label between y and x. So we could in general define<br>
y <<< x if for some target label t we have y <<= t << x, and then replace<br>
"y << x" by "y <<< x" in the restriction on assignment expressions.<br>
<br>
So that's the idea. It should now be reasonably clear how to extend this<br>
scheme to deal with "break" and "continue", by annotating loop constructs<br>
with target labels at appropriate points.<br>
<br>
Of course, a few adjustments might be needed to take account of all aspects<br>
of Java (e.g. I guess some care is also needed over where to put the target<br>
labels in try-finally statements), but I'm hopeful that in essence the scheme<br>
should be able to do everything one wants, without sacrificing much of<br>
importance in terms of programming power or convenience.<br>
<br>
Thanks for reading this far! I would be interested to know what you think,<br>
so any reactions/queries/problematic examples gratefully received.<br>
<br>
Cheers,<br>
John Longley<br>
(Lecturer, School of Informatics, University of Edinburgh, Scotland)<br>
<br>
<br>
[PS: Please reply to my email address, as I guess I'm not a recipient of<br>
this mailing list.]<br><font color="#888888">
<br>
<br>
-- <br>
The University of Edinburgh is a charitable body, registered in<br>
Scotland, with registration number SC005336.<br>
<br>
<br>
</font></blockquote></div><br>