#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
