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

On Sat, Aug 13, 2011 at 2:05 PM, Sam Tobin-Hochstadt <samth at ccs.neu.edu> wrote:
>
> On Aug 13, 2011 1:35 PM, "Carl Eastlund" <cce at ccs.neu.edu> wrote:
>>
>> On Sat, Aug 13, 2011 at 1:26 PM, Matthias Felleisen
>> <matthias at ccs.neu.edu> wrote:
>> >
>> > 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.
>>
>> How about instead of "in spirit", we focus on program logic.  There is
>> no semantic dependence on the typechecker -- Racket can tell what the
>> program does without it.  However, programmers cannot read that code
>> and know what it is for and whether it is correct without reference to
>> the typechecker.  That's a meaningful dependency.  It makes
>> maintaining that line of code 100% dependent on the typechecker.
>
> What I mean by "semantically independent" I mean exactly that your statement
> is not correct.  The meaning of the property is defined without reference to
> the type checker.  It means "this let-bound function is probably called in
> tail position wrt the let.". This says nothing about types, and can be
> reasoned about independently.
>
> Sam

How do I know it means that?  Is the correspondence between "this
let-bound function is probably called in tail position" and the value
of the "typechecker:called-in-tail-position" property documented
outside of the typechecker?  The precise intended meaning of the
syntax property is not immediately obvious just from its name.  If it
is documented outside of the typechecker, why does it start with
"typechecker:"?

--Carl