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: (define-type PMByte (Refine [v : Fixnum] (and (< v 256) (< -256 v)))) (: rgb-distance^2 (-> Color Color Nonnegative-Fixnum)) (define (rgb-distance^2 c1 c2) (define-values (r1 g1 b1) (split-rgb c1)) (define-values (r2 g2 b2) (split-rgb c2)) (define rd : PMByte (fx- r2 r1)) (define gd : PMByte (fx- g2 g1)) (define bd : PMByte (fx- b2 b1)) (unsafe-fx+ (fx* rd rd) (fx* gd gd) (fx* bd bd))) typed-color.rkt:61:24: Type Checker: type mismatch expected: PMByte given: Fixnum in: (fx- g2 g1) context...: /usr/share/racket/pkgs/typed-racket-lib/typed-racket/utils/tc-utils.rkt:123:0: report-all-errors /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt:376:0: type-check /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt:619:0: tc-module /usr/share/racket/pkgs/typed-racket-lib/typed-racket/tc-setup.rkt:96:12: temp34 /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typed-racket.rkt:23:4 I would really like to be able to reason about the Integer bounds (and therefore signs) dynamically. So that when you have something like: (: square (-> Fixnum Nonnegative-Fixnum)) (define (square x) (fx* x x)) You will get something better than: multiplication.rkt:7:2: Type Checker: type mismatch expected: Nonnegative-Fixnum given: Fixnum in: (fx* x x) I will look into the refinements implementation to see what are the current limits and what the future possibilities might be. > > 3. I don't see any boundaries where you describe -- can you say more? Run typed-performance.rkt and see: typed: cpu time: 1347 real time: 1347 gc time: 3 typed-orig: cpu time: 1367 real time: 1367 gc time: 3 unsafe: cpu time: 54 real time: 54 gc time: 1 typed, unsafe provided: cpu time: 292 real time: 292 gc time: 0 plain: cpu time: 436 real time: 436 gc time: 1 The "typed" and "typed-orig" are the same. But the "typed" and "typed, unsafe provided" should be the same and only "typed-orig" should enforce contracts. The typed-unsafe-color.rkt just does: (unsafe-provide (all-from-out "typed-color.rkt")) Which was my attempt at re-providing typed procedures without contracts. 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/fe6b4c71-398f-efe0-ce93-59048faa4fe7%40trustica.cz.
