using neg-propositions in partition?

[John Clements]

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

[Ben Greenman]

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

> --
> 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...@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.
>

[John Clements]

Ah! Thanks for the pointer. Should have looked in the issues. Yes, 2 filters certainly work fine.

John