> On Jan 11, 2018, at 9:52 AM, Sam Tobin-Hochstadt <sa...@cs.indiana.edu> wrote: > > 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.
Okay, that makes sense. Many thanks for taking the time to write this up. John > > Sam > > On Thu, Jan 11, 2018 at 12:35 PM, 'John Clements' via Racket Users > <email@example.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.