This is an intentional design choice, but I also think it's pretty
hard to avoid. In particular, consider immutable hash tables. In that
case, (HT A B) is a subtype of (HT A* B), if A <: A*. But then for
immutable hash tables, your `checked-hash-ref` has the same issue that
the original type for `hash-ref` has, because we can just instantiate
A to the bigger type. In general, if you take out the `HashTableTop`
lines, you probably won't get a different behavior in the cases you're
thinking of, and those cases are important for cases where you
genuinely only know that you have a hash, and not something about the
key/value types.
Sam
On Thu, Jan 11, 2018 at 12:35 PM, 'John Clements' via Racket Users
<racket-users@googlegroups.com> wrote:
> I was surprised and a wee bit dismayed this morning to see that this code,
> using hash-ref with the wrong key type, typechecks:
>
> #lang typed/racket
>
> (define my-hash : (HashTable String String)
> (make-immutable-hash
> '(("abc" . "def")
> ("ghi" . "jkl"))))
>
> (hash-ref my-hash 1234)
>
> So, I printed out the type of hash-ref:
>
> (All (a b c)
> (case->
> (-> (U (Immutable-HashTable a b)
> (Mutable-HashTable a b)
> (Weak-HashTable a b))
> a
> b)
> (-> (U (Immutable-HashTable a b)
> (Mutable-HashTable a b)
> (Weak-HashTable a b))
> a
> False
> (U False b))
> (-> (U (Immutable-HashTable a b)
> (Mutable-HashTable a b)
> (Weak-HashTable a b))
> a
> (-> c)
> (U b c))
> (->* (HashTableTop a) (False) Any)
> (-> HashTableTop a (-> c) Any)))
>
>
> Sure enough, hash-ref on a key outside the domain of the hash table is
> totally legal, and returns type Any. And why not? This is clearly sound.
>
> HOWEVER, as a TR programmer, I can’t imagine a lot of situations in which I’d
> prefer this behavior to simply having this be a type error; I know that TR’s
> philosophy is to try to support gradual typing, but if I want this check,
> I…have to roll my own hash-ref? It’s not hard, I guess:
>
> (: checked-hash-ref (All (A B) ((HashTable A B) A -> B)))
> (define (checked-hash-ref table key)
> (hash-ref table key))
>
>
> … but I just wanted to check and make sure this was a deliberate choice.
> Maybe I’m missing an obvious case where you want this?
>
> John
>
> --
> 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+unsubscr...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
--
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+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
