[racket-dev] (round), etc. in Typed Racket

From: Sam Tobin-Hochstadt (samth at ccs.neu.edu)
Date: Sun Dec 12 09:15:34 EST 2010

On Sat, Dec 11, 2010 at 10:53 PM, Robby Findler
<robby at eecs.northwestern.edu> wrote:
>> Changing Racket is tricky, but I think using the `Integer' type for
>> something useless (it's not even currently represented in the TR type
>> system) would be a mistake.
> Well, the change to TR would be to change "Integer" to "ExactInteger"
> (or similar) presumably, not to add a useless type.

I think not having an `Integer' type would be just as bad.

Given that (integer? 3.0) => #t, I think there will be an inevitable
discrepancy between what people expect and what the type system does.
One of these definitions has to not type check:

(: x : Integer)
(define x 1)

(: f : Integer -> Integer)
(define (f x) (add1 x))

(: g : Any -> Integer)
(define (g x) (assert x integer?))

You're suggesting the first one fail, because `Integer' would go away.
 Right now only `g' fails.  Adding an `Integer' type that corresponds
to `integer?' would make `f' fail.  My feeling is that the fewest
people will run into `g', and that it's therefore the right choice,
since there will be a FAQ about this regardless.
sam th
samth at ccs.neu.edu

Posted on the dev mailing list.