Match Hash Tables in Typed Racket

user_5046484 0
Viewed 221

I'm trying to match against a hash table in typed racket, but I keep getting the following error. The code works fine in untyped racket and I've tried changing it up some to no effect. The error looks like it's happening somewhere after the match macro gets expanded but I'm not familiar enough with racket to understand where or how to debug the issue.

Is is possible to use the hash-table pattern in typed racket?

(match (make-hash '((a . 2) (b . 3) (c . 2)))
    [(hash-table _ ...) #t])

Type Checker: Polymorphic function `hash-map' could not be applied to arguments:
Domains: HashTableTop (-> Any Any c) Any 
         HashTableTop (-> Any Any c) 
         (HashTable a b) (-> a b c) Any 
         (HashTable a b) (-> a b c) 
Arguments: (Mutable-HashTable Symbol Integer) (All (a) (-> a * (Listof a)))
typed-racket racket
1 Answers

it's impossible.

in the match macro, the hash-table form expands to syntax that includes the hash-map function, viz (lambda (e) (hash-map e list)). this is correct but its type is too abstract for typed racket to infer it. for the type checker to be satisfied, we'd need:

(lambda #:forall (k v) ([e : (HashTable k v)])
  (hash-map e
            (λ ([k : k] [v : v])
              (list k v))))

there's no practical way to specify this, so the hash-table matcher is unusable in typed racket.

if a for loop is usually best, e.g.

(for ([(k v) (make-hash '((a . 2) (b . 3) (c . 2)))] #:when (even? v))
  (printf "~a and ~a~n" k v))

or else something like (hash-keys m)

otherwise, positional matching requires advanced knoweldge of typed racket. for example, the following function, hash-set/cond, takes a hash table and arguments of the form (flag k v) ... and updates (if key already in table) or inserts (if key not already in table) each k/v pair if its associated flag is truthy:

(: hash-set/cond (∀ (k v) (->* ((HashTable k v))
                               #:rest-star (Any k v)
                               (HashTable k v))))
(define (hash-set/cond ht . args)
  (let loop ([ht : (HashTable k v) ht]
             [args : (Rec r (U (List* Any k v r) Null)) args])
    (if (null? args)
        ht
        (loop (if (car args)
                  (hash-set ht (cadr args) (caddr args))
                  ht)
              (cdddr args)))))

e.g.

(hash-set/cond (hash 'a 20 'b "yes")
  (even? 3) 'a 10 ; 3's not even, so 'a isn't modified
  #t 'b "canary" ; necessarily set 'b to "canary"
  'im-a-truthy-value! 'c 'new-value) ; ditto

returns #hash((a . 20) (b . "canary") (c . new-value)).

so if you end-up using typed racket a lot and want to use this kind of functionality, then it can be very useful in certain places! still, typed racket's type system can represent—but not handle—certain recursive hash table types. this is because, when checking the type of the value, hash? cannot refine the type of the hash table beyond it being a hash table with some type of key and value, i.e. hash? : (-> Any Boolean : HashTableTop) instead of (-> Any Boolean : (HashTable k v)). this makes recursing over particular recursively defined JSON schemata impossible. in these cases you must use untyped racket, though the saving grace here is that racket contracts can handle such complex definitions.

if your project is heavily based on complex hash tables, then clojure or janet are likely better language choices.

user_37957890
Related