[e-lang] Scope restriction on Macros

[Brandon Moore]

Mark Miller wrote:
> On 9/27/06, Brandon Moore <brandonm at yahoo-inc.com> wrote:
>   
>> Thinking about scoping, I reviewed the note on E macros at
>> http://www.erights.org/data/irrelevance.html
>>
>> I don't see exactly what restriction is being proposed. I'm wondering
>> whether desugaring
>> let x = exp in exp2
>> to
>> (fun x {exp2}) (exp)
>> is an error even if exp doesn't actually mention x.
>>     
>
> To avoid issues I don't think you meant to raise, let's assume the
> pre-expansion syntax was
>
>     let x = (exp) in {exp2}
>
> The pre-expansion scope analysis says there's a scope box that starts
> at the "let" and ends at the close curly. The "x" visible above is a
> defining occurrence of "x". The left-to-right order in the scope box
> is as shown, so this "x" is in scope in exp and exp2, and any further
> identifiers bound on exp are in scope in exp2.
>
> To make the expansion proper E, it'd be "(fn x {exp2}) (exp)". To
> avoid other issues I doubt you meant to raise, let's place curlies
> around that in the expansion as well, so let's say the above expands
> to
>
>     {(fn x {exp2}) (exp)}
>
> If exp doesn't mention "x", and exp does not define any variables used
> by exp2, and there are no names for which both exp and exp2 define
> variables, then the original would be accepted and would expand as
> above without an error. When any of these conditions are violated,
> then the original is statically rejected, because the pre-expansion
> scope analysis yields different bindings from the post-expansion scope
> analysis.
>   
I wasn't completely clear on this from "The Power of Irrelevance".
It seemed maybe it could be saying that an error would be signaled if 
computing the set of bindings in scope at exp before and after the 
expansion gave different environment. Reading more carefully, "Expansion 
happens after scope analysis" suggests pretty strongly that there's no 
nonsense about complaining about ambiguities involving names that are 
never used.

Perhaps this is a simpler way to think about the expansion process as 
well - resolve the binding first, then let a macro work on an AST with 
variables like "x bound by *that* pattern over there". You'd have to do 
a few extra checks on the AST you get back, but it would look more like 
syntactic validity checks rather than comparing pre- and port-expansion 
scoping.

>> It's a mismatch if
>> you compare the actual set of bindings in effect at each expression, but
>> not if you only look at what binds the variables that actually appear in
>> the code. I'd recommend the latter, if that isn't already what you
>> meant.
>>     
>
> I'm sorry, but I don't understand what you mean by the latter. Could
> you please clarify? Thanks.
>   
"The latter" means the scoping rules you have, as opposed to computing 
the environments in effect around bits of code before and after 
expansion and complaining if they differ.

>> Perhaps you could improve on this a bit, by letting the macro
>> explicitly declare that the binders from some pattern shouldn't be
>> mentioned at all in a particular expression, and provide a more specific
>> error message when things go wrong.
>>     
>
> I may not understand what you're suggesting, because I don't see how
> (what I think I understand) would help.
>   
It doesn't help accept more programs, but might help with error 
messages, and perhaps to support a more exact translation into the 
kernel. I'm thinking a "for" macro could explicitly declare that the 
loop variable doesn't scope over the definition of the collection to 
traverse, and that declaration would be a great place to hang a 
macro-specific error message, rather than getting some generic error 
"scope ambiguity: x bound at 11:15 before expansion, but 5:7 after".

Thinking a little more perhaps providing names for each argument to the 
macro would be enough to generate nice error messages. Saying for has a 
"item pattern", "collection definition", and "body" would be plenty to 
augment the sparse error above with a description like "Bindings from 
item pattern appear to scope over collection definition only before 
expanding macro for".

 From another perspective, if editors try to make it possible to switch 
