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 <alexan...@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 ____________________ Racket Users list: http://lists.racket-lang.org/users
