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 [email protected].
For more options, visit https://groups.google.com/d/optout.
