search

tonyday567 / numhask

A haskell numeric prelude, providing a clean structure for numbers and operations that combine them.
Other
68 stars 15 forks source link

Are the context constraints on Monus & Addus valid? #176

Open benhutchison opened 8 months ago

benhutchison commented 8 months ago

With the disclaimer that all this is pretty picky hair-splitting... 😼

I was skeptical about the default definition in Monus and Addus; specifically how they require distinct contexts BoundedJoinSemiLattice and MeetSemiLattice. There's nothing that requires these semilattices be compatible or related by any laws right?

I could use a vanilla BoundedJoinSemiLattice with join=min and bottom=0. But a MeetSemiLattice could define meet=min and be completely lawful. In which case a ∸ b will typically below the lower bound of the semilattice, which I dont think was the intention?

I dont think join and meet have, mathematically, a well-founded meaning WRT each other until they're put into the same lattice. That's why they often say join and meet are interchangeable terms when talking about the operation of a semilattice.

tldr I think the definition needs a lattice constraint rather than 2 semilattices.

  (∸) :: a -> a -> a
  default (∸) :: (BoundedJoinSemiLattice a, MeetSemiLattice a, Subtractive a) => a -> a -> a
  a ∸ b = bottom /\ (a - b)

https://github.com/tonyday567/numhask/blob/main/src/NumHask/Data/Positive.hs#L163-L164

tonyday567 commented 7 months ago

I think you're right.

I thought about the type synonym:

type LowerBoundedLattice a = (Lattice a, BoundedJoinSemiLattice a)

But I'm conscious of the exploding mess you get if you go for fine-grained classes. Class trees can become such a mess in Haskell, if you try to exactly match and types and laws. A JoinSemiLattice is both a super class of Lattice and a constraining class of BoundedJoinSemiLattice. By going with the "other" split - into BoundedJoinSemiLattice and MeetSemiLattice, it morally drops the absorption laws.

So this is the correct version?

(∸) :: a -> a -> a
  default (∸) :: (Lattice a, BoundedJoinSemiLattice a, Subtractive a) => a -> a -> a
  a ∸ b = bottom /\ (a - b)

BoundedJoinSemiLattice is a mouthful. Next major, it might be better renamed as LowerBounded.

benhutchison commented 7 months ago

I was surprised Wikipedia doesn't mention {Lower,Upper}BoundedLattice as things and asked here. My question was closed (put that down to some stack exchange maths subculture) but, as the comment notes, they are valid concepts and he gives some examples.

That said, defining a pair of incoherent semilattices would be a very odd thing to do in Haskell, so I think this is more of conceptual interest than a likely source of user bugs 😼