[racket] Specifying the type of a function that contains a type test (but isn't one)

On Mon, Apr 18, 2011 at 3:02 PM, Jeremiah Willcock <jewillco at osl.iu.edu> wrote:
> Given the following Typed Racket program:
>
> #lang typed/racket
>
> (: greater-than-5? (Any -> Boolean))
> (define (greater-than-5? x)
>  (and (integer? x) (> x 5)))

First, you probably want to use `exact-integer?' here, see the TR docs
for `Integer'.

> (: equal-to-7? (Any -> Boolean))
> (define (equal-to-7? x)
>  (and (greater-than-5? x) (= x 7)))
>
> I receive the error (highlighting the x in (= x 7)):
>
> Type Checker: Expected Complex, but got Any in: x
>
> Is there a way to tag greater-than-5? to mark that it only returns #t on
> integers?  Marking its type as (Any -> Boolean : Integer) causes an error:
>
> Type Checker: Expected result with filter ((Integer @ x) | (! Integer @ x)),
> got filter (((U Float Integer) @ x) | (OrFilter (! Integer @ x) ((U Float
> Integer) @ x))) in: (and (integer? x) (> x 5))

Second, there isn't currently a way to write this, because I haven't
found a notation I like.  It's something I want to do fairly soon,
though.
-- 
sam th
samth at ccs.neu.edu