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 On Mon, Apr 19, 2021 at 7:31 AM Hendrik Boom <hend...@topoi.pooq.com> wrote: > > 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 > > ... > ... > > -- > 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/20210419113103.c4fupxvl6ieb3uub%40topoi.pooq.com. -- 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%2Bbi1VmQ0zt5RnCnqSojvyzoBA%3D-WMN9CxSun-g1bv%3DJGw%40mail.gmail.com.
