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
____________________
Racket Users list:
http://lists.racket-lang.org/users
