#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 ⊥
_________________________
Racket Developers list:
http://lists.racket-lang.org/dev
