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
--
You received this message because you are subscribed to the Google Groups
"Racket Developers" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To post to this group, send email to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/racket-dev/8d04c19a-828d-40b8-aa76-25b086d58287%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
