>>> >>> 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? 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. Funny thing is that even trying to verify my color-blending code with TR helped me improve that code - quite to my surprise. The original idea was to start with lighting code (intensity, falloff, colored light) and then proceed on to more complex parts (something like what I tried with verifying the unsafe-structs usage). And it turned out that even that was a bit too much so I had to go down to the color handling code. I am afraid that at the moment TR cannot replace contracts in my design process. That is a pity - because although I mostly do "design by contract", it is NOT verification. So sometimes I have to run hoops thru loops to make the program fail on particular contract to see what is wrong. With TR my aim is to shift this effort from runtime to compile (or more precisely design) time. Still it is awesome tool for both code profiling and proving correctness of individual modules. > >>> 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. > So basically my unsafe-reprovide module should probably use some syntax trickery to generate new bindings for all typed provides it requires and re-provide them unsafely renaming them back to original name? I think I can do something like that using relatively simple syntax macro. Do I understand it correctly? Of course Ben's hint at unsafe-reprovide is something I'd like to investigate. Cheers, Dominik -- 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/af71d1d3-6246-bcae-31ba-be2b064baba7%40trustica.cz.
