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

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/89a85fa1/attachment-0001.html>