On Thursday, December 10, 2015 at 6:55:28 PM UTC+1, johnbclements wrote: > > On Dec 10, 2015, at 9:50 AM, George Neuner wrote: > > > > On Thu, 10 Dec 2015 12:35:34 -0500, Alex Knauth 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?
Or conversely, why was the special case added? Maybe there's an interesting reason, but this seems _very_ ad-hoc. And this thread IMHO shows why some dislike "ad-hoc" solutions: they solve some problem magically, but it's rather hard to know when you can rely on them. Somebody might object that you just need to look at the definition of `Number` and at the type of `-`. I think they'd be making my point for me. Especially if you care for types for their documentation value. But I appreciate some of this is inevitable for occurrence typing — if you go for regularity, you end up with the typing rules of type theory, which aren't adequate. > The natural extension to all numbers (each number has its own type) leads > (IIUC) to a totally intractable type system. You're right in the end, but for a subtler reason. Singleton types aren't a problem per se — but expecting (- C C) to have type Zero with the current approach, on the other hand, would add to the signature of - an entry per number. OTOH, there are decision procedures for Presburger arithmetic and they've been used in experimental programming languages in the past for bound checking; I'm not familiar enough with them to say whether using them would be too crazy or just as crazy as a good research project. Static analysis researchers have used much fancier stuff, but that's even less predictable. Cheers, Paolo -- 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.
