[racket-dev] math collection [was: Hyperbolic functions]

I found your message strange and I contemplated whether I should reply on 'dev' at all. 

In the interest of sharing and evolving the Racket idea, I am going with a response on 'dev'. Your central claim is that "the programming language implementer is not a member of an elite, enlightened caste that can make choices mere mortals cannot." Without any constraint this claim is plain wrong (like many general claims). You simply do not want every programmer to plug code into the JIT easily. You do not want #%plaiin-module-begin change meaning on you. You do not want to specify types so that the compiler randomly mangles bits for you and claims that they are the result. You can see that this is wrong with all the security that Matthew carefully adds to the implementation (not to speak of the design idea, which is abstract anyway). If we didn't want to restrict access to certain pieces in certain ways, why bother with inspectors and armed syntax and generative structs for basic forms. Why not allow (closure-environment (lambda (x) x)) to expose the pointer to the environment? (Which you can do in MIT Scheme, though there is called cadr.) 

I think the closest we have come to your claim is that 

 we wish to push back the boundaries without giving up safety and security. 

Finding this middle ground of a high degree of expressivity with good constraints imposed on it is the purpose Racket and PLT. And we have done really well with it for a long time 

-- Matthias








On Jun 27, 2012, at 2:12 PM, Jay McCarthy wrote:

> 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
> <robby at eecs.northwestern.edu> wrote:
>> Consider me done!
>> 
>> Robby
>> 
>> On Tue, Jun 26, 2012 at 11:05 PM, Neil Toronto <neil.toronto at 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<samth at ccs.neu.edu>
>>>>  wrote:
>>>>> 
>>>>> On Tue, Jun 26, 2012 at 10:44 PM, Robby Findler
>>>>> <robby at eecs.northwestern.edu>  wrote:
>>>>>> 
>>>>>> On Tue, Jun 26, 2012 at 9:25 PM, Sam Tobin-Hochstadt<samth at ccs.neu.edu>
>>>>>>  wrote:
>>>>>>> 
>>>>>>> On Tue, Jun 26, 2012 at 9:29 PM, Robby Findler
>>>>>>> <robby at 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 <jay at 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