[racket] filters and the type of partition

I think your first function ought to type check, and that it doesn't is a bug.

Second, `partition` could be relaxed in the way you say, and could use
#:+ as well.

Sam

On Thu, Sep 18, 2014 at 4:37 PM, Alexander D. Knauth
<alexander at knauth.org> wrote:
> 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?
>
>
>
> ____________________
>   Racket Users list:
>   http://lists.racket-lang.org/users