backwards incompatible change to redex: does it break your models?

[Robby Findler]

I've recently pushed a change to Redex
(https://github.com/racket/redex/commit/cbb2d88b) that disallows the
names of non-terminals in shortcuts in reduction relations. I did this
after seeing someone (quite reasonably!) assume that using a
non-terminal there meant the shortcut would work only for terms
matching those non-terminals, which is not how things actually work.

The upside of making this an error is that, instead of having to study
the minutiae of the reduction-relation-relation construct in the docs,
Redex users are told when they think redex is fancier than it is in
this respect.

The downside is that this broke a bunch of old models I had lying
around. I've fixed them (it's easy to do), but I worry that someone
who gets out an old model to show it to someone will be greeted with
this unexpected error message.

Any opinions on whether or not I should revert this commit?

Robby

[William J. Bowman]

I noticed this last week when I upgraded Redex for other reasons. It
broke one of my models, and I was momentarily confused. In fact, I
took the error message to mean I had somehow introduced an error and
spent some time staring at my tests to see if I had introduced a
syntax error. I only fixed the issue after investigating the git
commits to Redex.

It is a little confusing that, in this one place (AFAIK), I have to
arbitrary names rather than non-terminal names. It is also strange
that my context non-terminal do not trigger this error. That is, with
non-terminals E and e defined, [(--> (in-hole E e_0) (in-hole E e_1))
...] triggers an error while [(--> (in-hole E e0) (in-hole E e1))]
does not; perhaps this is just my misunderstanding of how
reduction-relation works.

--
William J. Bowman

> --
> You received this message because you are subscribed to the Google Groups "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to racket-users...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Robby Findler]

The reason the "E_1" and the "e_1" are treated differently is that the
"e" is mentioned in "binding" position of the shortcut. That is what
makes it special. Does this make sense? (Have a read of the paragraph
in the redex docs for reduction-semantics that talks about shortcuts
and let me know if it makes more sense now and, even better, if you
have any suggestions for edits!)

What if I were to actually make it do what people seem to think it
does, in the case that the chosen name is a non-terminal? So, if you
write a shortcut whose name is NOT a non-terminal, say "x" then it
would be like you wrote "any_x". And if you used a non-terminal, then
the shortcut would apply only when the expression actually matches the
corresponding non-terminal. Redex would still have to insist that the
parameters to the shortcuts are identifiers, but I could add in that
restriction?

This is also backwards incompatible, but in a different way, tho. So
that's slightly worrying. This form of backwards incompatibility has
the downside that it will just make things stop reducing instead of
getting a syntax error. So we'd have to like it a LOT to go this way.

Robby

[William J. Bowman]

On Sun, Dec 20, 2015 at 08:42:25PM -0600, Robby Findler wrote:
> The reason the "E_1" and the "e_1" are treated differently is that the
> "e" is mentioned in "binding" position of the shortcut. That is what
> makes it special. Does this make sense?

Yes, thank you.

> (Have a read of the paragraph
> in the redex docs for reduction-semantics that talks about shortcuts
> and let me know if it makes more sense now and, even better, if you
> have any suggestions for edits!)

I read through the documentation at
http://pkg-build.racket-lang.org/doc/redex/The_Redex_Reference.html?q=reduction-relation#(mod-path._redex/reduction-semantics).
The closest paragraph I can see to talking about this seems out of date.

"Each shortcut clause defines arrow names in terms of base-arrow-name
and earlier shortcut definitions. The left- and right-hand sides of a
shortcut definition are identifiers, not patterns and terms. These
identifiers need not correspond to non-terminals in language."

Of course now, the last sentence requires s/need not/must not/. I would
also add a final sentence such as "Therefore, the output of the shortcut is
not checked against the syntax of any non-terminal."

> What if I were to actually make it do what people seem to think it
> does, in the case that the chosen name is a non-terminal? So, if you
> write a shortcut whose name is NOT a non-terminal, say "x" then it
> would be like you wrote "any_x". And if you used a non-terminal, then
> the shortcut would apply only when the expression actually matches the
> corresponding non-terminal. Redex would still have to insist that the
> parameters to the shortcuts are identifiers, but I could add in that
> restriction?
>
> This is also backwards incompatible, but in a different way, tho. So
> that's slightly worrying. This form of backwards incompatibility has
> the downside that it will just make things stop reducing instead of
> getting a syntax error. So we'd have to like it a LOT to go this way.

The fact that it will cause previously good code to fail silently
is rather unacceptable. Although, I think this changed behavior is
preferable because it matches the behavior of much of the rest of Redex,
and matches what people seem to except.

Perhaps a different syntax for this changed version of shortcut, and
deprecating the current version?

--
William J. Bowman

[Robby Findler]

I somehow failed to get back to this before the release, and so the
currently available version of Redex will produce syntax errors for
such models. Lets hope it isn't too painful for people and if it is,
we can maybe try to unfix it.

Robby