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 <dominik.pantu...@trustica.cz> 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 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. -- 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/CAK%3DHD%2BZ_6fqz3pcXNC0Jm-aG1__zvruHgDz_w0xSVuh1R1pY7w%40mail.gmail.com.
