[racket-dev] Wrapping loops for TR isn't working, and the type annotations are for the wrong value

I like the idea of wrapping Racket's standard "for" loops with a few 
annotations and letting inference figure out the rest of the types.

The problem is, it doesn't work very well.

  1. Even though the loop's type is technically optional, it seems to 
always be required.

  2. Many simple loops don't typecheck anyway.

  3. It's a PITA to write new kinds of "for" loops in the same style.

  4. A #:when clause can only be last.

#4 is acknowledged in the TR reference.

As an example of #1, the following is one of the simplest loops:

   ;; "Type Checker: ... add more type annotations"
   ;(for/list: ([i  (in-range 5)]) i)

   ;; This works:
   (for/list: : (Listof Integer) ([i  (in-range 5)]) i)

Besides being annoying, it's obviously redundant.

For examples of #2, these don't typecheck:

   (for/vector: : (Vectorof Integer) ([i  (in-range 5)]) i)

   (for*/list: : (Listof Integer) ([i  (in-range 5)]
                                   [j  (in-range 2)])
     i)

An example of #3 is the `for/array:' I tried to write. Gah! If your data 
type isn't inductive with a polymorphic null value (which arrays aren't) 
or convertible from something that already has a "for" loop, Abandon All 
Hope.

Even if your spanky new data type *is* convertible from something that 
has a "for" loop, the requirement to specify the type of the *entire 
result* makes annotating the expanded loops really awkward. If a user writes

   (for/array: : (Array Symbol) ...)

and I want to construct it by converting a vector, the `for/array:' loop 
has to expand to (pretending for a moment that this works):

   (for/vector: : (Vectorof Symbol) ...)

I can parse (Array Symbol) to get the element type, but what if the user 
defines the type alias (define-type Symbol-Array (Array Symbol))?

Here's the proposal: deprecate the result annotations and use body 
annotations instead. Examples:

   (for/vector: ([i  (in-range 5)]) : Integer
     i)

   (for/array: ([i  (in-range 5)]) : Integer
     i)

The latter could easily expand to a small wrapper around the former.

Some typed "for" loops would have to be reimplemented, unless inference 
improves a lot. To make this easier, I've attached an example 
implementation of `for/vector:' and `for*/vector:'. It allows both body 
and result annotations, handles #:length properly, allows #:when clauses 
anywhere, and fixes the two bugs in `for/vector' I reported today.

Neil ⊥
-------------- next part --------------
#lang typed/racket/base

(require racket/vector
         (for-syntax racket/base syntax/parse)
         racket/unsafe/ops)

(define-syntax (ann: stx)
  (syntax-case stx ()
    [(_ v)  (syntax/loc stx v)]
    [(_ v t)  (syntax/loc stx (ann v t))]))

(define-syntax (inst: stx)
  (syntax-case stx ()
    [(_ v)  (syntax/loc stx v)]
    [(_ v t)  (syntax/loc stx (inst v t))]))

(define-for-syntax (base-for/vector: stx for: for/list:)
  (syntax-parse stx #:literals (:)
    [(name (~optional (~seq : T))
           #:length n-expr:expr
           (clauses ...)
           (~optional (~seq : A))
           body ...+)
     (with-syntax ([maybe-T  (if (attribute T) #'(T) #'())]
                   [maybe-A  (if (attribute A) #'(A) #'())])
       (quasisyntax/loc stx
         (let: ([n : Integer  n-expr])
           (cond [(index? n)
                  (define vs (ann: ((inst: vector . maybe-A)) . maybe-T))
                  (let/ec: break : Void
                    (define: i : Nonnegative-Fixnum 0)
                    (#,for: (clauses ...)
                            (define v (ann: (let () body ...) . maybe-A))
                            (cond [(= i 0)
                                   (define new-vs (ann: ((inst: make-vector . maybe-A) n v)
                                                        . maybe-T))
                                   (set! vs new-vs)]
                                  [else
                                   (unsafe-vector-set! vs i v)])
                            (set! i (unsafe-fx+ i 1))
                            (when (i . >= . n) (break (void)))))
                  (unless (= (vector-length vs) n)
                    ;; Only happens when n > 0 and vs = (vector)
                    (error 'name "expected ~e elements; produced ~e" n (vector-length vs)))
                  vs]
                 [else  (raise-type-error 'name "Index" n)]))))]
    [(_ (~optional (~seq : T))
        (clauses ...)
        (~optional (~seq : A))
        body ...+)
     (with-syntax ([maybe-T  (if (attribute T) #'(T) #'())]
                   [maybe-A  (if (attribute A) #'(A) #'())])
       (quasisyntax/loc stx
         (let ()
           (define vs (ann: ((inst: vector . maybe-A)) . maybe-T))
           (define: n : Nonnegative-Fixnum 0)
           (define: i : Nonnegative-Fixnum 0)
           (#,for: (clauses ...)
                   (define v (ann: (let () body ...) . maybe-A))
                   (cond [(= i n)  (define new-n (max 4 (unsafe-fx* 2 n)))
                                   (define new-vs (ann: ((inst: make-vector . maybe-A) new-n v)
                                                        . maybe-T))
                                   (vector-copy! new-vs 0 vs)
                                   (set! vs new-vs)
                                   (set! n new-n)]
                         [else  (unsafe-vector-set! vs i v)])
                   (set! i (unsafe-fx+ i 1)))
           (vector-copy vs 0 i))))]))

(define-syntax (for/vector: stx)
  (base-for/vector: stx #'for: #'for/list:))

(define-syntax (for*/vector: stx)
  (base-for/vector: stx #'for*: #'for*/list:))

;; The proposed syntax:
(for/vector: ([i  (in-range 5)]) : Integer
  i)

;; The old way, just for kicks:
(for/vector: : (Vectorof Integer) ([i  (in-range 5)])
  i)

;; Allow both ways?
(for/vector: : (Vectorof Integer) ([i  (in-range 5)]) : Integer
  i)

(for/vector: ([x  (in-range 5)]
              #:when (x . > . 1)
              [y  (in-range 5)]
              #:when (y . >= . x)
              ) : (Pair Integer Integer)
  (cons x y))

(for*/vector: ([x  (in-range 5)]
               [y  (in-range 2)]) : (Pair Integer Integer)
  (cons x y))