On Aug 13, 2011 2:13 PM, "Eli Barzilay" <<a href="mailto:eli@barzilay.org">eli@barzilay.org</a>> wrote: > > Two minutes ago, Sam Tobin-Hochstadt wrote: > > 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. > > +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