[racket] weird behavior with in-range in typed racket

[Alexander D. Knauth]

This program:
#lang typed/racket
(define n : Real 5)
(for/list ([i : Natural (in-range n)]) : (Listof Natural)
i)
And this program:
#lang typed/racket
(define n : Real 5)
(for/list ([i : Natural (identity (in-range n))]) : (Listof Natural)
i)
The first one produces an error:
. Type Checker: type mismatch
expected: Nonnegative-Integer
given: Integer in: (for/list ((i : Natural (in-range n))) : (Listof Natural) i)
The second one works fine:
'(0 1 2 3 4)
But why does the first one produce integer, but wrapping it in identity make it produce Nonnegative-Integer (Natural) ?



____________________
Racket Users list:
http://lists.racket-lang.org/users

[Alexis King]

This is because Racket’s for loops special-case on in-range, in-list, in-vector, etc. They do this for performance reasons—no need to check the type at runtime. This is probably redundant in a typed context, anyway, though, since the typechecker should be able to (ideally) make those optimizations itself.

Anyway, it looks like the TR expansion of for loops doesn’t account for the (rather large) type of in-range. I think Asumu’s rewriting the loops in TR, though—perhaps this will be fixed then?

Post by Alexander D. Knauth
#lang typed/racket
(define n : Real 5)
(for/list ([i : Natural (in-range n)]) : (Listof Natural)
i)
#lang typed/racket
(define n : Real 5)
(for/list ([i : Natural (identity (in-range n))]) : (Listof Natural)
i)
. Type Checker: type mismatch
expected: Nonnegative-Integer
given: Integer in: (for/list ((i : Natural (in-range n))) : (Listof Natural) i)
'(0 1 2 3 4)
But why does the first one produce integer, but wrapping it in identity make it produce Nonnegative-Integer (Natural) ?
____________________
http://lists.racket-lang.org/users

[Asumu Takikawa]

Anyway, it looks like the TR expansion of for loops doesn’t account for
the (rather large) type of in-range. I think Asumu’s rewriting the loops
in TR, though—perhaps this will be fixed then?

I have a semi-working rewrite of the for loops, but I don't want to get
people's hopes up quite yet because I'm not sure it's the right
approach.

More specifically, since it involves re-writing the `for` macros and
then doing a custom typechecking pass afterwards, it means that the
optimizer can't work straightforwardly on the expansion. (i.e., the
optimizer would need special casing for `for` too)

Also, it's probably not quite sound because it doesn't account for
custom sequence syntax defined via `define-sequence-syntax` in that it
assumes the expr form and the clause forms will typecheck to the same
thing (which does not hold in general).

It might be better to just coax the expansion more to be type-checkable
or maybe to improve type inference.

Cheers,
Asumu
____________________
Racket Users list: