[racket-dev] syntax-property guards? (was: Re: The Stepper strikes again)

On Aug 13, 2011, at 12:58 PM, Sam Tobin-Hochstadt wrote:

> On Sat, Aug 13, 2011 at 12:51 PM, Eli Barzilay <eli at barzilay.org> wrote:
>> 10 minutes ago, Sam Tobin-Hochstadt wrote:
>>> `match' also currently adds a syntax property to help the Typed
>>> Racket type checker understand the expansion.  Like 'disappeared-use
>>> for Check Syntax, this property is in theory semantically
>>> independent of Typed Racket, but only used there.
>> 
>> No, when your property is called `typechecker:called-in-tail-position'
>> it is not independent of a "typecheker".  It will be, if it gets a
>> generic name, and gets documented which turns it from a backdoor for a
>> backward dependency to a known API.
> 
> The *semantic* independence of the property and the typechecker
> implementation is not determined either by the name of the property or
> the documentation.


There are two levels of semantics here: 
 -- operational semantics of your module, which makes you correct
 -- 'in spirit' semantics, which makes Eli correct. 

I will say that even though I cannot define 'in spirit' formally, 
I am with Eli here.