At Wed, 02 Jan 2013 16:57:39 -0700,
Neil Toronto wrote:
On 01/02/2013 02:51 PM, Vincent St-Amour wrote:
In your experience, have these types caused you trouble other than when
you went looking for them specifically?
Not that I recall. If I stick to union types like Integer,
Exact-Rational, Flonum, Real, and Number, they don't often show up. I
expect generalization and covariance have a lot to do with it.
Great!
Of course, these types caused me trouble immediately because I went
looking for them immediately, to get optimizations. It's a happy
accident that always using Index for bounds and bounds-checked values
works out so well. (Unless you planned it?)
That's the reason I added `Index'. Without it, fixnum optimizations
would have been pretty much impossible.
This brings me to what I think is the major issue for us n00bs: the
types force you to understand the numeric tower really well if you want
to use types more precise than `Number'. Before you reach that level of
understanding, though, and Typed Racket spits errors at you, it's hard
to tell whether it has a legitimate complaint - especially when you
don't know whether you should expect, say, (i . fx . 0) to prove i :
Positive-Index.
Were there specific corners of the tower that you found frustrating
(other than fixnum types)?
Mostly `sqrt' and `log', when it's hard to prove their arguments are
nonnegative. I've gotten around it using `flsqrt' and `fllog'. I was
usually working with flonums anyway.
Yep, that's a good workaround (which OC recommends). It would be nice to
also have specialized versions of `sqrt', `log' and co that accept
reals, but raise exceptions instead of returning complex results.
They would still have to internally check for sign before calling `sqrt'
(or `real?' after, if we optimistically call `sqrt'), so they may not be
any faster than doing it inline in user code, but they may still be
convenient.
Would it make sense to provide something like that as part of the math
library?
One that has bugged me recently is that TR can't prove (* x (conjugate
x)) : Nonnegative-Real. I have no idea how you'd do it without turning
Number into a product type, though.
With richer types for complexes, this could be expressible. But it would
require duplicating the numeric tower for each component, which would
get very complicated (and slow down typechecking) very fast. We thought
about doing it, but quickly decided against it. The costs clearly
outweight the benefits.
I almost forgot this one:
(/ (ann 5 Nonnegative-Real) (ann 3 Nonnegative-Real))
- : Real
1 2/3
That one is by design.
- (/ (ann +inf.0 Nonnegative-Real) (ann -0.0 Nonnegative-Real))
- : Real
-inf.0
Considering all the floating-point zeroes to be non-negative (and
non-positive) helps with closure properties, but does cause some
unexpected corner cases. We've thought about that one for a while, and I
think it's the right compromise.
If you want more, you can grep for `assert' in the math library.
I will, thanks!
But it's often really hard to prove that something is nonnegative
without an explicit cast, assertion, or test, and thus stay within the
reals in expressions with roots.
I actually see that as a positive: if a property is too hard to prove
using the type system alone, you have the option to use casts,
assertions, or tests to help TR prove what you want [1]. Casts,
assertions and tests give you extra power to prove things that you
couldn't prove otherwise, or to make proofs easier.
We should differentiate between what *I* can prove and what *Typed
Racket* can prove. I can usually prove more.
Right. Replace prove with make TR prove in what I said.
Thanks again for the feedback!
Vincent
_
Racket Developers list:
http://lists.racket-lang.org/dev
