
On Fri, 2021-03-05 at 20:03 -0600, Zemyla wrote:
You're looking for Ratio Natural.
On Wed, Mar 3, 2021, 09:20 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?
How stupid of me not to think of Ratio Natural. I should have phrased my question more precisely: Are there types that by construction (not only morally) permit only certain subsets of real numbers with reasonably efficient arithmetical operations? A naive way to represent rationals between 0 and 1 would be as newtype Part = Part !Natural !Natural with semantics \(Part a b) -> a % (a+b) Then (*) is easy to implement. \x -> 1-x is O(1) but arithmetic mean is more complicated. I have a proof-of-concept. If there is general interest in Rationals between 0 and 1 I could turn it into a small package, provided no other implementation exists. Olaf