On Aug 13, 2011 1:35 PM, "Carl Eastlund" <<a href="mailto:cce@ccs.neu.edu">cce@ccs.neu.edu</a>> wrote: > > On Sat, Aug 13, 2011 at 1:26 PM, Matthias Felleisen > <<a href="mailto:matthias@ccs.neu.edu">matthias@ccs.neu.edu</a>> wrote: > > > > On Aug 13, 2011, at 12:58 PM, Sam Tobin-Hochstadt wrote: > > > >> On Sat, Aug 13, 2011 at 12:51 PM, Eli Barzilay <<a href="mailto:eli@barzilay.org">eli@barzilay.org</a>> 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