[PRL] hygienic macros

[Riccardo Pucella]

Hi Ryan,

>>> Has anyone from the syntactically inclined subset in PRL tried to
>>> implement (and failed) a macro expander in CαML or Fresh OCAML? I
>>> believe that this might shed some light on the nature of hygiene. --
>>
>> Interesting question. A while back, I thought about whether  
>> nominal logic
>> (the formalism underlying C{\alpha}ML and Fresh OCaml could help  
>> formalize
>> the notion of hygiene. Mitch told me that Dave and him had a look  
>> at that a
>> while back, and concluded that the framework was inappropriate. I  
>> do not
>> know the details, however.
>
> Part of the hygiene principle of macro expansion in Scheme---stated  
> very
> loosely---requires that an identifier introduced by a macro can only
> bind other identifiers introduced in the same macro step.
>
> There is a gap between the expansion of a macro and the discovery  
> of the
> roles played by all of the identifiers it introduces, because the
> binding forms are only uncovered by the expansion of the macro's  
> output.
> Thus these post-introduction, pre-resolution identifiers must be  
> able to
> handle a variety of different roles: "As a binding occurrence, I  
> act as
> an X.1.5; as a reference I act as an X.1.5, if there is a binding for
> X.1.5 in scope; otherwise I act like an X.1, if there is a binding for
> X.1 in scope; otherwise I act like an X."
> (This situation has been compared to superposition in quantum  
> mechanics.
> In fact, Mitch, Dave, and I did prove that this superposition is
> necessary to describe Scheme's macro system. Ask me if you're  
> curious.)

I see. You cannot tell the meaning of an identifier produced by macro- 
expansion by just looking at the result of the macro expansion, but  
you need to way until the very end to see how everything "gets  
resolved". I can see how one could think of it in terms of state  
superposition. (Although I am curious in seeing the details of the  
formal proof that something like that is required.)

>
> At a workshop last year, I asked Andrew Pitts whether he had thought
> about extensions to his theory of atoms and substitution to allow
> substitutions of *part* of a name (to support compound names with
> timestamps, etc). He answered, "You mean like *molecules*? No, I
> haven't."
>
> In summary, you can't do hygiene with atoms. You need either atoms  
> plus
> an environment, or molecules.

Presumably, adding molecules to something like nominal logic should  
not be very hard. (Pitt's work is much more foundational, so I expect  
that adding molecules at that level may be more demanding.)

The $10000 question then: if I grant you a framework with molecules,  
can you derive a property characterizing hygiene?

  Cheers,
  R