Type Checker: Inference for polymorphic keyword functions not supported

Hi,

I want to do a union of two hash tables mapping symbols to numbers, summing up the values for duplicate keys. Here's what I write:

#lang typed/racket

(require racket/hash)

(define h1 : (Immutable-HashTable Symbol Number) #hash((a . 1)))
(define h2 : (Immutable-HashTable Symbol Number) #hash((a . 2)))

(: combine-plus (-> Number Number Number))
(define (combine-plus a b) (+ a b))

(hash-union #:combine combine-plus h1 h2)

This gives the error "Type Checker: Inference for polymorphic keyword functions not supported."

When I use inst like so:

((inst hash-union Symbol Number) #:combine combine-plus h1 h2)

I get "Type Checker: Unexpected keyword argument #:combine".

What should I do to get this example to typecheck?

1 Like

It appears that the current type provided by Typed Racket for hash-union does not include support for the #:combine feature:

> (:print-type hash-union)
(All (a b)
  (-> (Immutable-HashTable a b) (HashTable a b) * (Immutable-HashTable a b)))
>

I don't see any TR issues that reference hash-union, so it's possible that this is something that could easily be added, although my intuition is extraordinarily weak here.

There are also many workarounds... hm. Well, I tried one I hoped would work, and got a really fun error.

Specifically, I tried this:

#lang typed/racket

(require/typed
 racket/hash
 [hash-union
  (All (a b) (-> (Immutable-HashTable a b)
                 #:combine (b b -> b)
                 (HashTable a b) *
                 (Immutable-HashTable a b)))]
 )
 

(define h1 : (Immutable-HashTable Symbol Number) #hash((a . 1)))
(define h2 : (Immutable-HashTable Symbol Number) #hash((a . 2)))

(: combine-plus (-> Number Number Number))
(define (combine-plus a b) (+ a b))

((inst hash-union Symbol Number) #:combine combine-plus h1 h2)

And it type-checks! Yay! ... But when I run it, I get this error:

hash/c: contract violation
  expected: chaperone-contract?
  given: a7
> 

@samth would certainly be able to answer this question.

1 Like

Thank you @jbclements for your reply. I did check the type of hash-union after I started the discussion (altough I forgot about :print-type, that's neat!) and I saw indeed that the type did not include any one of the optional keyword arguments.

Thank you also to have tried require/typed: I get exactly the same error, even the 7 in a7.

I tried another workaround with an untyped submodule converting the keyword argument into a normal argument:

#lang typed/racket

(module hash-union-submod racket/base
  (require racket/hash)

  (provide hash-union2-combine)
  (define (hash-union2-combine ht1 ht0 combine-fun)
    (hash-union ht1 ht0 #:combine combine-fun)))

(require/typed 'hash-union-submod
  [hash-union2-combine (All (a b) (-> (Immutable-HashTable a b)
                                      (Immutable-HashTable a b)
                                      (-> b b b)
                                      (Immutable-HashTable a b)))])

(define h1 : (Immutable-HashTable Symbol Number) #hash((a . 1)))
(define h2 : (Immutable-HashTable Symbol Number) #hash((a . 2)))
h1
h2

(: combine-plus (-> Number Number Number))
(define (combine-plus a b) (+ a b))

(hash-union2-combine h1 h2 combine-plus)

I really expected this to work, but guess what:

; hash/c: contract violation
;   expected: chaperone-contract?
;   given: a4

Well, the good news is that this seems to be the same kind of error as you get with require/typed. The bad news is that we don't even have a workaround :smiley:

I tried defining a couple functions from scratch, and I ran into the kind of obvious conclusion that type inference is not supported for the keyword arguments of polymorphic functions :smiley:

#lang typed/racket

(: foo (All (a) (->* (a a) () (Listof a))))
(define (foo x y) (list x y))
(foo 1 2)

(: bar (All (a) (->* (a a) (#:arg1 Number) (Listof a))))
(define (bar x y #:arg1 [z 1]) (list x y))
(bar 1 2)

(: baz (All (a) (->* (a a) (#:arg1 a) (Listof a))))
(define (baz x y #:arg1 [z x]) (list x y z))
(baz 1 2)
(baz 1 2 #:arg1 3) ; Type Checker: Inference for polymorphic keyword functions not supported

So, the problem kicks in when the type of the keyword argument involves a type variable.


OK, throwing away polymorphism works:

#lang typed/racket

(require/typed racket/hash
  [hash-union
   (->* ((Immutable-HashTable Symbol Number))
        (#:combine (Number Number -> Number))
        #:rest (HashTable Symbol Number)
        (Immutable-HashTable Symbol Number))])

(define h1 : (Immutable-HashTable Symbol Number) #hash((a . 1)))
(define h2 : (Immutable-HashTable Symbol Number) #hash((a . 2)))
h1
h2

(: combine-plus (-> Number Number Number))
(define (combine-plus a b) (+ a b))

(hash-union h1 h2 #:combine combine-plus)
(hash-union h1 h2 h2 #:combine combine-plus)
(hash-union h1 h2 #:combine +)

As you see, I can even use + directly, without hiding it behind combine-plus.

I guess I can just replace Symbol and Number with Any for now and help myself to casts, but I hope a better solution exists.

For the record, here is the solution with which I plan to continue for now, after having tried 3–4 different things:

#lang typed/racket

(module hash-union-submod racket
  (require (only-in racket/hash hash-union))
  (provide hash-union-list)
  (define (hash-union-list
           hts
           [combine
            (λ _ (error 'hash-union-list
                        "Don't know how to combine the values of duplicate keys."))])
    (apply hash-union #:combine combine hts)))

(require/typed 'hash-union-submod
  [hash-union-list
   (->* ((Listof (Immutable-HashTable Any Any)))
        ((-> Any Any Any))
        (Immutable-HashTable Any Any))])

(: combine-plus-any (-> Any Any Any))
(define (combine-plus-any x y)
  (+ (cast x Number) (cast y Number)))

(hash-union-list '(#hash((a . 1)) #hash((b . 1))))
(hash-union-list '(#hash((a . 1)) #hash((a . 1))) combine-plus-any)

In fact, what I need is applying hash-union to a list of hashes. What I do here is setting up a function hash-union-list which applies hash-union to a list with the #:combine keyword argument, in an untyped module hash-union-list. I then import hash-union-list into a typed module, replacing what might have been type variables by Any.

While this solution does the trick for me, it is underwhelming compared to this line of untyped Racket:

(apply hash-union #:combine combine-plus '(#hash((a . 1)) #hash((b . 1))))

Furthermore, if I define the type of hash-union-list with the type variables a and b, I run into the same contract violation as mentioned above in this discussion.

I'd be very interested in any effort to bring proper typechecking to keyword arguments. Naively, I have the impression that it shouldn't be that hard to do, but I expect to be wrong. Unfortunately, my time is limited, but if there are "easy" tasks, I'd be very happy to contribute.

1 Like

The best thing to contribute would be to add the #:combine argument to the type of hash-union which is here: typed-racket/base-env.rkt at d65ff8bd7146b15b79f31506f8aca410aed196e4 · racket/typed-racket · GitHub

2 Likes

Thanks @samth. I spend quite a bit of time thinking and reading base-env.rkt (and being busy with my day job :smiley: ) and I think I can boil down my problem to the following two questions:

  1. How is ->* in base-env.rkt different from the one which is exposed from the library? The type of hash-union in base-env.rkt seems to imply that the type of the rest arguments is first given as a list, and then the type of the mandatory arguments is specified, which looks like the reverse of the description in the documentation. Also, a level of parentheses is missing with respect to what I'd expect (i.e.,(-HT a b) instead of ((-HT a b))). So I am totally lost as to how I could add a keyword argument to that type. I tried looking for similar examples, but the best I could find is add-between which uses ->key instead of ->*.

  2. What is the best way to play with the development version of Typed Racket? Is raco pkg install-ing typed-racket-lib okay?