[racket] Puzzled about type inference

Robby and Matthias, hello.

On 2014 Aug 6, at 02:23, Robby Findler <robby at eecs.northwestern.edu> wrote:

> Also because it is a decision that users a) have control over and b)
> may not guess TR's behavior correctly.

Very much (b).  The consequences of TR's behaviour are reported later (at type-check time) and elsewhere (in an inappropriate domain for another function), relative to the place where the user is typing.

There's also a little unpredictability which this would help with: '(1 2 3) is (Listof Positive-Byte), but #(1 2 3) is (Vector Integer Integer Integer).

Further, the user may reason with the types they _mean_ an expression to have, and so may have difficulty tracking down the cause of a bad type.  For example, because (in the example I mentioned) I intended a vector to be an index to indexes, incidentally with some missing values, I created (make-vector n #f) and _thought_ of it as (Vectorof Positive-Integer).  That preconception meant it took slightly longer than it might have done to track down my error (of course, it was still faster than waiting for the program to fail a unit test).

And finally -- a variant of Robby's point -- if a user puts in a type annotation and can see the effect ripple through the larger expression, that would surely very effectively build intuition about the behaviour of the type checker, and where it's best or necessary to help TC out.

All the best,

Norman


-- 
Norman Gray  :  http://nxg.me.uk
SUPA School of Physics and Astronomy, University of Glasgow, UK