hash-ref in typed Racket

[Hendrik Boom]

In typed Racket I define a hashtable:

(: vector-to-contract (HashTable TType CContract))

(define vector-to-contract
(make-hash
(cast '(
(_bytes . bytes?)
(_s8vector . s8vector?)
(_u16vector . u16vector?)
(_s16vector . s16vector?)
(_u32vector . u32vector?)
(_s32vector . s32vector?)
(_u64vector . u64vector?)
(_s64vector . s64vector?)
(_f32vector . f32vector?)
(_f64vector . f64vector?))
(Listof (Pair TType CContract))
)
))

And then I try to look something up in it:

( hash-ref vector-to-contract (cast '_bytes TType) (cast 'other CContract))

and I am informed that I cannot, it seems, look up a value of type
TType in a hastable whose type indicates it looks up things of type
TType:

Type Checker: Polymorphic function `hash-ref' could not be applied to arguments:
Types: HashTableTop a (-> c) -> Any
HashTableTop a False -> Any
HashTableTop a -> Any
Arguments: (HashTable TType CContract) TType CContract
Expected result: AnyValues
in: (hash-ref vector-to-contract (cast (quote _bytes) TType) (cast
(quote other) CContract))


How *does* one use hashtables in typed Racket?

-- hendrik

[Sam Tobin-Hochstadt]

The problem here is with the optional third argument to `hash-ref`.
Typed Racket only allows `#f` or functions as the third argument.
Plain Racket allows any non-function value as a default, or a function
which is called to produce the default. Since "any non-function" is
not expressible in Typed Racket, it's more restricted here.

The best option is to wrap the third argument in a thunk: `(lambda () 'other)`.

As an aside, you probably don't want to use `cast` this extensively in
your program.

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/20200421143453.lauuqi3pb4fdgyhh%40topoi.pooq.com.

[Hendrik Boom]

On Tue, Apr 21, 2020 at 10:50:44AM -0400, Sam Tobin-Hochstadt wrote:
> The problem here is with the optional third argument to `hash-ref`.
> Typed Racket only allows `#f` or functions as the third argument.
> Plain Racket allows any non-function value as a default, or a function
> which is called to produce the default. Since "any non-function" is
> not expressible in Typed Racket, it's more restricted here.

I missed that. Thanks.

>
> The best option is to wrap the third argument in a thunk: `(lambda () 'other)`.
>
> As an aside, you probably don't want to use `cast` this extensively in
> your program.

No, I don't. I hoped it would help, but I was fixing the wrong problem,
so it didn't .

-- hendrik

> To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/CAK%3DHD%2BY-pc3Jfg4RgRmAPMqSUxUj8rJsm3np2eq2%2B-J5PWTO4Q%40mail.gmail.com.

[Tim Jervis]

For the type of the third argument, rather than "any non-function", could Typed Racket use the type of the values in the hash?

[Sam Tobin-Hochstadt]

Unfortunately, that doesn't work -- the values in the hash could
include functions.

Sam

> To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/aacb7226-8a0e-4fe0-9481-c1f72143eec2n%40googlegroups.com.

[Tim Jervis]

Wouldn’t that possibility then have to be part of the type for the values in the hash? Maybe I don’t understand how types work for hashes.

In this code:

#lang typed/racket

(define h : (Immutable-HashTable Integer (-> String))

  (make-immutable-hash))

(hash-ref h

          2

          (thunk "Hit and miss"))

I think I’ve set the type of the values of the hash h to be a thunk that returns a string. I’m then trying to access a key in that hash, which misses because the hash has no keys. The third argument works because it’s a function that happens to return a string. It’s funny because it looks like it type-checks, but it doesn’t really.

This code:

#lang typed/racket

(define h : (Immutable-HashTable Integer String)

  (make-immutable-hash))

(hash-ref h

          2

          (thunk "Hit and miss"))

also type-checks because even though the third argument to hash-ref is not a String, it is a function.

Oddly, to me at least,

#lang typed/racket

(define h : (Immutable-HashTable Integer String)

  (make-immutable-hash))

(hash-ref h

          2

          "Hit and miss")

Does not type check even though the type of the hash’s values is String, the same as the third argument of hash-ref.

[Tim Jervis]

For the record, this seems to work fine:

#lang typed/racket

(require/typed racket

  [hash-ref ((Immutable-HashTable Symbol 

  (U (-> String)

                                     String))

             Symbol

             (U String

                (-> String))

             ->

             (U String

                (-> String)))])

(let* ([h : (Immutable-HashTable Symbol 

 (U (-> String)

                                    String))

          (make-immutable-hash)]

       [h (hash-set h

                    'function

                    (thunk "Function value"))]

       [h (hash-set h

                    'string

                    "String value")])

  (printf "Fixed string on error:\n")

  (for ([key (in-list '(function string missing))])

    (printf "key: ~a\tvalue: ~a\n"

            key

            (hash-ref h

                      key

                      "Missed!")))

  (printf "\n")

  (printf "Thunk on error:\n")

  (for ([key (in-list '(function string missing))])

    (printf "key: ~a\tvalue: ~a\n"

            key

            (hash-ref h

                      key

                      (thunk "Missed!")))))

>

Fixed string on error:

key: function value: #<procedure:...

key: string value: String value

key: missing value: Missed!

Thunk on error:

key: function value: #<procedure:...

key: string value: String value

key: missing value: Missed!

but this attempt to generalise fails:

#lang typed/racket

(require/typed racket

  [hash-ref (All (K V)

                 (Immutable-HashTable K V)

                 K

                 V

                 ->

                 V)])

(let* ([h : (Immutable-HashTable Symbol

                                 (U (-> String)

                                    String))

          (make-immutable-hash)]

       [h (hash-set h

                    'function

                    (thunk "Function value"))]

       [h (hash-set h

                    'string

                    "String value")])

  (printf "Fixed string on error:\n")

  (for ([key (in-list '(function string missing))])

    (printf "key: ~a\tvalue: ~a\n"

            key

            (hash-ref h

                      key

                      "Missed!")))

  (printf "\n")

  (printf "Thunk on error:\n")

  (for ([key (in-list '(function string missing))])

    (printf "key: ~a\tvalue: ~a\n"

            key

            (hash-ref h

                      key

                      (thunk "Missed!")))))

>

; hash/c: contract violation

;   expected: chaperone-contract?

;   given: K4

[Sam Tobin-Hochstadt]

That particular pattern, with `(U String (-> String))`, will work, but
your generalized version would be wrong if it worked. Consider:

```
(: unsound : (Immutable-HashTable Symbol (-> String)) -> String)
(define (unsound h)
((hash-ref h (gensym) (lambda () "x"))))

(unsound (hash))
```

This program type checks with your second `require/typed` of
`hash-ref`, but it's wrong. We can see that by using
`unsafe-require/typed`, and we get an error because we can't apply
"x".

Furthermore, you can't generalize to (U T (-> T) either, because if T
is (-> String) then you get the same problem.

Sam

> To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/2F152CB5-E6E3-4C8F-B11F-0477DF2DD965%40gmail.com.