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

On Sun, Dec 12, 2010 at 8:15 AM, Sam Tobin-Hochstadt <samth at ccs.neu.edu> wrote:
> 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.

Well, IMO, given that the main driving design force behind TR is
matching up with Racket that you should not pick a simple convention
for relating Racket predicates to Typed Racket types and stick with it
(unless you can change Racket and, in this case, changing Racket seems
too hard). When you make exceptions to this rule, you'd want to do
that carefully and have big warnings in the docs, etc.

Another possible compromise point would be to have two types, Integer
and ExactInteger where Integer is a kind of alias for ExactInteger
that the type system itself never prints out, but that it accepts as
input. And perhaps you could even have a #:warn directive (like the
optimization flag) that would print out messages complaining about
using such aliases or something.

Or would it be possible to have a type Integer that actually matched
what integer? does? That would have the problem that people might
expect optimizations to kick when they wouldn't, but perhaps that's
the least painful point (well, I guess adding more complication to the
number hierarchy type system is its own source of pain ...)

Robby