On 01/02/2013 02:51 PM, Vincent St-Amour wrote:
At Wed, 02 Jan 2013 12:39:21 -0700,
Neil Toronto wrote:
One place this bit me pretty early was getting TR to optimize loops over
indexes *without using casts or assertions*.
Right, fixnum types are tricky. They don't have many closure properties,
so it's hard to stay within these types.
Because of this, we try to avoid exposing these types to beginners as
much as possible (by, e.g., not having functions in the standard library
require them as arguments). The hope is that only experts that are
trying to either (1) get every bit of performance our of their programs
or (2) enforce strict range properties in their programs actually need
to use these types. For the first use case, OC provides some help (and
better support is on the way).
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.
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?)
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.
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.
I almost forgot this one:
> (/ (ann 5 Nonnegative-Real) (ann 3 Nonnegative-Real))
- : Real
1 2/3
If you want more, you can grep for `assert' in the math library.
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. For example, *I* know that
this function preserves types:
(: x^2n (Real Positive-Integer -> Nonnegative-Real))
(define (x^2n x n)
(expt x (* 2 n)))
But TR has no concept of "even, positive integer". (To be clear, I'm not
advocating adding it.) Frustration happens when I know something, but I
can't get TR to "know" it.
FWIW, this mismatch doesn't happen very often anymore, probably because
I know TR's model of the numeric tower a lot better, and because you've
improved Racket's basic math types a lot.
Neil ⊥
_________________________
Racket Developers list:
http://lists.racket-lang.org/dev
