[Haskell-cafe] naturally, length :: a -> Int

[Henning Thielemann]

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.