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 racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
