Non-Trivial Filters in Typed Racket

[Kevin Clancy]

I've been experimenting with non-trivial filters for the numeric comparisons whose types are specified in base-env-numeric.rkt. For example, for the type of fl>=, I'm trying to use this:

(-> -Flonum -Flonum B : (-FS (-and (-imp (-filter -FlonumNan 0) -bot)
                                   (-imp (-filter -FlonumNan 1) -bot)
                                   (-or (-filter -PosFlonum 0)
                                        (-and (-filter -FlonumZero 0)
                                              (-filter -NonPosFlonum 1))
                                        (-and (-filter -NegFlonum 0)
                                              (-filter -NegFlonum 1))))
                             -top))

I think this could be improved by adding a negative filter, but with what I currently have I assumed that the following program would type-check:

(define (pos_only [x : Positive-Flonum]) x)

(define (doit [x : Nonnegative-Flonum] [y : Positive-Flonum])
  (define q (if (fl>= x y) x 3.0))
  (pos_only q))

It does not type-check. Instead, it produces the following type error:

. Type Checker: type mismatch
  expected: Positive-Flonum
  given: Nonnegative-Flonum in: x

The true filter implies that y is not nan. It also implies that if y is neither non-positive or negative then x must be positive. Since y is not nan, it is not possible for y to be both positive and non-positive. Hence, x should have type PositiveFlonum in its occurrence in the if statement. What has gone wrong? Do non-trivial filters work correctly at this point?

Thanks,
Kevin