On Mon, Apr 19, 2021 at 3:19 PM Dominik Pantůček <dominik.pantu...@trustica.cz> wrote: > > >>> > >>> 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. > > Awesome! Now TR can properly reason about the differences. > > I guess it is not possible to make TR deduce the proper type of (* rd > rd) like: > > (define-type Byte^2 (Refine [v : Fixnum] (and (>= v 0) (< v (* 255 255))))) > > Are there any plans of adding such reasoning?
I'm not currently working on this, but I'd be happy to help out if you want to take this on. The relevant code is here: https://github.com/racket/typed-racket/blob/master/typed-racket-lib/typed-racket/typecheck/integer-refinements.rkt#L129-L143. The problem is that the spec of * is basically to create a linear expression precisely describing the result, and then say that the result is equal to that. But such a linear expression doesn't exist for *, of course. So you'd have to have a different strategy then (that's when `(Object? product-obj?)` is #f). > Honestly, when I went through the code for binary fx... operations I > realized that making them variadic is possible but not straightforward > at all. Without digging deeper it seems to me that it is actually a lot > of work. I will look into it again later on. Here's a first step, which might help get you started: https://github.com/samth/typed-racket/commit/2514e7107b4da5322a07fe260123432f4055 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%2Ba2P_rDZYD_13U4_nifiALycxKOYxfTcJXOVgZqnekJmA%40mail.gmail.com.
