On Wed, 3 Mar 2021, Olaf Klinke wrote:
While we're at it: Can there be a Fractional type permitting only positive numbers, as the positive real numbers are closed under division? Can there be a type of rationals between 0 and 1 (which is closed under multiplication) where (/x) is the right adjoint to (*x)?
Once I defined a wrapper for numbers that (morally) restricts the value range to non-negative values: http://hackage.haskell.org/package/non-negative However, it turned out to be impractical. It is incompatible with its base number type. If you have even more variants for positive numbers, for numbers in the range [0,1] you will do more conversions than computations. I found the LiquidHaskell approach convincing: You have a base type and add constraints on the value range. You could assign a [0,1]-value to a non-negative value without conversion, because LiquidHaskell would ask Z3 and Z3 would confirm that a [0,1]-value is always non-negative.