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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/fe6b4c71-398f-efe0-ce93-59048faa4fe7%40trustica.cz.
