paulstansifer / redex Goto Github PK

Robby says: "One thing to also look into for Redex: in addition to an
alpha-sensitive equality, we also need an alpha-sensitive hashing. I
think it's straightforward: just normalize and then call the
equal-based hash function that's built into Redex.

We'll need this for traces (the way it collapses different paths to
the same term is based on hashing)."

Currently, rib and shadow have no functional difference.

proposed design: if default-equiv accepts three arguments, also give it the language as an argument

Freshening is (and should be!) nondeterministic. But metafunction caching assumes that metafunctions are deterministic. I think that we need to disable caching for any metafunctions that destructure any binding forms (or, at least, any binding forms that bind names). It sounds pretty costly, unfortunately.

Essentially, the "default" binding form that applies to everything will have special behavior: even though it #:exports nothing; any binders free in its subterms should be free in it (this is already inherently true of references).

By accident, this is already mostly the case, and indeed needs to be the case for the Right Thing to happen in certain situations.

This proposal will make non-binding-specified lists less like binding forms. Suppose that one is passing multiple arguments to a metafunction, one of which is (define x 1) (which exports x), and one passes those arguments as a plain list (in fact, this is exactly how metafunctions normally operate). The list must then be destructured, and therefore freshened. If x is treated as free, it must not be renamed, but normally, if (define x 1) is neither imported nor exported, then x is treated as bound, and therefore in need of renaming.

This would make it possible to express let* in its natural syntax.

I think that this can be done Dybvig-style, but I worry that it might only be possible if we were willing to put non-plain-old-data into terms, and break term-destructuring-with-anything-other-than-redex-match.

The basic approach is simple: the enumeration for a binder is a single (fresh) atom, since it doesn't matter what you choose. Inside a scope, the finite enumeration of the names that are bound in that scope comes before the infinite enumeration of free names (on the theory that choosing different free names is not as interesting as choosing different bound names).

However, this probably won't work: (a) Whether a name is a binder or not is not defined until the term is complete, and can be matched against a pattern. (b) This requires that all bound names be selected before all free names.

For (a), we might be able to use an approximation: traverse each nt's pattern, intersecting it against the binding patterns. If a variable is always used as a binder, treat it as such. If a variable is never used as a binder, treat it as a reference. Otherwise, enumerate both possibilities, maybe?

For (b), dependent cons might do the trick, as long as forward- and self- references don't exist. They're rare, but they are perfectly legal. The only thing that I can think of to deal with them, though, is to first generate the entire shape of the Redex value ("shape" here means everything but the particular variable names), and only then enumerate over the variable name possibilities.

The shape-first trick would also solve problem (a), I suppose: just match against the shape. And, as long as there exists at least one reference position, there is always an infinite enumeration of possible namings, which I think helps matters?

...make it a metafunction! (but one that uses default-language, instead of setting it)