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

On Aug 13, 2011 2:13 PM, "Eli Barzilay" <eli at barzilay.org> wrote:
>
> 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'?

Is this just an argument about how to name these syntax properties?  If so,
I'm happy with whatever you think I should name it.  That doesn't seem to
get us anywhere on the other questions, though.

Sam
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/dev/archive/attachments/20110813/c1edbbce/attachment.html>