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

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/dev/archive/attachments/20110813/b8d2a988/attachment.html>