[racket] Another basic TR question

At Thu, 13 Feb 2014 16:22:35 -0500,
Bloch Stephen wrote:
> 
> [1  <multipart/signed (7bit)>]
> [1.1  <multipart/alternative (7bit)>]
> [1.1.1  <text/plain; us-ascii (quoted-printable)>]
> 
> On Feb 13, 2014, at 2:51 PM, Sam Tobin-Hochstadt wrote:
> 
> >> (for/sum: : Flonum [[ii : Index 300]]
> >>  pi)
> >> 
> >> and I get the type error "Expected Flonum, but got Zero".  Where is there a
> >> zero anywhere in this code?  And even if there were a zero, shouldn't Zero
> >> be a subtype of Flonum?
> >> 
> >> Don't tell me the Zero I'm running into is the initial value of for/sum's
> >> hidden accumulator....
> > 
> > Unfortunately, that's exactly what I'm going to tell you.  Typed
> > Racket isn't smart enough to know that the initial value is never
> > used, and so 0 is thought to be a possibility.
> 
> Doesn't that make for/sum: useless for anything other than exact integers?

`for/sum:' is also useful for any return type that includes exact
integers (well, that include at least exact zero), such as `Real'.
`Flonum' (and `Single-Flonum') are the only types for which it won't
work.

> Couldn't for/sum: initialize its accumulator to a Real-Zero rather
> than the overly-specified type Zero?  (That would rule out complexes,
> but it would be a big step in the right direction.)  (Should there be
> a Complex-Zero type?)
> 
> Even better, could for/sum: look at the annotation type and decide
> what initial value (0 or #i0.0) to use?

That would solve this problem, but would have some potentially
undesirable side effects. For example, the return value of `for/sum:'
of an empty sequence would depend on the type annotation. This would
also be a divergence from untyped Racket's behavior, which Typed Racket
aims to always be consistent with.


At Thu, 13 Feb 2014 16:30:50 -0500,
Bloch Stephen wrote:
> On Feb 13, 2014, at 2:56 PM, Vincent St-Amour wrote:
> > You can use `assert' to check, at run-time, that you do always get a
> > Flonum:
> > 
> >    (assert (for/sum: : Real [[ii : Index 300]]
> >              pi)
> >            flonum?)
> > 
> > This expression typechecks at type Flonum.
> 
> Hmm.  So just changing the annotation type from Flonum to Real does
> the trick?

Yes. The `Real' type includes integers as well as floating point numbers
(and also exact rationals (i.e. fractions)).

> for/sum: initializes its accumulator to an exact 0, which is of type
> Zero, which is a subtype of Real but not of Flonum.
> It then adds pi, which is a Flonum, which is also a subtype of Real,
> and it has no problem proving the answer to be a Real (just not a
> Flonum).

Exactly.

> Even though AFAIK anything plus a Flonum produces either a Flonum or
> an error.

That's true for addition (but not for, say, multiplication). However, as
far as the typechecker knows, there may never actually be any additions
performed. If the input sequence is empty, the initial value of the
accumulator will get returned right away. In your case, that can't
happen, but the typechecker doesn't know that.

> I'm so confused....

If you need help navigating types, Typed Racket provides some type
exploring facilities:

  http://doc.racket-lang.org/ts-reference/Exploring_Types.html

You can do things like querying a function's type to know, say, the
return type you would get given argument types, and vice versa. You can
also expand union types (like `Real') to see what they contain.

For a more detailed description of the design principles of the Typed
Racket numeric tower, we wrote a paper on the topic:

  http://www.ccs.neu.edu/racket/pubs/padl12-stff.pdf


Vincent