(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 > <dominik....@trustica.cz> 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 racket-users...@googlegroups.com. > > 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 racket-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/17e9a04a-1648-4c88-8e2e-70691ca0fd0dn%40googlegroups.com.
