Typed Racket: type relations

[Dominik Pantůček]

Hello Racketeers,

working on gradually typing some of my modules I encountered an
interesting problem:

(define-type Color Fixnum)

(: argb-average (-> Color * Color))
(define (argb-average . argbs)
(let loop ((as : Fixnum 0)
(rs : Fixnum 0)
(gs : Fixnum 0)
(bs : Fixnum 0)
(n : Fixnum 0)
(argbs : (Listof Color) argbs))
(if (null? argbs)
(make-argb (fxquotient as n)
(fxquotient rs n)
(fxquotient gs n)
(fxquotient bs n))
(let-values (((a r g b) (argb-split (car argbs))))
(loop (fx+ as a)
(fx+ rs r)
(fx+ gs g)
(fx+ bs b)
(fx+ n 1)
(cdr argbs))))))

Type Checker: type mismatch
expected: Byte
given: Fixnum
in: (fxquotient bs n)

The only way of fixing this issue was using unsafe-fxquotient which is
unsafe-require/typed accordingly:

(unsafe-require/typed
racket/unsafe/ops
(unsafe-fxquotient (-> Fixnum Fixnum Byte)))

Is there a better way?

The relation between Byte and (Nonnegative-)Fixnum is mathematically
sound here, but making TR understand it is apparently pretty hard...


Cheers,
Dominik

[Sam Tobin-Hochstadt]

To improve this, we'd have to extend the type of `fxquotient`, which
is reasonable, but I'm not sure what the addition would be. In
particular, your addition is not sound:

(fxquotient 1024 2) produces 512 which is not a Byte.

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...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/608fdb93-b2ce-37e0-750c-037b47fed102%40trustica.cz.

[kamist...@gmail.com]

(Not experienced with typed racket) How about something like this, is there something bad about this?

(fxquotient (-> Fixnum Fixnum Fixnum))
(fixnum->byte (-> Fixnum Byte)) ;; possible runtime error

(fixnum->byte (fxquotient rs n))

(I don't expect a type to always snap to the narrower one automatically...

Or is that something typed racket actually tries to do [which would be cool], but this is something I am more likely to expect from a dependently typed language??)

TL;DR does typed racket try to reason about math and or treat values as types?

[Dominik Pantůček]

I wanted to polish things a bit before starting a longer discussion, but
here we go ;-)

The code in question[1] is part of my work into exchanging unsafe
modules which can be used either contracted or uncontracted for TR
modules. The goal is to replace racket/unsafe/ops with TR to provide
compile-time type consistency and to have modules which are internally
consistent and if they are used with other TR code the consistency
remains. More on that later.

On 16. 04. 21 15:51, Sam Tobin-Hochstadt wrote:
> To improve this, we'd have to extend the type of `fxquotient`, which
> is reasonable, but I'm not sure what the addition would be. In
> particular, your addition is not sound:
>
> (fxquotient 1024 2) produces 512 which is not a Byte.

Please, take a quick look at the typed-color.rkt in the repository.

The "Color" type is just a Nonnegative-Fixnum. It is a generic RGB value
with blue in lowest 8 bits, green shifted above blue and red on top. 24
bits in total. The split-rgb splits it into 3 R,G,B values - where each
of those values is a byte.

Then the rgb-average function takes an arbitrary number of Color values,
computes sums of their distinct R,G,B components and divides all of them
by the number of values before merging them together into one RGB Color
value.

Average value of (listof Byte) is definitely a Byte again. I am sorry I
didn't send the whole code in question. I was focused on other parts and
this is just a side issue in my current work.

Is there a way to express this in TR while still generating a code that
is on-par with the unsafe version? In theory, TR should excel in this.

A similar problem arises with the rgb-distance^2 function where the
component difference can be either positive or negative. But definitely
a square of whatever Integer is positive. And definitely the result
cannot be bigger than 3*255^2=195075, which is definitely
Nonnegative-Fixnum on any platform.

Again - is there a way to express this in TR and generate a code that
has no runtime checks?

The motivation here is that the performance and type soundness should go
hand in hand. If I prove the code will never get a value of a wrong
type, there is no need for runtime checks. Actually the more strict
rules, the better code can be (in theory) generated.

Then the typed/untyped boundaries introduce contracts - or they don't. I
am really confused, why there is a typed/untyped boundary between
typed-unsafe-color.rkt and typed-color.rkt. I assume this comes from my
poor understanding of TR - it will probably get better in the
forthcoming months as TR has proven to be an invaluable tool for
improving the quality of performance-oriented modules so far. More on
that later too...


Cheers,
Dominik

[1] https://gitlab.com/racketeer/typed-racket-performance

[Sam Tobin-Hochstadt]

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.

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))))

3. I don't see any boundaries where you describe -- can you say more?

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...@googlegroups.com.

> To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/d95b9140-fd78-0230-439b-aba654505fd0%40trustica.cz.

[Dominik Pantůček]

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

[Hendrik Boom]

On Sun, Apr 18, 2021 at 09:05:11AM +0200, Dominik Pantůček wrote:
...
...

>
> 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.

Reading the documentation you link to, it seems that the problem is that
(fx* x x) is not linear in x.
It says that it can reason only about linear expressions. This is a
quadratic form.

-- hendrik

...
...

[Sam Tobin-Hochstadt]

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

[Dominik Pantůček]

>>>
>>> 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

[Ben Greenman]

>>>> 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.

My hint turned into a PR and merged a few years ago.
https://github.com/racket/typed-racket/pull/657

