[Feature Request] add types for `and/c` and `or/c`.

[NoahStoryM]

Is your feature request related to a problem? Please describe. Example Code

(: p [-> Any Boolean : (U Zero Symbol)])
(define p
  (λ (a)
    (or
     (and
      (natural? a)
      (not (exact-positive-integer? a)))
     (symbol? a))))

(displayln (p 0))
(displayln (p 1))
(displayln (p 'two))

Describe the solution you'd like I hope we can use and/p, or/p, and not/p so that we can define p in this way:

(: p [-> Any Boolean : (U Zero Symbol)])
(define p
  (or/p
   (and/p
    natural?
    (not/p exact-positive-integer?))
   symbol?))

Describe alternatives you've considered This is the definition I tried: (I'm not sure whether using for in the definition of predicate will cause problems, but I think it should be allowed)

#lang typed/racket

(define-predicate any? Any)
(define-predicate nothing? Nothing)

(: and/p (All (A ...) [-> (pred A) ... A (pred (∩ A ... A))]))
(define and/p (λ ps (λ (a) (and (any? a) (for/and ([p (in-list ps)]) (p a))))))

(: or/p  (All (A ...) [-> (pred A) ... A (pred (U A ... A))]))
(define or/p  (λ ps (λ (a) (or (nothing? a) (for/or ([p (in-list ps)]) (p a))))))

(: not/p (All (A) [-> (pred A) [-> Any Boolean : #:+ (! A) #:- A]]))
(define not/p (λ (p) (λ (a) (not (p a)))))

[Optional] Additional context Some additional suggestions

1. Since we allow the use of the mathematical symbol ∩, will it be better to also support ∪?
2. From the above code, we can see that in the definition of and/p, or/p, and not/p, any? and nothing? are somewhat similar to true and false. Should we add any? and nothing? in TR? (I feel that in some cases where predicate is used as a function parameter, any? and nothing? may play a role similar to Boolean)

[samth]

I'm confused about the motivation here. The code you started with seems like how I would write the program in Racket, and thus how I'd want to write the program in Typed Racket as well.

If the problem is that we can't easily define combinators over predicates to put in a library, then that seems like a separate issue from adding things to typed/racket itself, which is intended to be a typed version of the contents of racket.

However, it seems like these definitions of and/p and or/p work correctly, as well as your definition of not/p:

(: and/p (All (A B) [-> (pred A) (pred B) (pred (∩ A B))]))
(define and/p (λ (p q) (λ (a) (and (p a) (q a)))))

(: or/p (All (A B) [-> (pred A) (pred B) (pred (U A B))]))
(define or/p (λ (p q) (λ (a) (or (p a) (q a)))))

One further problem is that not/p doesn't produce a predicate in the sense your and/p expects. That's because Typed Racket doesn't have negation types. If you don't use not/p but instead write (lambda (x) (equal? 0 x)) then it works.

[NoahStoryM]

My initial motivation was that I found myself often use predicate to check the same variable in cond by and, or and not, it looks cumbersome in these cases.

And in most cases, flat contract and predicate are very similar. In fact, my original idea was to add types to and/c, or/c and not/c (maybe unsafe should be used here):

(require/typed racket/contract/base
   [or/c (All (A ...) [-> (pred A) ... A (pred (U A ... A))])]
   [and/c (All (A ...) [-> (pred A) ... A (pred (∩ A ... A))])]
   [not/c (All (A) [-> (pred A) [-> Any Boolean: #:+ (! A) #:- A]])])

But now it seems that because TR does not have negation types, and there is no way to use ooo in U and ∩, so there is no way to achieve them?

Maybe as you said, I should add (All (A B C D E) (case-> ...)) to and/c and or/c here. But I think the problem here is that if ooo cannot be used in some return value types, it will affect the definition of some composite functions.

[samth]

I'm still a bit confused. It sounds like you want to program in a more point-free style when writing predicates. Contract combinators can be used for this, but (a) not/c doesn't work that well because TR lacks negation and (b) it's not possible to use ... with union and intersection so you would have to limit things to a fixed arity.

That all seems accurate, but then I don't understand what the feature request would be.

[NoahStoryM]

I'm sorry my thoughts were a bit confusing, maybe I need some time to sort out them. I wonder if you are willing to provide types for and/c and or/c in TR? Maybe in this way:

(provide or/c and/c)

(require typed/racket/unsafe)

(unsafe-require/typed racket/contract/base
  [or/c  (All (A B C D E)
              (case-> [-> (pred Any)]
                      [-> (pred A) (pred A)]
                      [-> (pred A) (pred B) (pred (U A B))]
                      [-> (pred A) (pred B) (pred C) (pred (U A B C))]
                      [-> (pred A) (pred B) (pred C) (pred D) (pred (U A B C D))]
                      [-> (pred A) (pred B) (pred C) (pred D) (pred E) (pred (U A B C D E))]))]
  [and/c (All (A B C D E)
              (case-> [-> (pred Nothing)]
                      [-> (pred A) (pred A)]
                      [-> (pred A) (pred B) (pred (∩ A B))]
                      [-> (pred A) (pred B) (pred C) (pred (∩ A B C))]
                      [-> (pred A) (pred B) (pred C) (pred D) (pred (∩ A B C D))]
                      [-> (pred A) (pred B) (pred C) (pred D) (pred E) (pred (∩ A B C D E))]))])