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

On Aug 13, 2011, at 1:34 PM, Carl Eastlund 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.

I feel we're getting perilously close to writing a paper about the essence of AOSD....


Regard a piece of code as a machine.  Not a specification of a machine, but the actual machine.

Now, tools like the stepper and typechecker need to be able to refer to "that part of the machine, right there." There are various ways of doing it, but what we've chosen to do (add a piece to the machine that's superfluous except when the machine is run using a particular mode or tool) has the advantage that it's robust. It doesn't necessarily break when other parts of the code around it change, and it's obvious to anyone modifying the code that you need to think about that annotation when you change the code.

I could imagine a tool that allowed such annotations to be automatically hidden, so that the underlying code is clearer, but I can't see a better way of "separating these concerns."

Am I missing something?

John

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4624 bytes
Desc: not available
URL: <http://lists.racket-lang.org/dev/archive/attachments/20110813/d6a9a842/attachment.p7s>