[racket] [redex] side-condition matching upon errors

On Wed, Sep 4, 2013 at 9:01 AM, Eric Tanter <etanter at dcc.uchile.cl> wrote:

> Right, all this boils down to the following "strange" (although
> technically understandable, I guess) behavior:
>
> if metafunction `different' is defined, then:
>
> > (term (different x x))
> #f
>
> if it is not defined then:
>
> > (term (different x x))
> '(different x x)
>
> which, in any context expecting to see if something is #t, is not
> distinguishable.
>
> So there is some kind of "implicit unquoting" for defined metafunctions (I
> don't know how this is implemented under the hood), which is quite
> confusing when one would expect errors instead.
>
> I don't know if/how that can be fixed, but I can only report that the
> debugging of such silent bugs is quite frustrating.
>
>
Yeah, I know. This is a general problem in Redex.



>
> BTW, the doc of `term' says:
> "It behaves similarly to quasiquote, except for a few special forms that
> are recognized (listed below) and that names bound by term-let are
> implicitly substituted with the values that those names were bound to,
> expanding ellipses as in-place sublists (in the same manner as syntax-case
> patterns)."
>
> But, if `different' is defined, then:
> > `(different x x)
> '(different x x)
>
> So the doc should also say something about metafunctions appearing in the
> term, and how they are treated, no?
>
>
Right!


>
> As for backwards compatibility issues, I don't know how much people rely
> on side-condition taking something not-#f/#t... Probably too much :)
> (also, there could be a `side-condition-soft' variant that is not strict
> in the boolean-ness, or vice-versa)
>
>
Well, if we're willing to force clients to change their code, then it isn't
hard for them to write their own metafunctions that turn non-#f things into
#ts.

But I think you're right that just changing this is a good idea and
backwards compatibility be damned. I'll put it on my list.

Robby


> Thanks,
>
> -- Éric
>
>
> On Sep 4, 2013, at 8:22 AM, Robby Findler <robby at eecs.northwestern.edu>
> wrote:
>
> > These are not errors, technically. The side-condition form in a
> judgment-form is not unquoted, so that's a redex expression, not a Racket
> one. In other words, the side-condition is not (/ 1 0), but '(/ 1 0). Ditto
> for the "different" example.
> >
> > Or perhaps you're already getting that and you're saying that
> side-conditions in judgment-forms should insist on receiving booleans?
> >
> > I see that the current behavior for side-condition was first released
> more than a year ago, so I'm a bit worried about backwards compatibility.
> What do you think about that?
> >
> > Robby
> >
> >
> > On Tue, Sep 3, 2013 at 9:10 PM, Eric Tanter <etanter at dcc.uchile.cl>
> wrote:
> > Hi,
> >
> > Strangely, `side-condition' matches when the associated expression fails
> with an error.
> >
> > For instance, using the redex tutorial example, if one writes:
> >
> >   [(types Γ x_1 t_1)
> >    (side-condition (/ 1 0))
> >    ------------------------------------
> >    (types (x_2 : t_2 Γ) x_1 t_1)]
> >
> > Then the rule applies, as if it was (side-condition #t).
> >
> > Of course, (/ 1 0) is not really realistic, but the same happens if one
> writes:
> >
> >   [(types Γ x_1 t_1)
> >    (side-condition (different x_1 x_2))
> >    ------------------------------------
> >    (types (x_2 : t_2 Γ) x_1 t_1)]
> >
> > and forgets to define `different' (assuming it is a standard Redex
> metafunction)... Instead of a nice error that `different' is undefined, the
> rule silently applies.
> >
> > I understand that anything that is not #f is true, but arguably this
> should not apply to an error. Or is there a good reason why this is so?
> >
> > Cheers,
> >
> > -- Éric
> >
> > ____________________
> >   Racket Users list:
> >   http://lists.racket-lang.org/users
> >
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20130904/e15d5b0a/attachment.html>