Lambda the Ultimate

I have hobby-researched the topic of hygiene for quite some time, and it's become a no-brainer for me that hygiene is good. The reason is that macros can be viewed as "programmable inline functions", and when considering inlining, it's quite clear that renaming of the variables introduced by an inlined piece of code, as well as making sure that variables used by that piece of code still point to their original bindings when the code is inlined, is necessary.

So it seems that there are two fundamental issues, which are sometimes referred to as "hygiene" vs "referential transparency": introduction of names vs use of names.

When a macro introduces a name into its output, we want to automatically rename (or otherwise mark) that name, so that it's actually invisible at the point of the macro call. (Except when we want to introduce a visible name, which requires the use of a hygiene breaker, a function that can inject a name into a particular context.)

When a macro (expansion) uses a name, we want to make sure that that name cannot be shadowed by the surrounding context of the macro call. Somehow, a name used by a macro expansion needs to remember its original binding, namely the binding that was in effect where the macro was defined (as opposed to called).

My questions:

• Are these the issues "necessary and sufficient" to consider when thinking about and implementing hygiene, or is there something I'm missing?
• What about SRFI-72? If I understand it correctly, SRFI-72 proposes a different hygiene rule than standard Scheme, in particular around the issue of quasiquotation. Is this hygiene rule state of the art, or is that a point that is being debated and/or researched?

Thanks!

Hello everyone,

First, thank you for reading this post.

I am currently creating an application that deals with Typed Lambda Calculus expressions and I have a serious problem. I have been looking everywhere for the definition of order of a type and after reading several books and articles, the only thing I found was the wikipedia page of Simply Typed Lambda Calculus. There, it shows such definition (even though the recursive function that someone wrote and the text that someone added later do not really match... to my opinion)

If anyone knows or has ever seen the definition of assignment of order to a lambda calculus type, I would really appreciate to know the source, book, article... that I can reference in my work.

Thank you,
Best,
Mark

I've been trying to find papers about garbage collection for a pure langauge. I can't find anything closer than garbage collectors for langauges that seldom mutate their objects. I've read a lot of Henry Baker's papers, and a few others. It seems to me that there should be big advantages to garbage collecting a pure language. Can anyone suggest any papers, either positive or negative, on the topic?

The reason I feel there should be advantages is that objects in a pure langauge can only reference older objects. Also which objects a given object references never change, so perhaps contiguous chunks of unchanging objects could arise.

[edit: Thomas Lord pointed out that I am not talking about pure langauges, but an even more restricted class of language. I was thinking about total pure languages, but I don't think you need totality to ensure that all objects only reference older objects, so that your reference graph is acyclic. I'd still love papers on garbage collection specialized to pure languages or total languages.]