Consider splitting the Semiring class?
sharkdp opened this issue · 28 comments
Here is the current definition of the Semiring typeclass and the definition of + and *:
class Semiring a where
add :: a -> a -> a
zero :: a
mul :: a -> a -> a
one :: a
infixl 6 add as +
infixl 7 mul as *It would be nice if I could use the + operator from the Prelude for (numerical) types that are commutative monoids under addition but not full semirings (because multiplication is not defined, for example). Correspondingly, I'd like to use the * operator for (numerical) types that are monoids under multiplication, but do not form a full semiring.
The ideal solution (in my point of view) would be a hierarchy where Monoid and some Abelian version like Monoid <= CommutativeMonoid could be used to define the Semiring class. Obviously, this does not work because one would need to define two conflicting Semiring and Monoid instances for each Semiring.
Would something like the following work? Obviously, it is not very pretty...
-- | A class for numerical types that form commutative monoids under addition.
-- |
-- | Instances must satisfy the following laws:
-- |
-- | - Associativity: `(a + b) + c = a + (b + c)`
-- | - Identity: `zero + a = a + zero = a`
-- | - Commutative: `a + b = b + a`
class AdditionMonoid a where
add :: a -> a -> a
zero :: a
infixl 6 add as +
-- | A class for numerical types that form monoids under multiplication.
-- |
-- | Instances must satisfy the following laws:
-- |
-- | - Associativity: `(a * b) * c = a * (b * c)`
-- | - Identity: `one * a = a * one = a`
class MultiplicationMonoid a where
mul :: a -> a -> a
one :: a
infixl 7 mul as *
-- | The `Semiring` class is for types that support an addition and
-- | multiplication operation.
-- |
-- | Instances must satisfy the following laws:
-- |
-- | - Multiplication distributes over addition:
-- | - Left distributivity: `a * (b + c) = (a * b) + (a * c)`
-- | - Right distributivity: `(a + b) * c = (a * c) + (b * c)`
-- | - Annihiliation: `zero * a = a * zero = zero`
class (AdditionMonoid a, MultiplicationMonoid a) <= Semiring aAny thoughts?
It would work, but I think we'd decided we didn't want to make the Prelude classes "overly" granular, and this probably falls into that (though of course the level that is considered overly probably differs from person to person). It's why we just have HeytingAlgebra => BooleanAlgebra too, rather than having lattices, posets, etc. in the hierarchy also.
You've also encountered the problem here of how best to approach a granular hierarchy, in that there are many ways of representing the same thing, or there are overlapping concerns where different operators have the same behaviour up to a point, leaving the choice of whether to make them instances of Semigroup and Monoid somewhat arbitrary (or having multiple different versions of the same thing - in the case of varieties of monoid that roll up multiple laws into one).
If there was an unambigious way that we could do this, and we had default superclass instances, then I'd probably be in favour 😉 but I think what we have for now this is probably the finest grained hierarchy the Prelude will provide.
To solve the problem you have, I'd suggest using Monoid (or an extended version of it for CommutativeMonoid, AbelianGroup if the additional laws are necessary) and defining those for your types - since you're only after using them for one type or the other anyway. Some newtyping may be required if you want to use the same type for both - like we have with the Additive and Multiplicative newtypes in purescript-monoid.
Can you give some examples of the types you have in mind? I'm unable to think of anything which is a commutative monoid under addition but does not have multiplication defined (can't multiplication be defined in terms of addition?), or anything that forms a monoid under multiplication but is not a semiring.
It would work, but I think we'd decided we didn't want to make the Prelude classes "overly" granular, and this probably falls into that (though of course the level that is considered overly probably differs from person to person). It's why we just have HeytingAlgebra => BooleanAlgebra too, rather than having lattices, posets, etc. in the hierarchy also.
Thank you for the explanation. I wasn't aware of that.
You've also encountered the problem here of how best to approach a granular hierarchy, in that there are many ways of representing the same thing, or there are overlapping concerns where different operators have the same behaviour up to a point, leaving the choice of whether to make them instances of Semigroup and Monoid somewhat arbitrary (or having multiple different versions of the same thing - in the case of varieties of monoid that roll up multiple laws into one).
If there was an unambigious way that we could do this, and we had default superclass instances, then I'd probably be in favour but I think what we have for now this is probably the finest grained hierarchy the Prelude will provide.
Alright. Thanks for the reference to default superclass instances. That sounds interesting.
To solve the problem you have, I'd suggest using Monoid (or an extended version of it for CommutativeMonoid, AbelianGroup if the additional laws are necessary) and defining those for your types - since you're only after using them for one type or the other anyway. Some newtyping may be required if you want to use the same type for both - like we have with the Additive and Multiplicative newtypes in purescript-monoid.
Yes, thanks. That's what I did so far (simply defined a Monoid instance, which leaves me with <>).
In the end, this is not something that's particularly important. I only liked the aesthetics of it because
class (AdditionMonoid a, MultiplicationMonoid a) <= Semiring ais pretty close to the mathematical definition... "a semiring R is a set ... such that (R, +) is a commutative monoid and (R, *) is a monoid ... (plus additional laws)".
... and I wanted to use * instead of <>, but I can live with that 😄.
Can you give some examples of the types you have in mind? I'm unable to think of anything which is a commutative monoid under addition but does not have multiplication defined (can't multiplication be defined in terms of addition?), or anything that forms a monoid under multiplication but is not a semiring.
For example: vectors form a commutative monoid under addition but there is no multiplication operation in general (scalar multiplication has the wrong domain and the cross product in 3D has no identity element).
The particular example I am interested in is physical units. They form a (commutative) monoid under multiplication but addition is not defined in general.
I would probably add a CommutativeMonoid subclass of Monoid in that case, in purescript-monoids. Many of our existing newtypes would have instances too.
Alright, I'll close this then.
@hdgarrood Do these examples make sense?
Yeah, your examples make sense, thanks :) I agree that it would be nice to be able to use + and * for these operations, but I also like that + and * have a precise meaning arising from how they interact with each other in PureScript, because of the Semiring laws, which I think we'd lose by splitting up Semiring like this.
I think it might be good to have a VectorSpace class in a library, maybe VectorSpace (v :: * -> *) where the type parameter for v is the type of the field (scalars), or perhaps VectorSpace (v :: *) (f :: *) which could then be used for a whole bunch of things, eg: N-dimensional euclidean space, complex numbers, quaternions, and I'm sure there are others. Or perhaps this has been done already?
I agree that it would be nice to be able to use + and * for these operations, but I also like that + and * have a precise meaning arising from how they interact with each other in PureScript, because of the Semiring laws, which I think we'd lose by splitting up Semiring like this.
This is a good point, actually. I haven't considered this.
I think it might be good to have a VectorSpace class in a library, maybe VectorSpace (v :: * -> *) where the type parameter for v is the type of the field (scalars), or perhaps VectorSpace (v :: *) (f :: *) which could then be used for a whole bunch of things, eg: N-dimensional euclidean space, complex numbers, quaternions, and I'm sure there are others.
Sounds good! 👍
For what it's worth, this still sounds like a good idea to me!
@sharkdp I saw you didn't use instances at all (not even for Monoid) for https://github.com/sharkdp/purescript-quantities, but instead implemented qAdd, qSubtract, …, which is really a shame as it would have been really predestined for instantiating an AdditionMonoid or similar.
update: Ops, not true. Mixed up Quantity and Unit. Still, using <> instead of + feels wrong...
@paf31 Can you please explain how a "CommutativeMonoid subclass of Monoid" would exactly look like
The Haskell Foundation prelude (http://haskell-foundation.readthedocs.io/en/latest/core-numerical/) could also be an inspiration how this could be solved!
@sharkdp I saw you didn't use instances at all (not even for Monoid) for https://github.com/sharkdp/purescript-quantities, but instead implemented qAdd, qSubtract, …, which is really a shame as it would have been really predestined for instantiating an AdditionMonoid or similar.
update: Ops, not true. Mixed up Quantity and Unit. Still, using <> instead of + feels wrong...
I'm using <> for multiplication of units - but yes, I agree. It would be great to be able to use the multiplication operator *.
@hdgarrood Actually, thinking about this again ...
but I also like that + and * have a precise meaning arising from how they interact with each other in PureScript, because of the Semiring laws, which I think we'd lose by splitting up Semiring like this.
... I believe this would still be possible? We would simply have the laws that describe the interplay of the two monoids (the Distribution laws and the Annihilation law) in the Semiring class.
My issue with this is that in general, there doesn't appear to be any good way of deciding whether some monoid should use the Monoid type class, or AdditiveMonoid, or MultiplicativeMonoid, or some combination of all three. Having a three separate classes which all represent the exact same mathematical structure feels much more wrong to me than the current situation (even if these classes would occupy different places once you look further down in the hierarchy). If I have created a type which has just one sensible monoid instance, do I give it just Monoid, or all three, or something else? What do we do about code which needs to operate on some arbitrary monoid; how do you pick which constraint you're going to use when they mean the same thing? (Or am I misunderstanding; would each of these classes have different laws?)
This appears to me to really to just be about cosmetics, in which case I think the best approach is to define your own operator alias for append, either with the general type or specialised to some specific type.
... I believe this would still be possible? We would simply have the laws that describe the interplay of the two monoids (the Distribution laws and the Annihilation law) in the Semiring class.
Yes, but that's a significantly weakened version of what we have now, in my view. With this suggested approach you would be able to use + and * together with only the much weaker AdditiveMonoid a => MultiplicativeMonoid a => ... constraints, and then you don't have the Semiring laws.
Oh, sorry, I forgot that your proposal had commutativity for the additive monoid class but not the multiplicative one, so these classes aren't exactly the same. Even so, we do already have the Monoid and CommutativeMonoid classes, so I think this still applies.
I can't stop coming back to this issue 😅. I can't believe there is no better solution.
What about having AdditiveMonoid and MultiplicativeMonoid but no Monoid.
I was thinking of several examples and I can't think of one where I don't feel like one of the 2 is more appropriate.
"hello" + "world"
[1, 2] + [1, 2]
Quantity 5 N * Quantity 8 sGranted, 1 + 2 is commutative and "hello" + "world" isn't, but I don't understand why this should be a problem.
Every AdditiveMonoid is also a MultiplicativeMonoid according to the laws, so I'm not sure how that helps. MultiplicativeMonoid is just Monoid by another name.
Every AdditiveMonoid is also a MultiplicativeMonoid
AdditiveMonoid has add & zero, and MultiplicativeMonoid has mul & one.
So I think I don't understand what you mean!?
MultiplicativeMonoid is just Monoid by another name
And with the symbol everyone expects: * There would be no need for the meaningless <> anymore, instead we would use * and + everywhere.
So it seems reasonable that matrix and quaternion (for example) multiplication would be performed with the + operator?
The important bit is not the precise names or symbols used, but the types of the operations and the laws.
<> does have meaning - the meaning comes from the idea of a Monoid - again, the important part is the type of the operation <> and the laws it satisfies.
Having separate classes and choosing instances based on what operator feels more appropriate for that specific type would seriously harm modularity and reuse. Having just one Monoid class means that libraries like foldable-traversable or maps can write functions which work for any Monoid just once.
So it seems reasonable that matrix and quaternion (for example) multiplication would be performed with the + operator?
No, but what prevents one to use the * operator? ^^
the laws it satisfies
But the laws are not enforced in anyway. So this argument is mood anyway in my opinion.
It's just documentation and goodwill if something adheres to any laws. And you could just document if it does, or doesn't.
would seriously harm modularity and reuse
which work for any Monoid
This is exactly what https://github.com/tfausak/purescript-neon is really good at, and they have no laws at all 😅.
This guy is speaking from the bottom of my heart:
- Laws should not prohibit useful instances. This means you can use
oron booleans and arrays. - There should be no type class hierarchy. This means
HasZerodoes not implyHasAdd. If you need both, add both to your type signature. - Functions should be defined in type classes. This means
addcan be used for both numbers and strings. - Type classes should be as small as possible. This means the
Boundedtype class is split intoHasBottomandHasTop. - Type classes should be designed for programmers, not mathematicians. This means
HasAddis a semigroup, but it's not calledSemigroup.
I think I should maybe just try to revive the project.
Quaternion and matrix multiplication does not commute, that’s what stops the use of *.
Giving up instances adhering to laws is an option, but not one we will ever adopt in the core libraries or anything I’d use, since being able to reason about code is why I like PS.
I can't see how https://github.com/tfausak/purescript-neon would be less suited to reason about code, but my theoretical background in that department is still a little sparse...
instance quaternionAdd :: Quaternion HasAdd where ...Btw: It seems just as unreasonable that matrix and quaternion multiplication is performed with the append operator.
Laws are a big part of what enable you to reason about code. For instance, the Monoid laws ensure that we don’t leak information about the structure of the map in the function foldSubmap - we would lose that property if we dropped the laws from the Monoid class.
dropped the laws from the Monoid class
Like I said, they only exist in documentation. You can't really drop them anyways ^^.
We could just as well write:
foldSubmap :: forall k v m. Ord k => HasEmpty m => HasAppend m => Maybe k -> Maybe k -> (k -> v -> m) -> Map k v -> m
Or If want to keep it shorter:
class (HasEmpty a, HasAppend a) <= Monoid a
and then we can reuse Monoid.
Anyway it boils down to:
Type classes should be as small as possible. This means the Bounded type class is split into HasBottom and HasTop.
Sounds like a really good idea to me.
In practice, laws are adhered to, and this is ‘enforced’ socially - if I provide a non law abiding instance by accident, and someone notices and lets me know, then that’s a bug and I’ll prioritise fixing it. Where appropriate I’ll provide a proof in the comments. Adherence to laws is generally not machine checked but empirically laws are still extremely useful.
I feel like you’re not reading what I wrote properly. You can of course write that function using Neon’s classes, but it leaks internal information if you use it with something which isn’t a genuine Monoid.
if I provide a non law abiding instance by accident, and someone notices and lets me know, then that’s a bug and I’ll prioritise fixing it
If I write in my documentation it should adhere to the law... It's the same thing.
If you want to give it a name you can make a class class (HasEmpty a, HasAppend a) <= Monoid a
I feel like you’re not reading what I wrote properly.
Sorry, I think we're talking past each other, or I don't understand the topic well enough.
I think I didn't get what you meant with 'leaks internal information'