在类型化球拍的集合列表上使用apply时，会出现奇怪的类型检查器行为

Question

我有一个集合的列表，我想取这些集合的并集。

类似于下面的内容

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

它可以工作并给出正确的结果(设置'a 'b)

现在，如果我尝试像这样编写相同的代码：

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

然后我得到以下错误：

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

如何将集合并集函数应用于集合列表？

我应该提到的是，同一段代码适用于非类型化球拍语言或使用语言typed/racket/no-check，这就是为什么我认为这绝对是一个类型检查问题。

Answer 1

错误消息指出，涉及集合的函数的域是(Setof e) (Setof e) *，这意味着set-union至少需要一个参数才能正确应用。(Listof (Setof Symbol))可能是空列表，这将导致运行时错误。

因此，您应该为l指定一个更具体的类型。您可以使用(List (Setof Symbol) (Setof Symbol))来最精确地描述它，或者，如果您只需要一个类型来捕捉“至少包含一个元素的集合的列表”的概念，则可以使用(Pairof (Setof Symbol) (Listof (Setof Symbol)))类型。

Answer 2

@Alexis King的诊断是正确的，如果你知道列表是非空的，她建议对输入列表使用更具体的类型是一个很好的建议。但是，在某些情况下，不可能更改输入列表的类型:有时列表是空的，您必须处理它。

当列表为空时，您需要一个空集，因此除了列表之外，还可以对空集应用set-union：

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

即使l具有可以为空的原始类型(Listof (Setof Symbol))，它也会被类型化为球拍以接受联合：

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

为了确保结果类型可以是特定的，以便联合可以是(Setof Symbol)，您应该确保(set)的类型至少是特定的。在这种情况下，空集可以具有(Setof Nothing)类型，因此可以使用((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)