Ok, three parts: 1. Is it possible to make `average` on `Byte` provably produce a `Byte`? This is not going to be possible with plain Typed Racket, even with refinements to the numeric tower. The problem is that maintaining the invariant that a <= (* n 255) is not something that we can express just with the sets of values Typed Racket reasons about.
2. The rgb-distance^2 issue is really just that there's no negative counterpart to `Byte`, so `Byte` minus `Byte` is `Fixnum`. We could add that, at the cost of extra complexity in the numeric tower generally. However, I would suggest that the right fix here is to use refinement types, and specify exactly what you want. Unfortunately, the refinement types feature (good intro here: https://blog.racket-lang.org/2017/11/adding-refinement-types.html) isn't quite able to prove everything you want, but that's the direction we should go. For example, it can already prove that rd in the rgb-distance^2 function has this type: (define-type PMByte (Refine [v : Fixnum] (and (< v 256) (< -256 v)))) 3. I don't see any boundaries where you describe -- can you say more? Sam On Fri, Apr 16, 2021 at 12:06 PM Dominik Pantůček <[email protected]> wrote: > > 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 [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/racket-users/d95b9140-fd78-0230-439b-aba654505fd0%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%2BZ_6fqz3pcXNC0Jm-aG1__zvruHgDz_w0xSVuh1R1pY7w%40mail.gmail.com.
