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

Two minutes ago, Sam Tobin-Hochstadt 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.

+1.


> 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.

To rephrase what Carl said: what if you change the TR "type chekcer"
to a "type verifier"?  You'd change the property name, which means
that a TR change has lead to a change in match.  That's the actual
dependency.


> 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.

Exactly -- having "typechecker:" in the name is bogus.  Would you mind
changing it to `swindle:called-in-tail-position'?

-- 
          ((lambda (x) (x x)) (lambda (x) (x x)))          Eli Barzilay:
                    http://barzilay.org/                   Maze is Life!