I wanted to polish things a bit before starting a longer discussion, but here we go ;-)
The code in question[1] is part of my work into exchanging unsafe modules which can be used either contracted or uncontracted for TR modules. The goal is to replace racket/unsafe/ops with TR to provide compile-time type consistency and to have modules which are internally consistent and if they are used with other TR code the consistency remains. More on that later. On 16. 04. 21 15:51, Sam Tobin-Hochstadt wrote: > 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. Please, take a quick look at the typed-color.rkt in the repository. The "Color" type is just a Nonnegative-Fixnum. It is a generic RGB value with blue in lowest 8 bits, green shifted above blue and red on top. 24 bits in total. The split-rgb splits it into 3 R,G,B values - where each of those values is a byte. Then the rgb-average function takes an arbitrary number of Color values, computes sums of their distinct R,G,B components and divides all of them by the number of values before merging them together into one RGB Color value. Average value of (listof Byte) is definitely a Byte again. I am sorry I didn't send the whole code in question. I was focused on other parts and this is just a side issue in my current work. Is there a way to express this in TR while still generating a code that is on-par with the unsafe version? In theory, TR should excel in this. A similar problem arises with the rgb-distance^2 function where the component difference can be either positive or negative. But definitely a square of whatever Integer is positive. And definitely the result cannot be bigger than 3*255^2=195075, which is definitely Nonnegative-Fixnum on any platform. Again - is there a way to express this in TR and generate a code that has no runtime checks? The motivation here is that the performance and type soundness should go hand in hand. If I prove the code will never get a value of a wrong type, there is no need for runtime checks. Actually the more strict rules, the better code can be (in theory) generated. Then the typed/untyped boundaries introduce contracts - or they don't. I am really confused, why there is a typed/untyped boundary between typed-unsafe-color.rkt and typed-color.rkt. I assume this comes from my poor understanding of TR - it will probably get better in the forthcoming months as TR has proven to be an invaluable tool for improving the quality of performance-oriented modules so far. More on that later too... Cheers, Dominik [1] https://gitlab.com/racketeer/typed-racket-performance -- 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/d95b9140-fd78-0230-439b-aba654505fd0%40trustica.cz.