[racket] filters and the type of partition

From: Alexander D. Knauth (alexander at knauth.org)
Date: Thu Sep 18 16:37:10 EDT 2014

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?  




Posted on the users mailing list.