For/sum in typed/racket

Questions & Answers
1

I'm experimenting with typed/racket to see if it can speed up some lengthy numerical calculations. As a first step, I tried to sum all the square roots up to a million, first in plain Racket:

(for/sum ([i 1000000])
  (sqrt i)))

This takes around 130ms on my computer, which isn't setting any speed records. Using racket/flonum, the performance is much improved:

(for/sum ([i 1000000])
  (flsqrt (->fl i)))

This is down to 8ms, which is pretty good! I tried a few other languages that I know, and the only ones to beat this were C, and JS (when using floats, but not with bignums).

Next I wanted to see if typed/racket could yield similar gains, perhaps without explicit types at each step. (Ideally, it would also optimize through function calls.) Unfortunately, I've been unable to figure out a valid syntax for using for/sum in typed/racket.

I see lots of "type-ann-maybe" in the documentation (and are they the same in either position?), but I just can't figure out how to make the compiler happy. The documentation for this function even says "All annotations are optional", yet my first example (above) in typed/racket yields "Type Checker: Error in macro expansion -- insufficient type information to typecheck. please add more type annotations".

When I try to add annotations to help it out, such as:

(for/sum : Flonum ([i : Integer 1000000])
  (flsqrt (->fl i)))

I get:

Type Checker: type mismatch
  expected: Flonum
  given: Zero

I've tried every combination I can think of, of typed functions, casts, hints, and so on. No matter the error, it points to the first character of the for/sum line, and gives the "context" as typed-racket/typecheck/tc-toplevel.rkt, which seems unhelpful. There's nothing in the error message (at least, to this vanilla Racket user) which suggests an obvious fix.

I did see a comment somewhere (I've forgotten where) that aggregation loops are somehow special in typed/racket, perhaps due to the possibility of an empty list (even though this list can clearly never be empty), and require extra annotation, but the comment didn't actually say what to do.

Is there any tutorial which teaches how to read typed/racket error messages? Or can someone suggest a way to make for/sum work? I am lost here. Thanks!

1 Like
2

Agreed. I doubt a plain ‘client’ of Typed Racket can get this done.

The base-env file (prims.rkt) in the Typed Racket package unfortunately ‘hardwires’ 0 as a plain constant into the accumulator and that should be something that a TR programmer can specify as a base case. While 0 belongs to a number of types, it doesn’t belong to Flonum (and one could perhaps just add this).

You could fix this by modifying the file in racket/share/pkgs/typed-racket-lib/typed-racket/base-env/prims.rkt … or wait for one of the implementors to actually fix this issue.

1 Like
3

In this case, you can just use for/fold instead:

(for/fold : Flonum
  ([sum : Flonum 0.0])
  ([i : Integer (in-range 1000000)])
  (fl+ sum (flsqrt (->fl i))))
2 Likes
4

That’s what for/sum essentially expands to .. yes!

5

This isn't a fixable bug -- the 0 is there in the underlying #lang racket version and changing TR to do something different would change the semantics.

6

From what I could tell TR makes the choice to put the 0 into the general typed fold. This means that that the TR macro could come with an option to specify the identity elements of iterators so that the type works out. (Perhaps for/sum is the only one.)

7

Typed Racket re-implements the macro (so as to propagate type annotations) but it re-implements it to have the same behavior as for/sum from racket. If for/sum adds something for specifying the initial value then TR will follow that.

8

Thanks for reminding me of my design guideline :slight_smile:

(I have experimented with for/max and for/min which would need such neutral elements too. When I recover from Sw Dev, I may take a stab at that.)

9

Thanks! Both for the sample code, and letting me know I'm not crazy for missing an obvious for/sum solution.

Perhaps it would be worthwhile to make a note in the documentation that for/sum doesn't (and can't) match Racket semantics perfectly, like for flonums, and/or what to use instead? I see I'm not the first person to struggle with this.

Anyway, this typed/racket for/fold solution is longer (and less obvious), needs explicit type annotations, still requires racket/flonum wrapper functions, and the result here is 5x slower than standard Racket. So I think typed/racket is not the solution for me in this case.

10
  1. for/sum in Typed Racket does match Racket's semantics.
  2. When I time the following programs:
#lang typed/racket
(require racket/flonum)
(time
 (for/fold : Flonum
   ([sum : Flonum 0.0])
   ([i : Integer (in-range 1000000)])
   (fl+ sum (flsqrt (->fl i)))))

and

#lang racket
(time
 (for/sum ([i (in-range 1000000)])
   (sqrt i))

and

#lang racket
(require racket/flonum)
(time
 (for/sum ([i (in-range 1000000)])
   (flsqrt (->fl i)))

The TR program is about twice as fast as the Racket program using flsqrt and 25x faster than the Racket program with just sqrt.

11

Just to be very explicit, the differences between

and the semantics of for/sum are:

  1. The sum variable is initially 0, which is not a Flonum; and
  2. Therefore, the results have to be combined with +, not fl+.

The issue here is that you have annotated the result of for/sum as a Flonum, but the typechecker can't prove that the sequence is non-empty (that would need dependent types), so it can't prove that the result won't be 0.

Here is a working version:

#lang typed/racket
(require racket/flonum)
(for/sum : (U Zero Flonum) ([i 1000000])
  (flsqrt (->fl i)))

If you need to use the result as a Flonum, assert will do that with a minimum of runtime cost:

#lang typed/racket
(require racket/flonum)
(fl+ 1.0
     (assert (for/sum : (U Zero Flonum) ([i 1000000])
               (flsqrt (->fl i)))
             flonum?))

The assert expands to something like (if (flonum? x) x (error "not a Flonum")). While writing (cast x Flonum) would also work, cast in Typed Racket uses the contract system, which has a greater runtime cost: assert is generally preferable when its first-order check is sufficient.

I agree that this is a very confusing error message. I'm not familiar with the right parts of the Typed Racket implementation to know how to produce a better message, but it might mean an adjustment around here: