15

A group extends the idea of a monoid to allow for inverses. This allows for:

gremove :: (Group a) => a -> a -> a
gremove x y = x `mappend` (invert y)

But what about structures like natural numbers, where there is no inverse? I'm thinking about:

class (Monoid a) => MRemove a where
    mremove :: a -> a -> a

with laws:

x `mremove` x = mempty
x `mremove` mempty = x
(x `mappend` y) `mremove` y = x

And additionally:

class (MRemove a) => Group a where
    invert :: a -> a
    invert x = mempty `mremove` x

-- | For defining MRemove in terms of Group
defaultMRemove :: (Group a) => a -> a -> a
defaultMRemove x y = x `mappend` (invert y)

So, my question is: what is MRemove?

singpolyma
  • 10,999
  • 5
  • 47
  • 71
  • I think it is the same as `Group`. `Group` does not add anything, it just implements a shortcut for what's already in `MRemove`, namely `invert = mremove mempty`. (but I'm no mathematician) – Will Ness Feb 16 '13 at 19:03
  • @WillNess Except that there exist structures, such as the natural numbers, for which there may be implemented `MRemove`, but not `Group` – singpolyma Feb 16 '13 at 19:04
  • 3
    what would be (2-5)? bottom, right? (7-5) would work, (2+5)-5 would work, (5+2)-5 would work, just 5+(2-5) would not work? what's so different about (0-5) then? what I'm driving at, we **anyway** need to define an extension of a given data type to allow for the `mremove` to be total (to work always). If we allow for `mremove` to diverge sometimes, we can allow for `invert` to diverge always just the same, no? And if we perform extension and `mremove` becomes total, so will `invert` then. – Will Ness Feb 16 '13 at 19:16
  • @WillNess yes, `mremove` will only be total if the structure is a group. However, when the structure is not a group, `invert` **always** diverges. – singpolyma Feb 16 '13 at 19:18
  • In real implementations of things like the natural numbers, usually `mremove` actually breaks the laws and returns `mempty` in the impossible cases, but that's not better than bottom from this perspective. – singpolyma Feb 16 '13 at 19:19
  • 1
    Wouldn't it satisfy the given laws to return `mempty`? A pseudo-subtraction on naturals that clips to zero is sensible and would seem to fit the requirements. – C. A. McCann Feb 16 '13 at 19:20
  • @C.A.McCann Hmm, you're right. I don't think clipping to `mempty` actually violates the laws I've had in mind – singpolyma Feb 16 '13 at 19:22
  • 2
    What if we consider sets instead of naturals. `mremove` would be set differencing and `mappend` would be a union operation. That definition makes sense and is total without the need for the objects to form a group. – sabauma Feb 16 '13 at 19:24
  • @singpolyma: I assumed that was *why* you wrote the laws that way, that `mremove` should coincide with `mappend`ing the inverse where the latter is defined, but can do something else in other cases. – C. A. McCann Feb 16 '13 at 19:25
  • @C.A.McCann It is. I think I confused myself by picking `Nat` as my example. @sabauma's example of sets is much clearer. – singpolyma Feb 16 '13 at 19:25
  • 4
    @singpolyma: Also, [this may be relevant](http://en.wikipedia.org/wiki/Monus). – C. A. McCann Feb 16 '13 at 19:28
  • @C.A.McCann that seems relevant, and I had considered a description in terms of ordering, but I'm not sure that generalizes to sets – singpolyma Feb 16 '13 at 19:33
  • Is there a reason you didn't include an axiom `(x // y) <> y = x`, where `(//) = mremove` and `(<>) = mappend`? If you include that, then I think you have a [right loop](http://en.wikipedia.org/wiki/Quasigroup#Right-_and_left-quasigroups). – Antal Spector-Zabusky Feb 16 '13 at 21:50
  • Actually, scratch that—quasigroups and loops don't require associativity. And if you have a loop, [Wikipedia says](http://en.wikipedia.org/wiki/Quasigroup#Loop) that all elements have a unique left and right inverse, so it would seem that an associative loop is just a group. If you have a right loop, then all elements necessarily have a unique left inverse. (I haven't yet proved that `x // y = x <> leftinv y`, but I'd guess that it's true.) So an associative right loop (`MRemove` plus the above axiom) is a structure much like a group, but with only one-sided inverses. – Antal Spector-Zabusky Feb 16 '13 at 22:24
  • @AntalS-Z I didn't include that axiom because it doesn't work on, say, naturals where `(x - y) + y` will be `y` if `y > x` – singpolyma Feb 16 '13 at 23:24
  • 1
    Set subtraction does not obey proposed laws. – n. m. could be an AI Feb 17 '13 at 16:32
  • @n.m. Oh, hmm. Because if x and y are overlapping sets, then (x U y) // y might be missing elements. Yeah – singpolyma Feb 17 '13 at 18:03
  • 1
    Do your monoids have the [cancellation property](http://en.wikipedia.org/wiki/Monoid#Properties)? Otherwise mremove is not well-defined. – j.p. Feb 20 '13 at 16:10
  • @jug if one is writing `mremove`, then it has to be well-defined (as specified by the laws, and possibly other laws) – singpolyma Feb 21 '13 at 23:22
  • @singpolyma: Exactly. Without the cancellation property, you have to make non-canonically choices leading to contradictions. Take for example the set consisting of 0 and 1 (and maybe 2 if you like it more complicated) with the multiplication (modulo 4 in case you take also 2). Your 3rd law gives (calling mappend "*" and mremove "/") contradicting values 0 and 1 for $0/0$: $(0*0)/0 = 0$ and $(1*0)/0 = 1$ (with $2$ you get for example $0$ or $2$ for $0/2$ as $(2*2)/2 = 2$ and $(0*2)/2 = 0$). – j.p. Feb 22 '13 at 17:59
  • @singpolyma: If your monoid is commutative and possesses the cancellation property, by Grothendieck's construction you have a subset of a group that is closed under multiplication. – j.p. Feb 22 '13 at 18:04

4 Answers4

9

The closest common structure I can think of is a torsor, but it doesn't really apply to naturals in an obvious way. Think of the operations you can perform on time values:

  • "Subtract" two times, yielding an interval of time (a different type)
  • Add an interval of time to a time to get another time
  • Add or subtract intervals of time to get another interval

Very few other operations on pairs of time values make sense. You can't add times, or multiply them, or anything we're used to in algebra. On the other hand, the interval type is much more flexible, supporting addition, subtraction, inversion, and so on. A torsor could thus be defined in Haskell as:

class Group (Diff a) => Torsor a where
  type Diff a
  subtract : a -> a -> Diff a
  add      : a -> Diff a -> a

Anyway, that's an attempt at answering your direct question (you can find more at John Baez's excellent page on them), even though it doesn't cover your natural example.

The only other thing that comes close to answering your question, as far as I know, is the solution to code reuse in Coq's (semi)ring solver tactic. They introduce a notion of an "almost ring" with axioms similar to the ones you describe, to allow them to reuse most of their code for naturals as well as full rings. I don't think the idea is very widespread, though.

copumpkin
  • 2,836
  • 18
  • 25
6

The name you're looking for is cancellative monoid, though strictly speaking a cancellative semigroup is enough to capture the concept of subtraction. I was wondering about the very same question a year or so ago, and I found the answer by digging through mathematical jargon. Have a look at the CancellativeMonoid class in the incremental-parser package. I'm currently preparing a new package that would contain only the monoid subclasses and a few of their instances, and I hope to release it soon.

Mario B.
  • 76
  • 1
  • Good find! Also http://en.wikipedia.org/wiki/Cancellation_property#Examples_of_cancellative_monoids_and_semigroups – singpolyma Feb 24 '13 at 18:02
  • There's a package called monoid subclasses which includes the cancellative monoid: https://hackage.haskell.org/package/monoid-subclasses-0.4.1.2/docs/Data-Monoid-Cancellative.html I just realised that a list is a `ReductiveMonoid`, but not a `CancellativeMonoid` nor a `CommutativeMonoid`, so the package can't represent lists as an instance of `ReductiveMonoid`. This is through using the `Data.List.(//)` operation as the mremove. – CMCDragonkai Dec 28 '15 at 11:00
1

A similar question has been asked here. The answer given there is a commutative monoid with monus.

Andrew Thaddeus Martin
  • 3,225
  • 17
  • 37
0

EDIT: This answer is wrong. See my comment below. I'm preserving the answer in case it is interesting.

Take a look at subtraction semigroups. It's a semigroup with a subtraction operator that obeys these laws:

x - (y - x) = x
x - (x - y) = y - (y - x)
(x - y) - z = (x - z) - y

x <> (y - z) = (x <> y) - (x <> z)
(y - z) <> x = (y <> x) - (z <> x)

Sadly, I cannot find resources that discussion a "subtraction monoid", but I assume it would need to obey the following additional law:

x - x = 0
Andrew Thaddeus Martin
  • 3,225
  • 17
  • 37
  • I think a subtraction semigroup may be too strong. It seems to have total subtraction. – dfeuer May 26 '18 at 11:59
  • The original question asks about a typeclass with total subtraction. However, I realized this morning that subtraction monoids are the wrong answer for a different reason. I mistook the <> operator to be addition when it's actually more like multiplication. So, it doesn't actually do what the original question asked about. – Andrew Thaddeus Martin May 26 '18 at 15:56