To improve this, we'd have to extend the type of `fxquotient`, which is reasonable, but I'm not sure what the addition would be. In particular, your addition is not sound:
(fxquotient 1024 2) produces 512 which is not a Byte. Sam On Thu, Apr 15, 2021 at 6:22 PM Dominik Pantůček <[email protected]> wrote: > > Hello Racketeers, > > working on gradually typing some of my modules I encountered an > interesting problem: > > (define-type Color Fixnum) > > (: argb-average (-> Color * Color)) > (define (argb-average . argbs) > (let loop ((as : Fixnum 0) > (rs : Fixnum 0) > (gs : Fixnum 0) > (bs : Fixnum 0) > (n : Fixnum 0) > (argbs : (Listof Color) argbs)) > (if (null? argbs) > (make-argb (fxquotient as n) > (fxquotient rs n) > (fxquotient gs n) > (fxquotient bs n)) > (let-values (((a r g b) (argb-split (car argbs)))) > (loop (fx+ as a) > (fx+ rs r) > (fx+ gs g) > (fx+ bs b) > (fx+ n 1) > (cdr argbs)))))) > > Type Checker: type mismatch > expected: Byte > given: Fixnum > in: (fxquotient bs n) > > The only way of fixing this issue was using unsafe-fxquotient which is > unsafe-require/typed accordingly: > > (unsafe-require/typed > racket/unsafe/ops > (unsafe-fxquotient (-> Fixnum Fixnum Byte))) > > Is there a better way? > > The relation between Byte and (Nonnegative-)Fixnum is mathematically > sound here, but making TR understand it is apparently pretty hard... > > > Cheers, > Dominik > > -- > You received this message because you are subscribed to the Google Groups > "Racket Users" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/racket-users/608fdb93-b2ce-37e0-750c-037b47fed102%40trustica.cz. -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/CAK%3DHD%2BY3JuW%3DN9paE-n5mm51E1qSde1ZCEa5xuxPE7H1_WPXWA%40mail.gmail.com.
