(Not experienced with typed racket) How about something like this, is there something bad about this?
(fxquotient (-> Fixnum Fixnum Fixnum)) (fixnum->byte (-> Fixnum Byte)) ;; possible runtime error (fixnum->byte (fxquotient rs n)) (I don't expect a type to always snap to the narrower one automatically... Or is that something typed racket actually tries to do [which would be cool], but this is something I am more likely to expect from a dependently typed language??) TL;DR does typed racket try to reason about math and or treat values as types? Sam Tobin-Hochstadt schrieb am Freitag, 16. April 2021 um 15:51:46 UTC+2: > 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/17e9a04a-1648-4c88-8e2e-70691ca0fd0dn%40googlegroups.com.
