[racket-dev] Overly general types for mutable containers

#lang typed/racket

(define: x : Index 1)

(: bar ((Vectorof Index) -> (Vectorof Index)))
(define (bar xs) xs)

(: foo (All (A) ((Vectorof Index) -> (Vectorof Index))))
(define (foo xs) xs)


So we have an Index `x' and a couple of identity functions `bar' and 
`foo' that only differ by the fact that `foo' is polymorphic.

In the REPL:

 > (vector x)
- : (Vector Integer)
'#(1)


So we get a general type. I guess it's so "literals" like `(vector 0 1 0 
1)' don't get overly-specific types like `(Vector Zero One Zero One)', 
for which non-trivial mutation would fail to typecheck. I respect that, 
but I have a problem with it: it's been surprising me too much.

Here's a surprise that took 20 minutes to figure out:

 > (bar (vector x))
- : (Vectorof Index)
'#(1)
 > (define xs (vector x))
 > (bar xs)
Type Checker: Expected (Vectorof Index), but got (Vector Integer) in: xs


I finally decided that there must be a special rule for applying 
functions like `bar' directly to `(vector x ...)', since the vector is 
never referred to except as a (Vectorof Index). Okay, that's one fewer 
circumstance in which `(vector x)' won't get an overly general type.

One reason it took so long to figure out that special rule was this 
surprise, and the fact that I was working on a non-toy program and had 
to reduce the problem to this:

 > (foo (vector x))
Type Checker: Polymorphic function foo could not be applied to arguments:
Argument 1:
   Expected: (Vectorof Index)
   Given:    (Vector Integer)
  in: (foo (vector x))


Remember that `foo' only differs from `bar' in that it's polymorphic, 
parameterized on a type `A' that it doesn't use. So that's one 
circumstance in which `(vector x)' gets an overly general type.

Here's another reason it took a while to figure all this out:

 > ((inst vector Index) x)
- : (Vector Integer)
'#(1)


I expect Sam to declare that that's the bug, and possibly also the fact 
that `(foo (vector x))' doesn't type. But really, I think generalizing 
the container's types is the bug. It runs directly counter to what I 
expect from immutable containers, which I use most of the time:

 > (list x)
- : (Listof Index) [generalized from (List Index)]
'(1)
 > (list 0 1)
- : (Listof (U Zero One)) [generalized from (List Zero One)]
'(0 1)


Honestly, I'd rather have to write `((inst vector Integer) 0 1 0 1)' or 
`(ann #(0 1 0 1) (Vectorof Index))' when I create "literal" vectors.

Neil ⊥