typed-racket

typed-racket copied to clipboard

Observed:

scratch.rkt> (version)
- : String
"7.8"
scratch.rkt> (modulo 256 255)
- : Integer [more precisely: Byte]
1
scratch.rkt> (modulo 256 256)
- : Integer [more precisely: Index]
0

Expected:

scratch.rkt> (modulo 256 256)
- : Integer [more precisely: Byte]
0

Currently, modulo returns a Byte if the modulus is 255 or less, and an Integer if the modulus is 256 or more.

However, an integer mod 256 can be at most 255. The cutoff should reflect that: return a Byte if the modulus is 256 or less, and an Integer if the modulus is 257 or more.

Note that this is only relevant when the modulus is exactly 256. Below 256, (modulo) already returns a Byte; above 256, it is correct not to.

Apart from changing the type of modulo, we can use #:with-refinements to work around this:

#lang typed/racket/base #:with-refinements

(ann (modulo 1000 256) Byte)

@samth do you think we should change the corresponding case of the type of modulo to fix the problem without using #:with-refinements. That is, (-> Integer Byte Byte) to (-> Integer (U Byte 256) Byte))

That would work, and seems easy enough.