On Sun, Apr 18, 2021 at 3:05 AM Dominik Pantůček <dominik.pantu...@trustica.cz> 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 racket-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/CAK%3DHD%2BYGgTbFjyaTQ8ETuXmRB4%2BsYoW7iYAujjWcFa0FNHEdrg%40mail.gmail.com.
