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.
