[racket] Puzzled about type inference

In a sense, you put your finger on a sore spot of TR from R -- we are still figuring out how to help programmers along here. I rewrote your program like this: 

#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 (map #{vector->list @ NI} (cast '(#(1 2) #(3 4) #(5 6)) (Listof VNI))))
       (res (#{make-vector @ [Maybe NI]} (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)


I focused on what the type checker really needs -- hints on how to specialize those functions, and only those, that depend on your initial insight that the TC needs a hand with make-vector. Then I checked on the maps and realized that I need to help the TC along with the instantiations of vector->list (how can it know with context-free reasoning what kind of vector it is) and the same for car (how can it know what kind of list you're getting here). 

[[ Also, I don't know why this code looks like it does. There are alternative: 

#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))

(let* ((i0 (cast '(#(1 2) #(3 4) #(5 6)) [Listof VNI]))
       (idx+level (map #{vector->list @ NI} i0))
       (res (#{make-vector @ [Maybe NI]} (1+ (apply max (map #{car @ NI LNI} idx+level))) #f)))
  (for ((q : [Vectorof NI] (in-list i0)))
    (define i (vector-ref q 0))
    (define l (vector-ref q 1))
    (vector-set! res i l))
  res)


]]




On Aug 3, 2014, at 6:46 PM, Norman Gray wrote:

> 
> Greetings.
> 
> Short version: I repeatedly find myself adding TR type annotations by trial-and-error -- I'm sure I'm missing something.
> 
> I had a particularly acute case of this this afternoon.  I have a bit of typed/racket/base code as follows:
> 
> (: 1+ (Nonnegative-Integer -> Positive-Integer))
> (define (1+ n)
>  (+ n 1))
> 
> (define map1 #{map @ (Listof Nonnegative-Integer) (Vectorof Nonnegative-Integer)})
> (define map2 #{map @ Nonnegative-Integer (Listof Nonnegative-Integer)})
> (let* ((idx+level (map1 vector->list
>                        (cast '(#(1 2) #(3 4) #(5 6))
>                              (Listof (Vectorof Nonnegative-Integer)))))
>       (res (#{make-vector @ (U Nonnegative-Integer False)} (1+ (apply max (map2 car idx+level))) #f)))
>  (for-each (λ: ((p : (Listof Nonnegative-Integer)))
>              (let ((i (car p))
>                    (l (cadr p)))
>                (vector-set! res i l)))
>            idx+level)
>  res)
> 
> It doesn't much matter here what this does; but it typechecks and works OK.
> 
> What I'm puzzled by is the amount of explicit type information I had to add, in order to get it to typecheck, and I confess that I added that type annotation by simply going round and round the compile cycle in DrRacket, adding more and more until Racket stopped complaining.   Apart from anything else, the annotations end up making the code less readable than it might otherwise be.
> 
> I can pretty much see why I have to instantiate the make-vector explicitly (it'd probably be asking a bit much for Racket to look around and spot that the only thing called in the third argument of vector-set! is a Nonnegative-Integer), and I can sort-of see why I have to cast the '(#(1 2) ...) list [Racket identifies '(#(1 2) #(3 4) #(5 6)) as  (Listof (Vector Integer Integer)) which is more restricted than (Listof (Vectorof Real)), but less restricted than the actual (Listof (Vectorof Positive-Integer)) ].
> 
> But I can't really see why I have to spell out the instantiations of map1 and map2 (given the types of their arguments, I can unambiguously (?) deduce the type of the instantiation in both cases), and the type of the for-each argument, but I _don't_ have to spell out the type of idx+level.  And I have to spell out the maps , but not the car in (map2 car idx+level).
> 
> I can sort of see that type information propagates 'outwards', so that, for example, the type of map1 (specifically its domain) implies the type of idx+level, which the result of map1 is assigned to.  Analogously, because the type of p is known, then the corresponding car can be instantiated unambiguously.
> 
> However I don't have to instantiate vector->list, or the car argument to map2, so this appears to be type information propagating either 'inwards' from the type of map1/map2, or 'across' from the other argument.
> 
> Working through that, and looking at the simple case of 
> 
>    (map car (cast '((1 2) (3 4) (5 6)) (Listof (Listof Byte)))) ,
> 
> we have map's type as
> 
>    : (All (c a b ...)
>      (case->
>       (-> (-> a c) (Pairof a (Listof a)) (Pairof c (Listof c)))
>       (-> (-> a b ... b c) (Listof a) (Listof b) ... b (Listof c))))
> 
> Now, the type (Listof (Listof Byte)) fixes a in the first clause to be (Listof Byte), and thus, in the type of car
> 
>     : (All (a b) (case-> (-> (Pairof a b) a) (-> (Listof a) a))) ,
> 
> (Pairof a b) is (Listof Byte), meaning that a, here, must be Byte and thus the domain of car must be Byte, fixing c in the type of map.  So there appears to be no ambiguity, and while the algorithm for the general case would clearly be entertainingly challenging (am I correct that this was Sam's PhD work?), I'm not seeing a fundamental blocker.
> 
> In summary, I'm not saying anything's amiss here, but there are rather more 'sort-of's in the above account than I'm comfortable with.
> 
> So: (a) Am I doing something wrong, or writing unidiomatically?; and (b) is there a heuristic to guide me in what annotation I actually need to add and what can be inferred, so it's all a bit less trial-and-error?
> 
> All the best,
> 
> Norman
> 
> 
> -- 
> Norman Gray  :  http://nxg.me.uk
> SUPA School of Physics and Astronomy, University of Glasgow, UK
> 
> 
> ____________________
>  Racket Users list:
>  http://lists.racket-lang.org/users