# [racket-dev] Overly general types for mutable containers

 From: Neil Toronto (neil.toronto at gmail.com) Date: Sun Jul 8 00:58:12 EDT 2012 Previous message: [racket-dev] math Next message: [racket-dev] Overly general types for mutable containers Messages sorted by: [date] [thread] [subject] [author]

```#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 ⊥
```

 Posted on the dev mailing list. Previous message: [racket-dev] math Next message: [racket-dev] Overly general types for mutable containers Messages sorted by: [date] [thread] [subject] [author]