[racket] Another basic TR question

At Thu, 13 Feb 2014 19:08:16 -0500,
Stephen Bloch wrote:
> 
> Aha.  You don't want to initialize to something inexact, because then
> the sum of a bunch of exact things would be contaminated with
> inexactness.  And the only exact zero you've got isn't a Flonum.

Exactly.

> I suppose one could invent a Float-Exact-Zero, which is a Flonum and
> also exact and also an Integer, but that would screw up the assumption
> that Flonums are inherently inexact.  Or screw up the relationship
> (I'm not sure how much there is) between TR types and internal
> representations.

Right, the problem with that is that you wouldn't be able to assume that
something that's a subtype of `Flonum' will answer true to Racket's
`flonum?' and related predicates, or that it can safely be passed to
functions that only accept floating-point numbers.


At Thu, 13 Feb 2014 22:36:12 -0500,
Bloch Stephen wrote:
> 
> And while I've got your attention...
> 
> When I tried the same thing with a smaller limit, e.g.
> 
> > (for/sum: : Flonum [[ii : Index 8]]
> >  pi)
> 
> I got not only the aforementioned complaint about Zero but also a
> complaint that it expected Index, but got Byte (presumably it decided
> 8 was small enough to fit into a byte, so everything in sight must be
> a byte).  Which is especially puzzling since Byte is a subtype of
> Index....

You're correct, `Byte' is a subtype of `Index', which makes this error
message nonsensical.

What I assume is going on is that there's an accumulator in the
expansion that gets initialized to 8, and therefore gets assigned the
type `Byte'. Then, some other code in the expansion tries to update it
with the value of `ii', which is an `Index', which fails.

This is a general problem with Typed Racket and complex macros from
untyped Racket. Macros like `for/sum' bind many variables in their
expansion and, without type annotations on all of them, Typed Racket's
inference ends up doing what it can, which is not always enough.

You can usually solve these kinds of problems by adding extra type
annotations to clarify your intent:

    (for/sum: : Real ([ii : Index (ann 8 Index)])
      pi)

The extra annotation expresses that not only should the iteration
variable be an `Index', so should the iteration bound. It's unfortunate
that this is necessary, but sometimes the type checker needs a bit of
help.

Vincent