On Wed, Sep 4, 2013 at 9:01 AM, Eric Tanter <etan...@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 <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
