[racket] Typed Racket reactions on developing polymorphic typed array library, and questions

Vincent St-Amour wrote:
> At Sun, 22 Aug 2010 21:31:09 -0700,
> Neil Toronto wrote:
>> Vincent will be happy to know that all the flonum and fixnum ops are 
>> changed by TR's optimizer to be unsafe. (Except a certain add1 that TR 
>> can't prove doesn't overflow; I can prove it, so I changed it
>> myself.)
> 
> I am indeed happy. I'm pleasantly surprised about the fixnum part,
> since we can only optimize these in limited circumstances.

With the fixnums, it's mostly comparisons that are made unsafe. What I'm 
most pleased with is the fact that things like vector-length get changed 
to unsafe-vector-length, and that they return Nonnegative-Fixnums like 
they should. It seems every typed function I've used has the most 
liberal argument types and constrained return types they could have been 
given. Because of that, it's been quite easy to ensure that indexes 
remain fixnums, and that flonum ops return flonums.

It's fun to open the macro stepper and see "unsafe" scattered 
everywhere, in all the places I expect it. Pretty much every time it's 
not there is when I expect TR to be able to prove something it can't prove.

> Was simply adding types enough to trigger all these optimizations, or
> did you need to do a bit of extra work (except for that add1 case)?

Here's the list of extra work in the array library itself:

  - Abandon special handling of vector-backed arrays, which used 
polymorphic struct sub-types, in favor of loop syntax (Sam is looking 
into polymorphic struct sub-types)
  - Change (add1 i) into (unsafe-fx+ 1 i), prove it's safe
  - Handle type syntax in macros (no big deal)
  - Add extra checks to ensure that lexical indexes are fixnums in 
multidimensional arrays (e.g. ds : (Listof Fixnum) is only a valid array 
shape if (apply * ds) is a fixnum)
  - Replace match-define with multiple defines

For the last, IIRC, on my version of Racket, match-define calls a 
predicate to ensure the right struct type, but it's redundant in TR. 
Every little bit counts when it's in a tight loop. (FWIW, I like seeing 
all the unsafe struct refs as well.) I also recall TR reporting internal 
errors a few times when I used match or match-define, but I didn't file 
a bug report. I will next time.

I had to do the following in my tests and test app:

  - Use flsqrt, flfloor, flceiling instead of non-fl* versions
  - Use (* x x) instead of (sqr x)
  - Change literal numbers to literal floats (e.g. 1.0 instead of 1)

> However, you're right that the return type of a for/list: will always
> be a list, making the Listof redundant. This is even more true of
> for/fold:, and it annoys me too. In the case of for/fold:, it
> shouldn't be a problem since the types of the accumulators tell us all
> we need. I'll look into that.

Excellent, thanks.

>>   - I've found it useful to have a macro shaped like (with-refine* ([x 
>> pred?] ...) body ...). I have a lot of functions that take Integer and 
>> (Listof Integer) arguments, but actually operate only on 
>> Nonnegative-Fixnum indexes. (Nonnegativity and fixnum-ness are hard for 
>> TR to prove.) The function bodies are wrapped with this macro.
> 
> Having an assert* macro that would do something like that would be
> useful to have in the core. Could you send me your with-refine* macro
> so that I can include it in TR?

You'll want to rename it to with-asserts*, I suppose. I think if I were 
to spend more time on it, I'd make the type-name part optional, and in 
those cases use pred?'s syntax as a string as the second argument to 
raise-type-error.

Or maybe just leave it. Type errors should be friendly, yes? :)


#lang typed/racket

(require (for-syntax syntax/parse))

(define-syntax (with-refine* stx)
   (syntax-parse stx
     [(_ ([x:id pred? type-name] ...) body:expr ...+)
      (syntax/loc stx
        (cond [(not (pred? x))
               (raise-type-error 'with-refine* type-name x)]
              ...
              [else  (let () body ...)]))]))

(: fixnum-id (Number -> Fixnum))
(define (fixnum-id x)
   (with-refine* ([x fixnum? "Fixnum"])
     x))

(fixnum-id 1)
;; 1
(fixnum-id 0.0)
;; with-refine*: expected argument of type <Fixnum>; given 0.0


It would be nice if assert were capable of this. To do that, though, I 
think the type checker would have to treat the expression after the "if" 
in this case:

     (begin (if (pred? x)
                <something useful>
                (error ...))
            <some other useful thing...>)

as part of the "then" branch. (And as part of the "else" branch when the 
error is in the "then".)

Neil T