On Thu, 10 Dec 2015 13:10:04 -0600,
Paolo Giarrusso wrote:
>
> 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.
I don't remember, off the top of my head, why we added that particular
special case to the type of `-`.
In general, though, those kinds of more precise clauses inside the types
of numeric operations are there to enable closure properties. If you
know that you're operating on, e.g., non-negative floats, then you may
be able to rule out complex-number results in parts of your code.
> 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.
Right. That's why we've built tools to get information about these types
more digestible:
http://docs.racket-lang.org/ts-reference/Exploring_Types.html
> > 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.
You may be interested in:
http://andmkent.com/blog/2015/11/22/new-draft-paper-occurrence-typing-modulo-theories/
Vincent
--
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.
