Static analysis of non-local transfers: a proposal

[John Longley]

Hi Mark,

Many thanks for the speedy and encouraging response!

> If I've understood correctly, the restrictions you've described rely on
> detecting that the target of an assignment is of function type.
> However, the closures specification allows a closure literal such as
> {==> return;} to be converted to a 'compatible' interface type, and I'm
> wondering to what extent your proposal would be able to handle that?

I can see that this is an important issue. My proposal here would be that
a function type should be at least conceptually distinguished from the  
corresponding interface type, to the extent that we can think in terms  
of
a type conversion being inserted by the compiler, e.g.:

> 	static void m() {
> 		store (CONVERT {==> return;});
> 	}

I would then propose that such type-converted expressions should be subject
to a restriction similar in spirit to the others (but a bit stronger):

* In any expression CONVERT e (where CONVERT is an implicit conversion from
   function to interface type), no *shadowed* dynamic element y (i.e. one for
   which there is some target label l <<= y) may critically appear free in e.

As I see it, I don't really have any other option here, since once  
something is
treated as having an interface type, it can (under standard Java) be  
stored unrestrictedly and one loses all control of it.

[Of course, one should take care to set things up so that function application
is always permitted and isn't considered as requiring a type conversion,
even if the chosen syntax looks like method invocation on an object: e.g.

   {==> return;}.exec()

should certainly be allowed.]

I would be very interested to know whether the idea that not all closure
expressions are convertible to interface types appears at all acceptable
in terms of current thinking on type compatibility. It seems to me that
there is at least a coherent point of view which makes sense of this idea.
To wit: objects and closures clearly overlap in what they can express, but
they offer different things: objects can be stored in variables without
restriction but don't give you the non-local transfer features; while
closures give you these interesting features but (under my proposal) at the
cost of some restrictions on how they are stored. So, depending on what you
are trying to do, you can have either of these but not both at once - the
point being precisely that the combination of non-local transfer with  
unrestricted store is inherently unsafe. Type conversion thus makes  
sense
as long as one is in the intersection of the two regimes. As I say, I think
one is forced to take something like this view if one hopes to pre-empt
unmatched transfers via a static analysis.

While I'm here: there is a small loophole in what I described in my first
email, which I discovered in the course of my formal analysis. I said that
initializers needn't be subject to any special restriction - but that's not
quite true, as the following obscure scenario shows. Suppose one has a local
class declaration appearing within the declaration of e.g. a method m, and
suppose the local class has a field f of function type. Then an initializer
for f must be prevented from including a return statement that binds to
the target label of m (and likewise for assignments to f within initializer
blocks, I guess). E.g.

     {==> int} m() {
         class c {
            {==> int} f = {==> return ;}
         } ;
         return new c().f
     }

     // later:
     m().exec() ;  // throws unmatched transfer

I can certainly give appropriate restrictions to fix this problem - but on
the other hand, the issues only arises in such bizarre contexts that one
might prefer a simpler solution, such as simply forbidding fields of function
type in local class declarations appearing within the scope of a target label.

I will be much more confident of my scheme as a whole once my formal analysis
is completed! I expect to have a rough outline available within the next
couple of days.

Best wishes,
John


-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.