Nanevski and metaprogramming

Aleksandar Nanevski gave a talk at Northeastern's PL Seminar a while back on the applications of modal logic to programming language constructs. In particular, he told a nice story for a peculiar kind of dynamic binding and variable (or location?) mutation, and then he reused some of the exact same rules to talk about exceptions, and then again to talk about metaprogramming. One wonders if one can have all three at the same time (there are monad-like composition problems). And if I recall correctly, only the first story involved the diamond modality from modal logic; the other two only used the box modality.

I don't care so much about new strange ways to look at dynamic binding and exceptions. But I do care about metaprogramming. People have made type systems for metaprogramming by appealing to temporal and then modal logic before (Davies and Pfenning, "A modal analysis of staged computation"). But then box types represented closed code, and that was the end of the story. When constructing a new code value, one could refer to other "boxes" that one had "opened" in the current context, but the final code object would be a closed term.

Nanevski's boxes are parameterized over the holes in them: a set of names (the support) that the code depends on. One might call them metavariables. These names can be filled in with other code (values of box type)

It seems that the advantage of Nanevski's system is somewhat like the advantage of fibration over parameterization. One could always have encoded box types with non-empty support as functions from the support to a closed box type. This code:

box{X:A, Y:B} C

could be coded instead as the following:

(box A) -> (box B) -> (box C)

On the other hand, that commits us to an order to supply the arguments in. That's the first deficiency. Beyond that, what happens when you want to fill the X hole with a code object that itself has some support required? One can imagine how to compute the new support in Nanevski's system, but parameterization turns into a mess at that point.

So, on to Scheme macros.

Scheme's syntax objects don't have the integrity of box values. One can't say anything about the bindings within an isolated syntax object template. Here's an example:

(let ([code0 #'(+ 1 2)])
  #`(let ([+ -]) #,code0))

This is not a "nonhygienic" macro. It's just that syntax objects per se have no aversion to variable capture. It is only the macro expander that makes things "hygienic." Andre von Tonder seems like he wants to fix this particular point with his macro system proposal, but in the standard syntax-case system, that's one big difference between box values and syntax objects.

That's a distraction, though. The important feature of Nanevski's system is the support set (and metavariables are separate from variables). A better comparison would be between code expressions and syntactic templates (the things starting with #'). Then metavariables would correspond to pattern variables.

(syntax-case ()
 [(P Q R)
  #'(... P ... Q ... R)])

Only things bound by syntax-case are considered pattern variables in the template, so there's no way to have an "unbound" pattern variable in the template. Thus our macro system doesn't have a notion of a syntax object with syntactic holes in it. Sure, we can bind the names that appear within it, but those are object-level bindings, not metavariable bindings.

Would it be useful to have fibered syntax objects? Replace this pattern variable now, hold on to it for a while, replace a couple more?