Extend Refinement Types to Support Real-Number Constraints

[uyweywe]

Description:
Typed Racket's refinement types (Refine) are currently limited to linear integer constraints (e.g., <=, and, or on integer linear combinations). This restriction prevents expressing essential real-number constraints, such as non-zero denominators or real-valued ranges, hindering type safety in numerical computations.

Example Failure:

(define-type NonzeroReal (Refine [r : Real] (not (= r 0))))  ; ❌ Type checker error
(: safe-div (-> Real NonzeroReal Real))
(define (safe-div x y)
  (/ x y))

Proposal:
Extend the Refine type to support real-number equality and inequality constraints (e.g., (not (= r 0)), (< a b), (<= c 1.0)). This enhancement would:

1. Enable type-safe checks for non-zero reals and bounded ranges.
2. Enhance expressiveness for real-valued domains while preserving type safety.

Requested Features:

• Support for real-number predicates in Refine, including equality (=), inequality (<, >, <=, >=), and logical combinations (and, or, not).

[samth]

This would be nice to have, but we would need a solver for such constraints. Right now refinements use a simple Fourier-Motzkin Elimination-based solver. What would you propose for reals?

[uyweywe]

This would be nice to have, but we would need a solver for such constraints. Right now refinements use a simple Fourier-Motzkin Elimination-based solver. What would you propose for reals?

I don't know very much about solvers,but a similar project using z3 or cvc4. And here is the link: https://ucsd-progsys.github.io/liquidhaskell/

[samth]

Those systems do provide some real number handling, but (a) that's a very large dependency to add and (b) the handling of reals is far from complete (for fundamental undecidability reasons).

[uyweywe]

Those systems do provide some real number handling, but (a) that's a very large dependency to add and (b) the handling of reals is far from complete (for fundamental undecidability reasons).

So could it be easier to handle only rational numbers? Or is it possible to use the previous solver, although it is slow and only works for linear inequalities?

[uyweywe]

Those systems do provide some real number handling, but (a) that's a very large dependency to add and (b) the handling of reals is far from complete (for fundamental undecidability reasons).

I’ve done some research and found that solving nonlinear inequality systems seems quite challenging. So, could we first extend the types from integers to real numbers and directly use the Fourier-Motzkin Elimination algorithm? Although it can only solve linear inequality systems, extending it to the real number range is also very useful.

[samth]

That would be a nice addition. I'd be happy to review a patch, or provide guidance on what to work on, to add that. At the moment I'm not likely to work on it myself soon.