[racket] Typed Racket generalization and inference for containers

On Sun, Apr 7, 2013 at 10:18 AM, Andrey Larionov <anlarionov at gmail.com> wrote:
> Hello, Racket community.
> I'm a newbie and just started study Racket and Typed Racket and a little
> confused with generalization and inference.
> I found what inference works different for different containers type. For
> example:
> Set:
>> (set 0 195 196)
> - : (Setof Byte)
> (set 0 195 196)
> List:
>> '((195 . 1) (196 . 2))
> - : (Listof (Pairof Positive-Byte Positive-Byte)) [generalized from (List
> (Pairof Positive-Byte One) (Pairof Positive-Byte Positive-Byte))]
> '((195 . 1) (196 . 2))
> HashTable:
>> #hash((195 . 1) (196 . 2) (197 . 3))
> - : (HashTable Integer Integer)
> '#hash((195 . 1) (197 . 3) (196 . 2))

This is because sets and lists are immutable, while hash tables are
(potentially) mutable.  Typed Racket generates more general types for
mutable data because otherwise the lack of subtyping would make such
data very hard to use.

In fact, this hash table is immutable, but Typed Racket doesn't
distinguish between mutable and immutable hash tables.  If it did,
then you'd get the result you'd expect here.

> Actually i'm writing library for msgpack protocol and decide to implement it
> in Typed Racket. Here is my code which did't type check and broke all other
> program:
> (define-type Atom (U False True Null))
> (: atoms (HashTable Byte Atom))
> (define atoms #hash((#xc0 . ())
>                     (#xc3 . #t)
>                     (#xc2 . #f)))
> Error: Type Checker: Expected (HashTable Byte Atom), but got (HashTable
> Integer Atom) in: #hash((195 . #t) (194 . #f) (192 . ()))

This is a bug. You may be able to work around it by using the `hash`
function, instead of the literal data constructor.

Sam