[racket] Puzzled about type inference

Here's how I would annotate the original program, using Matthias' type
definitions:

```
#lang typed/racket

(: 1+ (Nonnegative-Integer -> Positive-Integer))
(define (1+ n)
  (+ n 1))

;; entirely unnecessary but helped me read; IGNORE
(define-type (Maybe α) (U False α))
(define-type NI Nonnegative-Integer)
(define-type LNI (Listof NI))
(define-type VNI (Vectorof NI))

(let* ((idx+level : (Listof LNI)
                  (map #{vector->list @ NI}
                       (ann '(#(1 2) #(3 4) #(5 6)) (Listof VNI))))
       (res : (Vectorof (Maybe NI))
            (make-vector (1+ (apply
                              max (map #{car @ NI LNI}
                                       idx+level)))
                         #f)))
  (for-each (λ ((p : LNI))
              (let ((i (car p))
                    (l (cadr p)))
                (vector-set! res i l)))
            idx+level)
  res)

;; expect
'#(#f 2 #f 4 #f 6)
```

The most signficant differences are (1) I'm not using `cast`, which
should be avoided when possible. `cast` is a runtime operation, and
might be hiding arbitrary bugs. (2) I've annotated the `let`-bound
variables, which makes life easier on the rest of the type checker and
helps improve error messages.

There are a few things that make this program require more annotations
than I'd like.

1. TR doesn't handle automatically inferring type arguments when
polymorphic functions (like `map`) are given polymorphic arguments
like `vector->list`. While fixing this would require work, it just
needs to be done -- there's no reason we shouldn't be able to make
this work.
2. Inference doesn't allow TR to figure out that it should use
Nonnegative-Integer for the contents of the vectors, and so it falls
back on guessing that it should type them as integers. If Typed Racket
knew about immutable vectors, then we could do better here, similarly
if inference worked better.

Sam


On Sun, Aug 3, 2014 at 8:12 PM, Matthias Felleisen <matthias at ccs.neu.edu> wrote:
>
> After some reflection, here is how I think you should proceed:
>
> #lang typed/racket
>
> (: 1+ (Nonnegative-Integer -> Positive-Integer))
> (define (1+ n)
>   (+ n 1))
>
> ;; entirely unnecessary but helped me read
> (define-type (Maybe α) (U False α))
> (define-type NI Nonnegative-Integer)
> (define-type LNI (Listof NI))
> (define-type VNI (Vectorof NI))
> (define-type LVNI (Listof VNI))
>
> (let* ((given  : LVNI '(#(1 2) #(3 4) #(5 6)))
>        (length : NI   (1+ (apply max (map (lambda ({x : VNI}) (vector-ref x 0)) given))))
>        (result : [Vectorof [Maybe NI]] (make-vector length #f)))
>   (for ((q : VNI (in-list given)))
>     (vector-set! result (vector-ref q 0) (vector-ref q 1)))
>   result)
>
>
> The above -- minus types -- is how I would probably write the code in Racket, following the style guide. (I would use three defines instead of let* but let's ignore this point.) I would use
>  -- given as a parameter (I am guessing here)
>  -- length to tell the reader that this is the new length of the vector
>  -- result to spell out what this vector is about
>
> The for-loop would use a single line because it is short and brings across the idea.
>
> If I were to move this code to Typed Racket, I'd add a type declaration to each identifier just like in any other (explicitly, statically) typed programming language. That's what I did, and there was no problem checking and running your code.
>
> -- Matthias
>
>
> ____________________
>   Racket Users list:
>   http://lists.racket-lang.org/users