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
