On Second Thought (Binding Polymorphism)

Maybe I spoke too soon. While Shriram's automaton language does in fact provide an example of binding abstraction, in the sense that the client doesn't know what the binding properties are, it is not an example of "binding polymorphism." That is, the macro writer still knows exactly what the binding properties of each subexpression are.

So as far as I know, the ability to delay the decision about the binding properties of names to the last possible moment is not in fact necessary for the automaton language example, which means that it has not in fact answered my earlier question.

I think what led to my confusion is that Macros that Work claims that the ability to delay the discovery of binders until the last possible moment is necessary to allow binding abstractions. But I don't think that's quite true. Rather, it's only necessary to allow the property I've been calling binding polymorphism, such as my contrived apply-syntax example.