IIRC, the only numeric type that are singletons are Zero and One, so this also typechecks:
(+ 1 (if (= 0 (- 0 0)) 1 "x")) On a related note, the (untyped)Racket optimizer has constant folding, so in (untyped)Racket all these expressions are compiled to 2. I don't know if it's possible to add constant folding to Typed Racket. Anyway, other obvious expressions like (lambda (x) (+ 1 (if (eq? x x) 1 "x"))) are not reduced (currently). Gustavo On Thu, Dec 10, 2015 at 3:12 PM, Vincent St-Amour <[email protected]> wrote: > Right. > > The key distinction here is that TR is not so much reasoning about > constants, but about a singleton type. So TR is still working in terms > of types, not in terms of concrete values. > > Vincent > > > > On Thu, 10 Dec 2015 11:55:24 -0600, > 'John Clements' via Racket Users wrote: >> >> >> > On Dec 10, 2015, at 9:50 AM, George Neuner <[email protected]> wrote: >> > >> > On Thu, 10 Dec 2015 12:35:34 -0500, Alex Knauth >> > <[email protected]> wrote: >> > >> >> In typed racket (- 1 1) and (- 2 2) are equal at runtime, but the type >> >> checker doesn't necessarily know that at compile time. It knows that >> >> (- 1 1) is zero because that's a special case in the type system. But it >> >> doesn't have a special case for (- 2 2), so it only knows that that's a >> >> Fixnum. >> > >> > But in this case the type checker isn't dealing with variables. Which >> > begs the question why is (- 1 1) special cased? Shouldn't there be a >> > general rule: (- C C) where C is a numeric constant? >> > [Ok, I know equality is a problem with floating point ... but, still, >> > the principle remains.] >> >> Check out the numeric tower in TR: there’s a type that includes just the >> number 1. The natural extension to all numbers (each number has its own >> type) leads (IIUC) to a totally intractable type system. >> >> John >> >> > >> > George >> > >> > -- >> > You received this message because you are subscribed to the Google Groups >> > "Racket Users" group. >> > To unsubscribe from this group and stop receiving emails from it, send an >> > email to [email protected]. >> > For more options, visit https://groups.google.com/d/optout. >> >> >> >> -- >> You received this message because you are subscribed to the Google Groups >> "Racket Users" group. >> To unsubscribe from this group and stop receiving emails from it, send an >> email to [email protected]. >> For more options, visit https://groups.google.com/d/optout. > > -- > You received this message because you are subscribed to the Google Groups > "Racket Users" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. For more options, visit https://groups.google.com/d/optout.
