[racket-dev] Five feature/limitation interactions conspire to drive mad

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