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

On 01/02/2013 10:09 AM, Matthias Felleisen wrote:
> 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.

They'll experience performance problems only for `math/array' and 
`math/matrix'. Most everything else isn't higher-order.

>> 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...

I don't believe it, either, because it's obviously wrong. That's why the 
array library has hundreds of test cases.

The "like `array-axis-reduce'" part is missing from that sentence, 
probably because I wasn't very clear about what it means. Having had 
time to mull it over, I've decided I meant "combinators". When I get a 
combinator to pass the type checker, its implementation is usually correct.

The type of `unsafe-array-axis-reduce' is

   (All (A B) ((Array A) Index (Index (Index -> A) -> B) -> (Array B)))

(Haskell, in Racket. It's so beautiful. *sniff*)

Like most combinators, it's not obvious from the type what it means. But 
the type puts severe constraints on what can be done with the arguments. 
Usually, when I "fill in" the code around a type like this, there are 
only two options that pass the type checker, which also plausibly 
implement what I want. For this, I had a test case in mind:

   (unsafe-array-axis-reduce arr 0 build-list)

which reduced the two options to the correct one.

On the other hand, I've written monads in untyped Racket before. It... 
really kind of sucks without having about 5x more test cases than code. 
If you don't have them - and they can be hard to come up with, so it's 
easy to leave them out - getting it right is awful. It's really easy to 
have something you think works until you use some return/bind combo you 
didn't think of before, which blows up.

> 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.

I wonder if I could sum up by claiming that, with combinators, there's a 
great amount of overlap between typos and semantic errors.

The simplest example I can think of is the type (All (A) (A -> A)), 
which has only one correct implementation. Everything else is a typo.

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

This is my experience as well.

One place this bit me pretty early was getting TR to optimize loops over 
indexes *without using casts or assertions*. It's a puzzle, but it's 
solvable with a couple of templates. Here's one to loop over [0..n-1]:

   ensure n : Index ...
   (let: loop ([i : Nonnegative-Fixnum  0] args ...)
     (cond [(i . fx< . n)  compute ...
                           (loop (fx+ i 1) args ...)]
           [else  answer ...]))

The optimizer changes `fx<' into `unsafe-fx<' and `fx+' into 
`unsafe-fx+'. Also, (i . fx< . n) proves i : Index within "compute ...".

Here's a template to loop over [n-1..0]:

   ensure n : Index ...
   (let: loop ([i : Index  n] args ...)
     (cond [(i . fx= . 0)  answer ...]
           [else  (let ([i  (fx- i 1)])
                    compute ...
                    (loop i args ...))]))

The optimizer changes `fx=' and `fx-' to their unsafe counterparts. 
Also, (i . fx= . 0) proves i : Positive-Index in the `else' branch, so i 
: Index in "compute ...".

This should also work:

   (let: loop ([i : Index  n] args ...)
     (cond [(i . fx> . 0)  (let ([i  (fx- i 1)])
                             compute ...
                             (loop i))]
           [else  answer ...]))

Unfortunately, (i . fx> . 0) doesn't prove i : Positive-Index, even 
though it could.

This brings me to what I think is the major issue for us n00bs: the 
types force you to understand the numeric tower really well if you want 
to use types more precise than `Number'. Before you reach that level of 
understanding, though, and Typed Racket spits errors at you, it's hard 
to tell whether it has a legitimate complaint - especially when you 
don't know whether you should expect, say, (i . fx> . 0) to prove i : 
Positive-Index.

It would be really handy if TR could give counterexamples in these 
cases. "This is how you can end up with an exact zero by multiplying an 
exact rational and a flonum: (* 0 1.0)."

After you do understand the numeric tower well, you start looking for 
ways to prove to TR that your code won't explode at runtime. It's not 
always possible - again because, sometimes, the types aren't as precise 
as they could be. But sometimes because it's just hard.

One fine example is `sqrt'. Its types are sensible:

   > (sqrt (ann 5 Real))
   - : Number
   2.23606797749979

   > (sqrt (ann 5 Nonnegative-Real))
   - : Real [generalized from Nonnegative-Real]
   2.23606797749979

But it's often really hard to prove that something is nonnegative 
without an explicit cast, assertion, or test, and thus stay within the 
reals in expressions with roots.

Neil ⊥