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 <ro...@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 <etan...@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 > ____________________ Racket Users list: http://lists.racket-lang.org/users
