Ah! Thanks for the pointer. Should have looked in the issues. Yes, 2 filters certainly work fine.
John > On Oct 5, 2021, at 4:45 PM, Ben Greenman <benjaminlgreen...@gmail.com> wrote: > > There's an issue open about partition: > https://github.com/racket/typed-racket/issues/138 > > Does `my-partition` work like you'd want? Based on Alex's last comment > on the issue, it seems hard to give a predicate that matches the type. > > > (Whenever I've wanted `partition` in typed code, I was always able to > use 2 filters instead.) > > On 10/5/21, 'John Clements' via Racket Users > <racket-users@googlegroups.com> wrote: >> I was somewhat surprised to see today that I can’t use a predicate with both >> positive and negative propositions in the way I would expect with >> partition: >> >>> (:print-type partition) >> (All (a b) >> (case-> >> (-> (-> b Any : #:+ a) (Listof b) (values (Listof a) (Listof b))) >> (-> (-> a Any) (Listof a) (values (Listof a) (Listof a))))) >> >> >> Specifically, I would have expected the type to be something like this: >> >> (All (a b c) >> (case-> >> (-> (-> b Any : #:+ a) (Listof b) (values (Listof a) (Listof b))) >> ;; the second list must consist of 'c's: >> (-> (-> b Any : #:+ a #:- c) (Listof b) (values (Listof a) (Listof c))) >> (-> (-> a Any) (Listof a) (values (Listof a) (Listof a))))) >> >> … so that if, say, I had a list of Elephants and Emus, that I could use >> elephant? to split it into two lists: one of type (Listof Elephant) and one >> of type (Listof Emu). >> >> I tried to roll my own, and got pretty close: >> >> (: my-partition >> (All (a b c) >> (case-> >> ;; the second list must consist of 'c's: >> (-> (-> b Any : #:+ a #:- c) (Listof b) (values (Listof a) (Listof >> c))) >> ))) >> >> (define (my-partition my-pred elts) >> (cond [(empty? elts) >> (values '() '())] >> [else >> (define-values (stacks non-stacks) >> (my-partition my-pred (rest elts))) >> (define f (first elts)) >> (cond [(my-pred f) >> (values (cons f stacks) >> non-stacks)] >> [else >> (values stacks (cons f non-stacks))])])) >> >> That is, I can do it for the case-> clause that I care about. Putting the >> other two back in there causes it to fail type-checking. Is that the >> problem, that TR can’t accommodate both flavors in the same type? >> >> John >> >> >> -- >> You received this message because you are subscribed to the Google Groups >> "Racket Users" group. >> To unsubscribe from this group and stop receiving emails from it, send an >> email to racket-users+unsubscr...@googlegroups.com. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/racket-users/aa1e77a8-9cc4-4f99-b413-1304daeec12b%40mtasv.net. >> -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/724d3012-b8e3-4be2-9ce1-fbc15cbd0bd6%40mtasv.net.
