FWIW, I agree with Robby and have had similar conversations with Sam in person. (Although for me it is that I wish I had the ability to claim that macro pieces had certain types regardless of what TR could infer from the generated code.)
I think a big part of the Racket philosophy is that the programming language implementer is not a member of an elite, enlightened caste that can make choices mere mortals cannot. This philosophy is the root of what I find beautiful about macros, continuations, first-class synchronization, and structure type properties, for example. Although I am not directly writing anything for the TR implementation, I have opinions about the goal of that project. To me, it is not "figure out a type system that is passable for Racket programs" but "make a type system that is to existing type systems as Racket is to pedestrian languages" ---- in particularly, by allowing more extensions (type or otherwise) to be done in language. I see Robby's point about contract / type isomorphism and mine about more powerful type macros as steps in that direction. <3 Jay On Tue, Jun 26, 2012 at 10:10 PM, Robby Findler <ro...@eecs.northwestern.edu> wrote: > Consider me done! > > Robby > > On Tue, Jun 26, 2012 at 11:05 PM, Neil Toronto <neil.toro...@gmail.com> wrote: >> I haven't got a clue what you two are arguing about anymore. If you both >> stop, maybe Sam can implement that perfectly safe change to the typed -> >> untyped contract barrier that he said he could do. That would be nice. >> >> ;) >> >> Neil ⊥ >> >> >> On 06/26/2012 09:23 PM, Robby Findler wrote: >>> >>> On Tue, Jun 26, 2012 at 10:08 PM, Sam Tobin-Hochstadt<sa...@ccs.neu.edu> >>> wrote: >>>> >>>> On Tue, Jun 26, 2012 at 10:44 PM, Robby Findler >>>> <ro...@eecs.northwestern.edu> wrote: >>>>> >>>>> On Tue, Jun 26, 2012 at 9:25 PM, Sam Tobin-Hochstadt<sa...@ccs.neu.edu> >>>>> wrote: >>>>>> >>>>>> On Tue, Jun 26, 2012 at 9:29 PM, Robby Findler >>>>>> <ro...@eecs.northwestern.edu> wrote: >>>>>>> >>>>>>> This sounds like a terrible solution. >>>>>>> >>>>>>> There are lots of places in our system where we just declare facts and >>>>>>> don't prove them and then use them for lots of things (often >>>>>>> optimizations). Why should this one be special? >>>>>> >>>>>> >>>>>> I don't know of any places like this in Racket. What are you thinking >>>>>> of? >>>>> >>>>> >>>>> The inliner and the JIT compiler and that whole interaction are the >>>>> ones I thought of. I should have said "lots of facts" not "lots of >>>>> places", tho. Sorry about that. >>>> >>>> >>>> I'm still not sure what you're thinking of. What operation does the >>>> inliner or JIT perform that is justified by a >>>> programmer-declared-but-not-checked fact? >>> >>> >>> There are many operations that are implemented partially in JIT and >>> wholly in the runtime system. The JIT generated version gets used >>> unless certain conditions hold, in which case the runtime system >>> version gets used. The programmer declared fact is embedded into the >>> code and not specified as a fact per se, but for example, there is one >>> such fact saying "this pile of assembly instructions is equivalent to >>> the C implementation of list-ref, under the condition that the number >>> argument is a fixnum less than 10,000 and we don't run out of pairs >>> too soon" (roughly). There are large pile of such things. Another one >>> you're probably more familiar with: "this pile of assembly >>> instructions is equivalent to + when the arguments are both fixnums or >>> both flonums". >>> >>> There is another pile of such invariants in the (pre-bytecode level) >>> inliner. It relies on beta substitution and the ability to run certain >>> primitives at compile time. (I don't know as much about that one, so >>> probably there are more things it relies on than that.) >>> >>>>>> Certainly, Typed Racket is intended to be sound in the same sense that >>>>>> Racket is safe, and that Haskell, OCaml, and Java are safe as well: if >>>>>> you don't use specifically-marked unsafe features (such as the FFI and >>>>>> `racket/unsafe/ops`), then you get a guarantee that depends only on >>>>>> the correctness of the runtime system/compiler, not on the correctness >>>>>> of any user code. >>>>> >>>>> >>>>> Of course I understand this. I'm pointing out that this is not a >>>>> significant guarantee, in and of itself (see last para below for an >>>>> elaboration here). >>>>> >>>>>> I think this a very important guarantee: we've seen >>>>>> far too often that trusting user code in languages like C and C++ was >>>>>> a big mistake in many contexts. >>>>> >>>>> >>>>> I don't think this is an either/or. Indeed, just to continue with C: >>>>> if everyone understood that the types were really just size markers >>>>> and nothing else, then lots of the seeming unsoundness goes away in C >>>>> (not all, of course, and as I've been learning from Regehr's blog, >>>>> there are lots of other dark corners). But no one is suggesting we >>>>> remove checks from array bounds, which is what really cost society >>>>> money wrt to C and, IMO, the kind of invariant that matters. >>>> >>>> >>>> I don't think the distinction that you're trying to draw here is >>>> meaningful. In particular, to return to our earlier example, if you >>>> assert the type Neil gave for an untyped value, backed up with the >>>> contract `(-> real? real?)`, then Typed Racket's type system can be >>>> off by arbitrarily much -- no claim it makes can be trusted. >>> >>> >>> I think you're making this out to be a boogey man, when it really isn't. >>> >>> But why doesn't your argument apply to any program that uses the FFI? >>> It also invalidates all of the guarantees that TR makes. (And there >>> are essentially no programs that don't use the FFI anymore.) >>> >>> And anyways, I think that TR actually makes *no* guarantees in a >>> precise technical sense. Even if I accept the proofs about the models >>> in your papers then (as I said earlier) we are not running your >>> models. Why should you be the only allowed to introduce these >>> particular bugs? I'm allowed to introduce other bugs, for example. >>> >>>> Further, >>>> the optimizer will happily transform your program from one that >>>> behaves one way to a different program, and cause the entire Racket >>>> runtime to segfault. So if we went the route that you're suggesting, >>>> Typed Racket might serve the "what invariants should I help >>>> programmers that read my code be aware of?" role, but we'd have to >>>> take out the optimizer, and the claims that if Typed Racket tells you >>>> something, then you know it to be true (modulo the extensive caveats >>>> about bugs in TR, Racket, GCC, Linux, Intel, etc). I don't think >>>> that's the right trade to make. >>> >>> >>> (I don't really get what you're saying here at all, but I also think >>> it isn't really an argument against my argument.) >>> >>> But I'll note that you forgot perl in your list. I'm sure it is used >>> in the build process of one of those tools that we rely on. >>> >>> Everything is hopeless. >>> >>> Robby >>> >>> _________________________ >>> Racket Developers list: >>> http://lists.racket-lang.org/dev >> >> >> _________________________ >> Racket Developers list: >> http://lists.racket-lang.org/dev > > _________________________ > Racket Developers list: > http://lists.racket-lang.org/dev -- Jay McCarthy <j...@cs.byu.edu> Assistant Professor / Brigham Young University http://faculty.cs.byu.edu/~jay "The glory of God is Intelligence" - D&C 93 _________________________ Racket Developers list: http://lists.racket-lang.org/dev