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

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.


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?


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)

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
>