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.
