Странное поведение проверки типов при использовании apply к списку наборов в набранной ракетке

Question

У меня есть список наборов, и я хочу взять их объединение.

Что-то вроде следующего

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

, который работает и дает мне правильный результат (set '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

@ Диагноз Алексис Кинг правильный, и ее предложение использовать более конкретный тип для входного списка будет хорошим, если вы знаете, что список не пустой. Однако в некоторых случаях невозможно изменить тип списка ввода: иногда список пуст и вам приходится с ним иметь дело.

Когда список пуст, вам нужен пустой набор, так что вы можетеприменить set-union к пустому набору в дополнение к списку:

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

Это заставит Typed Racket принять объединение, даже если 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)