On Sun, Apr 18, 2021 at 3:05 AM Dominik Pantůček <[email protected]> wrote: > > 0. Thank you very much for looking into this. > > On 18. 04. 21 4:57, Sam Tobin-Hochstadt wrote: > > 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. > > That is what I was afraid of. Mathematically speaking, the proof is > almost trivial. But expressing that turned out to be a tough nut to crack. > > I looked into base-env-numeric.rkt and I see that there is quite some > type reasoning already implemented. And it works great for simple cases > like (fxand 255 anything) - : Byte. > > Maybe adding an explicitly ranged Integer type and after reasoning about > the result match the final range against the set of coarse-grained types > could be a solution? Albeit not a trivial one in terms of implementing it. > > > > > 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)))) > > This is exactly what I was looking at (and for), but I am unable to use > it correctly:
I think you need to add #:with-refinements after the #lang line. > > 3. I don't see any boundaries where you describe -- can you say more? > > Run typed-performance.rkt and see: This might be related to https://github.com/racket/typed-racket/issues/289. Sam -- 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%2BYGgTbFjyaTQ8ETuXmRB4%2BsYoW7iYAujjWcFa0FNHEdrg%40mail.gmail.com.
