On Sat, Aug 13, 2011 at 1:26 PM, Matthias Felleisen <matth...@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 <e...@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. --Carl _________________________________________________ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/dev
