Weird typechecker behavior when using apply on a list of sets in typed racket

user_1412255 0
Viewed 98

I have a list of sets and I want to take a union of those.

Something like the following

(apply set-union (list (set 'a) (set 'b)))

Which works and gives me the correct result (set 'a 'b)

Now if I try to write the same code like this:

(: l (Listof (Setof Symbol)))
(define l (list (set 'a) (set 'b)))
(apply set-union l)

Then I get the following error:

Type Checker: Bad arguments to function in `apply':
  Domains: (Listof e)(Listof e) *
           (Setof e)(Setof e) *
  Arguments: (Listof (Setof Symbol))

How can I apply the set-union function to a list of sets?

I should mention that the same piece of code works with untyped racket language or with using language typed/racket/no-check, which is why I believe that it's definitely a typechecking issue.

typed-racket racket types
2 Answers

The error message notes that the domain of the function involving sets is (Setof e) (Setof e) *, which means set-union needs at least one argument to be correctly applied. (Listof (Setof Symbol)) could be the empty list, which would cause a runtime error.

Therefore, you should give l a more specific type. You could use (List (Setof Symbol) (Setof Symbol)) to describe it most precisely, or if you just want a type that captures the notion of “a list of sets with at least one element,” you can use the type (Pairof (Setof Symbol) (Listof (Setof Symbol))).

user_4653780

@Alexis King's diagnosis is correct, and her suggestion of using a more specific type for the input list is a good one if you know the list is non-empty. However in some cases it's not possible to change the type of the input list: sometimes the list is empty and you have to deal with it.

When the list is empty, you want an empty set, so you can apply set-union to the empty set in addition to the list:

(define l (list))
(apply set-union (set) l)
;=> (set)

This gets Typed Racket to accept the union even when l has the original type (Listof (Setof Symbol)) which can be empty:

(: l (Listof (Setof Symbol)))
(define l (list (set 'a) (set 'b)))
(apply set-union (set) l)
;=> (set 'a 'b)

To make sure the result type can be specific, so that the union can be (Setof Symbol), you should make sure (set) has a type at least as specific. In this case the empty set can have type (Setof Nothing), so you can use ((inst set Nothing)).

(: l (Listof (Setof Symbol)))
(define l (list (set 'a) (set 'b)))
(apply set-union ((inst set Nothing)) l)
;- : (Setof Symbol)
;=> (set 'a 'b)
user_54325010
Related