Here's the output I see from `typed-performance.rkt` . I'm on a commit
from Jan 20. Does this look more like you'd expect?

```
---
typed: cpu time: 2990 real time: 3023 gc time: 65
unsafe: cpu time: 405 real time: 408 gc time: 5
typed, unsafe provided: cpu time: 692 real time: 697 gc time: 10
plain: cpu time: 748 real time: 752 gc time: 3
---
typed: cpu time: 2817 real time: 2825 gc time: 11
unsafe: cpu time: 414 real time: 417 gc time: 3
typed, unsafe provided: cpu time: 671 real time: 675 gc time: 4
plain: cpu time: 750 real time: 754 gc time: 5
===
---
typed: cpu time: 1678 real time: 1684 gc time: 0
unsafe: cpu time: 161 real time: 165 gc time: 0
typed, unsafe provided: cpu time: 175 real time: 178 gc time: 0
plain: cpu time: 180 real time: 184 gc time: 0
---
typed: cpu time: 1744 real time: 1755 gc time: 0
unsafe: cpu time: 165 real time: 168 gc time: 0
typed, unsafe provided: cpu time: 164 real time: 167 gc time: 0
plain: cpu time: 195 real time: 198 gc time: 0
```

[Dominik Pantůček]

>> Of course Ben's hint at unsafe-reprovide is something I'd like to
>> investigate.
>
> My hint turned into a PR and merged a few years ago.
> https://github.com/racket/typed-racket/pull/657
>

I read that one yesterday - it does not address the issue fully. I meant
the hint at really implementing full (unsafe-reprovide ...) form.

> Here's the output I see from `typed-performance.rkt` . I'm on a commit
> from Jan 20. Does this look more like you'd expect?
>
> ```
> ---
> typed: cpu time: 2990 real time: 3023 gc time: 65
> unsafe: cpu time: 405 real time: 408 gc time: 5
> typed, unsafe provided: cpu time: 692 real time: 697 gc time: 10
> plain: cpu time: 748 real time: 752 gc time: 3
> ---
> typed: cpu time: 2817 real time: 2825 gc time: 11
> unsafe: cpu time: 414 real time: 417 gc time: 3
> typed, unsafe provided: cpu time: 671 real time: 675 gc time: 4
> plain: cpu time: 750 real time: 754 gc time: 5
> ===
> ---
> typed: cpu time: 1678 real time: 1684 gc time: 0
> unsafe: cpu time: 161 real time: 165 gc time: 0
> typed, unsafe provided: cpu time: 175 real time: 178 gc time: 0
> plain: cpu time: 180 real time: 184 gc time: 0
> ---
> typed: cpu time: 1744 real time: 1755 gc time: 0
> unsafe: cpu time: 165 real time: 168 gc time: 0
> typed, unsafe provided: cpu time: 164 real time: 167 gc time: 0
> plain: cpu time: 195 real time: 198 gc time: 0
> ```
>

No, this is still "wrong".

I experimented a bit with re-providing renamed / copied bindings as
discussed in those two issues and the results are definitely much
better. Almost perfect:


```
===rgb-average
---
typed: cpu time: 62 real time: 62 gc time: 10
typed-orig: cpu time: 1275 real time: 1275 gc time: 9
unsafe: cpu time: 50 real time: 50 gc time: 0
typed, unsafe provided: cpu time: 271 real time: 271 gc time: 0
plain: cpu time: 416 real time: 416 gc time: 0
---
typed: cpu time: 54 real time: 54 gc time: 1
typed-orig: cpu time: 1273 real time: 1273 gc time: 2
unsafe: cpu time: 49 real time: 49 gc time: 0
typed, unsafe provided: cpu time: 271 real time: 271 gc time: 0
plain: cpu time: 414 real time: 414 gc time: 0
===rgb-distance^2
---
typed: cpu time: 672 real time: 672 gc time: 1
typed-orig: cpu time: 664 real time: 664 gc time: 1
unsafe: cpu time: 12 real time: 12 gc time: 0
typed, unsafe provided: cpu time: 13 real time: 13 gc time: 0
plain: cpu time: 13 real time: 13 gc time: 0
---
typed: cpu time: 676 real time: 676 gc time: 1
typed-orig: cpu time: 664 real time: 664 gc time: 1
unsafe: cpu time: 13 real time: 13 gc time: 0
typed, unsafe provided: cpu time: 13 real time: 13 gc time: 0
plain: cpu time: 13 real time: 13 gc time: 0
```

Now the "typed" version of "rgb-average" is almost on par with usafe
one. I re-provided only rgb-average, I left rgb-distance intact. Also I
optimized it a bit (basically restructured the way the bindings are
introduced in the loop) and that helped a lot. But now...

Why is the re-provided through rename of copied binding (typed) 5 times
faster than the one which is unsafe-provide'd (typed, unsafe provided)
directly? I must be overlooking something.


Cheers,
Dominik

[Sam Tobin-Hochstadt]

It's a little more complicated than that -- the _constraints_ have to
be linear -- that is, the expressions in the refinements, but the
expressions reasoned about can be more general. However, it doesn't do
very much useful with multiplication by bounded values at the moment.

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...@googlegroups.com.

> To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/20210419113103.c4fupxvl6ieb3uub%40topoi.pooq.com.

[Sam Tobin-Hochstadt]

On Mon, Apr 19, 2021 at 3:19 PM Dominik Pantůček
<dominik....@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