Typed Racket needs annotation to realize (Mutable-HashTable Symbol Symbol) is of a more general type

[Marc Kaufmann]

Hi,

in order to put some discipline on my code (and formalize to myself what I'm passing around), I started using typed racket. I have definitely hit my share of gotchas that make me scratch my head, but I kind of start to understand how things work and adding `(ann this-is ThatType)` annotations.

However, I have the following piece of code:

```

(: register-study-session! (-> Number Symbol Void))
(define (register-study-session! sid study-type)
  (unless (hash-has-key? (db-table 'studies) sid)
    (hash-set! (db-table 'studies)
               sid
               (make-hash (list (cons 'study-type study-type))))))
```

then I get the following error:

```

exploration.rkt:139:4: Type Checker: Polymorphic function `hash-set!' could not be applied to arguments:                                                                                                          
Argument 1:                                                                                                                                                                                                       
  Expected: (HashTable a b)                                                                                                                                                                                       
  Given:    DB                                                                                                                                                                                                    
Argument 2:                                                                                                                                                                                                       
  Expected: a                                                                                                                                                                                                     
  Given:    Number                                                                                                                                                                                                
Argument 3:                                                                                                                                                                                                       
  Expected: b                                                                                                                                                                                                     
  Given:    (Mutable-HashTable Symbol Symbol)     

```                                                                                                                                                               
 

The DB type is as follows:

```

(define-type DBKey (U Symbol Number))
(define-type DBValue (U Symbol Number Boolean Char))
(define-type DB (HashTable DBKey (U DB DBValue)))

```

However when I annotate this with an (ann ...) around the make-hash, it works:

```

(: register-study-session! (-> Number Symbol Void))
(define (register-study-session! sid study-type)
  (unless (hash-has-key? (db-table 'studies) sid)
    (hash-set! (db-table 'studies)
               sid
               (ann (make-hash (list (cons 'study-type study-type))) DB)))) ;; ONLY THIS LINE CHANGED
```                                       

I don't understand why this leads to it passing, since it said that it thought the DB earlier was a mutable hash of type Symbol to Symbol, which I would have thought is of type DB (which is any hashtable). So why does the type checker complain at first - or maybe why does it pass later?

Cheers,
Marc

[Sam Tobin-Hochstadt]

The problem is that the `DB` type is _not_ a super-type of
`(Mutable-HashTable Symbol Symbol)`, because mutable data structures
are two way communications channels. If you used an immutable hash,
that's a one-way communication and you would have the expected result.

However, the change you made fixed the problem because it changes the
type that `make-hash` picks to create the hash table. The argument to
`make-hash` has the type `(Listof (Pairof Symbol Symbol))` which _is_
a sub-type of `(Listof (Pairof DBKey (U DB DBValue)))`.

Sam

> --
> You received this message because you are subscribed to the Google Groups "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to racket-users...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/6b08ac58-5c85-45ad-9fb7-dd367254e015%40googlegroups.com.

[Marc Kaufmann]

I assumed it was something to do with mutability, but I don't understand what you mean when you say there is a two-way channel. The reference in typed racket (https://docs.racket-lang.org/ts-reference/type-ref.html#%28form._%28%28lib._typed-racket%2Fbase-env%2Fbase-types..rkt%29._.Hash.Table%29%29) says this:

```

(HashTable k v)

is the type of a mutable or immutable hash table with key type k and value type v.

Example:

> (make-hash '((a . 1) (b . 2)))

- : (HashTable Symbol Integer) [more precisely: (Mutable-HashTable Symbol Integer)]

'#hash((a . 1) (b . 2))

```

That suggests to me that HashTable includes both Mutatable-HashTable and Immutable-HashTable. The example given even states that the HashTable Symbol Integer is more precisely of Mutable-HashTable Symbol Integer type - does that *not* mean that (Mutable-HashTable Symbol Integer) is a subtype of (HashTable Symbol Integer) in the reference example?

I now tried to redefine DB as Mutable-HashTable to avoid this issue, but that doesn't work either. It still doesn't accept `(make-hash (list (cons 'study-type study-type)))` as something of type DB. How is (Mutable-HashTable Symbol Symbol) not a subtype of DB, which is (Mutable-HashTable DBKey (U DB DBValue)), and DBKey is (U Symbol ... ;other stuff) and same for DBValue?

You wrote that make-hash is of type `(Listof (Pairof Symbol Symbol))`. Is there a way to expand and print the type of something in terms of primitive types (well, or maybe step through one layer of abstraction) so that I could play around with some toy examples to get a sense of what types are returned? I am clearly confused by what type `make-hash` returns and what `hash-ref` expects.

Cheers,

Marc

[Alexis King]

The point Sam is making is about the variance of Mutable-HashTable specifically. Its relationship to the HashTable supertype is a red herring (which is why changing the type to Mutable-HashTable didn’t help).

Immutable data structures, like lists and immutable hash tables, are covariant in their type parameters. That means, for example,

a <: b => (List a) <: (List b)

where “=>” means “implies” and “<:” means “is a subtype of.” The intuitive justification for this is that “a <: b” means “a value of type a can always be used in place of a value of type b.” For example, a list of integers can always be given to a function that expects a list of numbers.

This is not true of mutable data structures. Imagine you have bindings with the following types:

v : (Vectorof Integer)
f : (-> (Vectorof Number) Void)

Is (f v) well-typed? The answer is no. The reason is that f’s implementation could very well be the following:

(define (f x)
(vector-set! x 0 0.5))

If (f v) were allowed, it would insert 0.5 into v, but v is supposed to only contain integers! (This is the “two-way communication channel” Sam was alluding to.) Therefore, (Vectorof Integer) cannot be a subtype of (Vectorof Number). We say Vectorof is *invariant* in its type parameter, since

(Vectorof a) <: (Vectorof b) iff a = b.

The same issue applies to mutable hashtables. If your DB type is defined to be (Mutable-HashTable (U Symbol Number) (U DB DBValue)), and you try to pass a value of type (Mutable-HashTable Symbol Integer), the typechecker rightly rejects your program, as Mutable-HashTable is invariant in its type parameters, so the two types must be precisely identical.

A solution to your problem is therefore to ensure the types really do match precisely. That is what the type annotation you wrote does: it forces the type to be identical to DB, overriding the type that was inferred. One might hope that TR’s type inference could be better here, but it’s a trickier case than it looks.

An aside: some typed languages support “bounded polymorphism” to give the programmer more fine-grained control over variance. For example, in Java, a function that accepts a Map can promise not to mutate it by giving the function a bounded type:

void f(Map<? extends Foo, ? extends Bar> m)

The question marks serve as “wildcards” that indicate f may be called with any Map<K, V> where K <: Foo and V <: Bar. It is a compile-time error for f to attempt to add new elements to m, but it is perfectly fine for it to access elements. However, I don’t believe Typed Racket supports any form of bounded quantification or bounded polymorphism at the time of this writing, so functions in Typed Racket that operate on mutable data structures are forced to be invariant.

Alexis

> To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/CAD7_NO4-cDE_3AHZ%3Dv9ieC%2BjYEvgXgWcQG_TGA0DqbmX%3DBH%3DYQ%40mail.gmail.com.

[Ben Greenman]

On 11/6/19, Marc Kaufmann <marc.ka...@gmail.com> wrote:
> I assumed it was something to do with mutability, but I don't understand
> what you mean when you say there is a two-way channel. The reference in
> typed racket (
> https://docs.racket-lang.org/ts-reference/type-ref.html#%28form._%28%28lib._typed-racket%2Fbase-env%2Fbase-types..rkt%29._.Hash.Table%29%29)
> says this:
>
> ```
>
> (HashTable

> <https://docs.racket-lang.org/ts-reference/type-ref.html#%28form._%28%28lib._typed-racket%2Fbase-env%2Fbase-types..rkt%29._.Hash.Table%29%29>

> k v)
>
> is the type of a mutable or immutable hash table

> <https://docs.racket-lang.org/reference/hashtables.html#%28tech._hash._table%29>

> with key type k and value type v.
> Example:
>
>> (make-hash

> <https://docs.racket-lang.org/reference/hashtables.html#%28def._%28%28quote._~23~25kernel%29._make-hash%29%29>

> '((a . 1) (b . 2)))
>
> - : (HashTable Symbol Integer) [more precisely: (Mutable-HashTable Symbol
> Integer)]
>
> '#hash((a . 1) (b . 2))
>
> ```
>
> That suggests to me that HashTable includes both Mutatable-HashTable and
> Immutable-HashTable. The example given even states that the HashTable
> Symbol Integer is more precisely of Mutable-HashTable Symbol Integer type -
> does that *not* mean that (Mutable-HashTable Symbol Integer) is a subtype
> of (HashTable Symbol Integer) in the reference example?

Right --- (Mutable-HashTable Symbol Integer) is a subtype of
(HashTable Symbol Integer).

> I now tried to redefine DB as Mutable-HashTable to avoid this issue, but
> that doesn't work either. It still doesn't accept `(make-hash (list (cons
> 'study-type study-type)))` as something of type DB. How is
> (Mutable-HashTable Symbol Symbol) not a subtype of DB, which is
> (Mutable-HashTable DBKey (U DB DBValue)), and DBKey is (U Symbol ... ;other
> stuff) and same for DBValue?

See Alexis's reply.

For a small example, (Mutable-HashTable Symbol Symbol) is NOT a
subtype of (Mutable-HashTable Symbol (U Symbol String))

```
#lang typed/racket/base

(define-type (M-HT A B) (Mutable-HashTable A B))

(define (f (x : (M-HT Symbol (U Symbol String))))
(void))

(define h : (M-HT Symbol Symbol)
(make-hash '((A . X))))

(f h) ;; type error
```

> You wrote that make-hash is of type `(Listof (Pairof Symbol Symbol))`. Is
> there a way to expand and print the type of something in terms of primitive
> types (well, or maybe step through one layer of abstraction) so that I
> could play around with some toy examples to get a sense of what types are
> returned? I am clearly confused by what type `make-hash` returns and what
> `hash-ref` expects.

The blue boxes in Dr. Racket might help. There are also a few tools
for looking at types in the REPL:

https://docs.racket-lang.org/ts-reference/Exploring_Types.html

[Marc Kaufmann]

Thanks Alexis, I now see why the subtyping doesn't work and why mutability is the issue. So when using mutable data structures, I really have to use the largest possible type everywhere or add annotations or similar - making types on immutable data more flexible. That's interesting.

Thanks for pointing out the REPL tools for looking at types Ben, I'll check those out.

I've now worked around having to put annotations everywhere by making some custom constructors with type signatures. That obviously requires direct annotations still, but at least my code isn't sprinkled with `(ann (make-hash ...) DB)` anymore, instead it has `(make-db ...)`.

Maybe I missed this (subtle, to me) point in the documentation, but somehow highlighting the issue of mutability and subtyping may be worth it. In https://docs.racket-lang.org/ts-guide/more.html, the docs mention the need to annotate mutable data, but this seems somewhat different from the "It's mutable, so you need to annotate", especially as the problem was lack of precision, rather than overly conservative type inference. I would suggest adding it as a point 5, or a variation of point 4, using Alexis' example with `(f v)` as to why it fails.

Cheers,

Marc