Would a Monus class allow defining a Quotient Semifield over non-negative numbers?

[benhutchison]

I, a self-described rusted-on Scala programmer, spent today studying (er.. admiring) NumHask for inspiration. We don't have anything as nice or as principled in Scala.

Spire is the closest thing and quite praiseworthy. Nonetheless, NumHask is considerably more principled in some areas, one being the definition of rounding functions in QuotientField. Spire puts these in an IsReal type class that IsRealy as lawless as the wild west.

But one aspect of QuotientField that troubles me is the Subtractive requirement, via Field, which implies that to support round/floor/ceiling, a number system must admit negative numbers. That clashes with my real-world common sense that says that we ought to be able to sensibly define round/floor/ceiling on non-negative rationals, naturals etc.

Possibly, a QuotientSemifield built on top of Semifield + Monus (truncating subtraction) is an answer. I suspect there's an abstraction there that can be lawfully defined on a closed set of non-negative numbers.

I also think Monus itself is useful for safely decreasing Magnitudes generally without straying outside the positive domain.

[tonyday567]

Thanks for your interest and kind words. We don't have anything as principled in Haskell either! Sadly, the Num, Rational, Real and friends are baked into the prelude, and this make it very difficult to shift habits.

I also think Monus itself is useful for safely decreasing Magnitudes generally without straying outside the positive domain.

Yes, and I also agree that Subtraction as a constraint of QuotientField is a wart.

Presaging both of these is defining Positive - the closed set of non-negative numbers as you say. In Haskell, there's always the unwrapping and wrapping of newtypes that gets in the way of something such as this. You're working with a double, take the magnitude, and some fancy library wraps the answer in a newtype Positive that you then have to unwrap etc etc.

instance Basis Double where
  type Mag Double = Double
  type Base Double = Double
  magnitude = P.abs
  basis = P.signum

You could put the Mag type as an extra parameter to Basis (moving away form TypeFamilies), but then the user invariably has to write Basis Double Double or Basis Double Positive everywhere when the constraints don't get resolved.

Back to Monus, I think the major design decisions would be:

• Whether to use the Maybe type or zero for a - b if a < b. It comes down to how useful it is to distinguish Nothing and Maybe zero (ie a == b)
• Whether to define truncated subtraction, or go for a whole suite of truncated arithmetic, and abstract the Positive type to a more general (open or closed) "Interval" type.
• Whether to define neginfinity as zero

[benhutchison]

I really like your Basis abstraction, splitting a directed quantity (a vector - signed numbers are just 1D vectors to me) into its direction and magnitude according to some basis/reference. Feels very right to me.

But this begs the question, how to work with the magnitude, which is always non-negative. NumHask feels a bit incomplete atm in that it doesnt have a complete toolkit for closed arithmetic on the magnitudes. Monus & MSemiring (?) feel like a nice answer here.

re " abstract the Positive type to a more general (open or closed) "Interval" type", there's a few intervals that seem perennially useful:

• [0, inf) : non-negative
• [0 + eps, inf) : positive qty, safe denominator
• [0, 1] : probability, fraction, weights
• [1, inf) : growth coefficient
  Aliases or specialised operators for some of these might be valuable if you go for a more general interval approach

[tonyday567]

Apologies for going ahead and getting some code laid. I found I couldn't think about it without something concrete.

[benhutchison]

Beautiful seeing the maths come to life, and so elegantly. Gave me Haskell envy just reading it. MSemifield is certainly a thing now, there's an executable existence proof..

[tonyday567]

Sitting on this for a bit.

I feel like saying that 4 - 7 = 0, which is the basic formulation of monus is problematic, as in it creates more potential for bugs than it solves.

Saying 4 - 7 = Nothing or 4 - 7 = error are also problematic.

[tonyday567]

#175

After a bit more tweaking, QuotientField doesn't need Monus at all for a good Positive instance.

This leaves Monus floating around a bit, prior to working out if it can be integrated with Basis. Until then saying 4 ∸ 7 might allay my concerns that it could be misinterpreted.

[benhutchison]

My interpretation is that in common language, when talking about "subtraction" of non negative quantities, we actually mean monus, not minus, but don't bother to distinguish. So I'm for treating it as a separate operation.

…

On Sun, 31 Dec 2023, 4:21 pm Tony Day, ***@***.***> wrote: #175 <#175> After a bit more tweaking, QuotientField doesn't need Monus at all for a good Positive instance. This leaves Monus floating around a bit, prior to working out if it can be integrated with Basis. Until then saying 4 ∸ 7 might allay my concerns that it could be misinterpreted. — Reply to this email directly, view it on GitHub <#173 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAAXJZDKD4CL3SYCCJANLBDYMDY5RAVCNFSM6AAAAAA7A5R3FGVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTQNZSGY3TIMRWGM> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[benhutchison]

So I finally found time to go through #175 and understand how you built a quotient field off a semifield.

I have one question.

round takes an additional Subtractive constraint that means it couldn't be used in a strictly positive context. Understandably since negative numbers round away from zero.

I feel like a variant of round that rounds towards zero/smaller magnitude (like truncate) would be useful for rounding positive numbers? Can that be defined without needing Subtractive a?

[tonyday567]

That is a default signature, and the implementation for Positive overrides this, here: https://github.com/tonyday567/numhask/blob/ghc-9.8.1/src/NumHask/Data/Positive.hs#L100

I tried to wrangle the subtractive out of the default but it really does need the negate.

[benhutchison]

That is a default signature, and the implementation for Positive overrides this, here: https://github.com/tonyday567/numhask/blob/ghc-9.8.1/src/NumHask/Data/Positive.hs#L100/

Got it. Thanks for explaining.

As a Scala native, I didn't understand how DefaultSignatures works and that the default method can include more constraints than explicitly provided methods. Now I'm actually curious/doubtful if such is possible in Scala, where TCs are modelled as implicitly passed traits, and instances as trait implementations.. 🤔

[tonyday567]

It tends to work in practice and becomes very comfortable. Just part of the ghc api, I suppose.

I might merge this and do a major bump.

[benhutchison]

I feel like a variant of round that rounds towards zero/smaller magnitude (like truncate) would be useful

I was thinking and reading on this a little more. I do think semantically there's a distinction between rounding down (towards negative infinity) vs rounding towards zero. And it may be worth a separately named method on QuotientField like eg roundZero.

For Positive they will do the same thing. But for negative numbers, they behave differently. Essentially, roundZero would be to truncate as round is to floor

PS

• I suppose for completeness this suggests there's a variant of ceiling that moves away from zero.
• The not-towards-zero way of rounding relates to Basis. When we round "up" to inf vs "down" towards negative inf, do we actually mean along vs against the Basis? If the basis strangely pointed at neg inf, then rounding down ought to move towards +inf, I guess..
• Alas https://en.wikipedia.org/wiki/Rounding didn't suggest any succinct names as nice as truncate.