typed-racket

typed-racket copied to clipboard

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