[racket] filters and the type of partition
Is there any way for a predicate-ish thing to do something like this:
#lang typed/racket
(: vectorof-real? : [(U Number (Vectorof Real))
-> Boolean :
#:+ (Vectorof Real)
#:- Number])
(define (vectorof-real? x)
(vector? x))
Because this works:
(let ([x : (U Number (Vectorof Real)) #(1 2 3)])
(if (vector? x)
(ann x (Vectorof Real))
(ann x Number)))
And also I noticed the types for the functions filter and partition are:
> filter
- : (All (a b)
(case->
(-> (-> a Any : #:+ b) (Listof a) (Listof b))
(-> (-> a Any) (Listof a) (Listof a))))
#<procedure:filter>
> partition
- : (All (a b)
(case->
(-> (-> a Any) (Listof a) (values (Listof a) (Listof a)))
(-> (-> Any Boolean : a) (Listof b) (values (Listof a) (Listof b)))))
#<procedure:partition>
For the filter function, the predicate only has to accept the type a for both cases and can return Any for both cases. Is there any reason why the second case of partition doesn’t do that? And is there a reason why it doesn’t use #:+ for the filter?
The current type for partition wouldn’t allow me to use my vectorof-real? as the predicate even if it did work, right? But filter would?