[racket-dev] Five feature/limitation interactions conspire to drive mad

On Jan 1, 2013, at 7:42 PM, Neil Toronto wrote:

>> Question: did you start the math library in an untyped form (and switch) or did you go with types from the get-go?
> 
> It's all been in Typed Racket from the beginning. This was initially because I mostly had floating-point functions planned, and I wanted TR's help proving that I never used non-flonums by mistake. Also, I wanted the special functions to have performance competitive with C implementations.



I suspect I asked you the question before. Here is why I am asking. TR is still in its formative phase. So is the numerical type hierarchy, and so is OC. If you had developed in R first, we could have created 

 (1) a use-case story for TR 
 (2) measured how often you accidentally use an integer in library code and this 'pollute' the performance by accident 
 (3) measured how easily OC helps you with (2) 
 (4) measured the performance of 'best but not unsafe' R code 
 (5) converted from R to TR and measured improvement cmp to (4)

Step (5) is particularly interesting because none of our past R -> TR experiences was about number-intensive programs. As you may know, we claimed in PADL '12 that writing numeric code in R is like translating text book math into code. Question is whether this is true from an SE perspective. Even if it is, how much do you pay for this ease of SE; see (2) through (5). 

In OOPSLA '12 we claimed OC can help you a lot with finding (among others) numerical slow-downs where an R programmer accidentally pollutes numeric programs with ints and, worse, big nums. Again, it would have been wonderful to confirm the conjecture. 

BUT: I understand that this library isn't a small library and we already imposed on you and your 'vacation' time. So perhaps it would have been way too much effort to conduct an SE/performance experiment at the same time. 

I remain worried that R programmers will want to use math and array and matrix and friends and will experience performance problems when you have invested so much work in doing it right the first time. But we will see. 


;; ---



> 3. ... I can't speak for anyone else, but when I get something ... to pass the type checker, my code is usually correct.


I have heard this sentence often, in exactly this form. I have never believed it and I will share an anecdote here on this one. Some 10 years ago I was invited to teach at some European summer school on functional programming. I presented my first lecture early and I emphasized the design recipe, and our brand-new built-in support for testing. As the only untyped speaker (sounds like 'unwashed' when I write this here), I was heckled for testing my code. But you know me, I gave back what I got. That afternoon a speaker whose initials are P and W spoke about something typed and he wanted to imitate me with a life demo. He ran his code .. and got an exception. I couldn't help it but suggesting a test suite facility for this language; its name starts with H. 

I will freely acknowledge that type systems such as ML's, Haskell's, and ours eliminate typo-level mistakes immediately. I am deeply skeptical about the elimination of semantic bugs. That's not what these type systems are about. 




> 4. TR's types for Racket's numeric tower, especially the additional `Index' type, makes it easy to safely use unsafe indexing. Throughout `math/array', values of type `Index' are always either a size (e.g. a vector length) or an index that has been proved to be less than a size. IOW, if I can get TR to prove j : Index, I'm satisfied that (unsafe-vector-ref xs j) is actually safe. Also, if `j' is a loop counter, TR can usually compare and increment using unsafe fixnum ops.
> 
> There are a bunch of other little things that are like #4 (which is only a big thing because indexes are so prevalent in `math/array'). Maybe I'll collect those into a separate user story.


Interesting. My extremely limited experience -- and Shriram's -- suggests an eternal struggle with the numerical tower for 'beginners' like myself. 

Thanks -- Matthias