<div dir="ltr"><br><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, Sep 4, 2013 at 9:01 AM, Eric Tanter <span dir="ltr"><<a href="mailto:etanter@dcc.uchile.cl" target="_blank">etanter@dcc.uchile.cl</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">Right, all this boils down to the following "strange" (although technically understandable, I guess) behavior:<br>
<br>
if metafunction `different' is defined, then:<br>
<br>
> (term (different x x))<br>
#f<br>
<br>
if it is not defined then:<br>
<br>
> (term (different x x))<br>
'(different x x)<br>
<br>
which, in any context expecting to see if something is #t, is not distinguishable.<br>
<br>
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.<br>
<br>
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.<br>
<br></blockquote><div><br></div><div>Yeah, I know. This is a general problem in Redex.</div><div><br></div><div> <br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
<br>
BTW, the doc of `term' says:<br>
"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)."<br>
<br>
But, if `different' is defined, then:<br>
> `(different x x)<br>
'(different x x)<br>
<br>
So the doc should also say something about metafunctions appearing in the term, and how they are treated, no?<br>
<br></blockquote><div><br></div><div>Right!</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
<br>
As for backwards compatibility issues, I don't know how much people rely on side-condition taking something not-#f/#t... Probably too much :)<br>
(also, there could be a `side-condition-soft' variant that is not strict in the boolean-ness, or vice-versa)<br>
<br></blockquote><div><br></div><div>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.</div><div><br></div>
<div><div>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.</div></div><div><br></div><div>Robby</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
Thanks,<br>
<br>
-- Éric<br>
<div class=""><div class="h5"><br>
<br>
On Sep 4, 2013, at 8:22 AM, Robby Findler <<a href="mailto:robby@eecs.northwestern.edu">robby@eecs.northwestern.edu</a>> wrote:<br>
<br>
> 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.<br>
><br>
> Or perhaps you're already getting that and you're saying that side-conditions in judgment-forms should insist on receiving booleans?<br>
><br>
> 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?<br>
><br>
> Robby<br>
><br>
><br>
> On Tue, Sep 3, 2013 at 9:10 PM, Eric Tanter <<a href="mailto:etanter@dcc.uchile.cl">etanter@dcc.uchile.cl</a>> wrote:<br>
> Hi,<br>
><br>
> Strangely, `side-condition' matches when the associated expression fails with an error.<br>
><br>
> For instance, using the redex tutorial example, if one writes:<br>
><br>
> [(types Γ x_1 t_1)<br>
> (side-condition (/ 1 0))<br>
> ------------------------------------<br>
> (types (x_2 : t_2 Γ) x_1 t_1)]<br>
><br>
> Then the rule applies, as if it was (side-condition #t).<br>
><br>
> Of course, (/ 1 0) is not really realistic, but the same happens if one writes:<br>
><br>
> [(types Γ x_1 t_1)<br>
> (side-condition (different x_1 x_2))<br>
> ------------------------------------<br>
> (types (x_2 : t_2 Γ) x_1 t_1)]<br>
><br>
> 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.<br>
><br>
> 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?<br>
><br>
> Cheers,<br>
><br>
> -- Éric<br>
><br>
> ____________________<br>
> Racket Users list:<br>
> <a href="http://lists.racket-lang.org/users" target="_blank">http://lists.racket-lang.org/users</a><br>
><br>
<br>
</div></div></blockquote></div><br></div></div>