between expanded and unexpanded forms, it might be nice to indicate at 
least in the expanded for that using some names in a particular 
expression will lead to scope errors. I'm thinking of a "hide (bindings) 
in {expr}" construct, to explicitly remove some names from a scope. This 
would perhaps be usable in it's own right in cases where a large 
complicated block of code that doesn't need much authority is for some 
reason being defined inline in a scope where powerfully capabilities are 
visible.
If nothing else, this reminds me that it should of course be impossible 
for any code synthesized by a macro to be captured by bindings in scope 
at the macro invocation.
>> This reminds me a bit of IF logic:
>> http://planetmath.org/encyclopedia/IFLogic.html
>>     
>
> Could you give a less mathematical summary of this work?
>   
It's mostly normal logic, except you can say that the choices made at 
certain quantifiers
in a formula shouldn't depend on some binder that seems to enclose them. 
It starts with a game-theoretic interpretation of connectives. A few 
examples:
If it's your turn and the top of the proof is F /\ G, your choose 
between proving F and G.
If the top is a forall, your opponent picks a value, and then you have 
to prove the body.
If you reach a negation, your opponent starts trying to prove the body, 
and you have to stop them.

The IF extension to this is marking up formula with informational 
independence rules.
For example, a formula like forall x . F /\ G might be annotated to say 
your opponent doesn't have to show you what they picked for x until 
after you've committed to one of F or G, just like you generally have to 
make a move in a card game without seeing what your opponent drew in the 
last turn.

>> On to other things:
>>
>> (I'd like to note that Haskell follows a left-to-right binding order in
>> the case of lets, because it does let a name scope over its own
>> definition, and relies on lazy evaluation to sort it out.)
>>     
>
> E does something similar for def expressions, using promises instead
> of lazy evaluation:
>
>     ? interp.setExpand(true)
>     ? def x := [1, x, 3]
>     # expansion: def [x__1, xR__3] := Ref.promise()
>     #            def res__5 := def x := __makeList.run(1, x__1, 3)
>     #            xR__3.resolve(x)
>     #            res__5
>
>     # value: [1, <***CYCLE***>, 3]
>
>
>   
>> The thinking about scoping I was doing concerned using lambdas and
>> ordinary functions to emulate/provide simple scope-building sugar.
>> As a quick example, for loops could be used as:
>>
>>  foreach [0..3] \x ->
>>    foreach [0..5] \y -> do
>>      ... stuff with x,y ...
>>
>> ("\var1 var2 .. varN -> body" is Haskell for lambda, and
>>  "do" introduces a block of statements)
>>     
>
>     ? pragma.enable("lambda-args")
>
> The above turns on the experimental "lambda-args" syntactic extension,
> which allows the use of scope-respecting control structure syntax to
> invoke user defined control abstractions.
>
>     ? def __for := <elang:control.__for>
>
> The above imports a foreach-like control abstraction, which we use to
> express your example below:
>
>     ? __for (0..3) each x {
>     >     __for (0..5) each y {
>     >         println(`[$x,$y]`)
>     >     }
>     > }
>     [0,0]
>     [0,1]
>     [0,2]
>     ...
>
> In the expansion of this, each "each" clause is packaged up as a
> closure and sent as an argument in a message to the __for object. This
> expansion exactly preserves source scope relationships, so the above
> expansion-surprise-reject issues don't arise.
>   
This sort of notation should handle many cases. I suppose the pattern 
(should be a pattern, anyway) can be omitted if you just want to control 
evaluation? This seems to even cover a sort of case construct, if you 
don't mind trying each option in turn, and catching pattern match failures.

It seems a bit odd to me to devise such a nice plan for binding if 
macros otherwise make arbitrary transformations to code. Bindings are 
especially important because they carry permissions, but it seems like 
it would still be hard to rule out much in a security review if you had 
to conservatively assume a macro invocation could expand to any 
well-formed expression (taking that to include proper scope discipline). 
lambda-args seem like a nice restriction on macros, from this point of view.

>> Maybe it's worth including some syntax like this to make it easy to
>> provide simple scope-handling things, and to provide a uniform
>> appearance for those things.
>>     
>
> Does the above "lambda-args" syntax provide what you need? If so,
> that'd be great, because it's much cleaner than introducing
> user-defined macros into E.
>   
It seems like quite a lot should be covered by this, combined with 
quasiliterals for places that actually need new syntax.


Brandon