What are structures with "subtraction" but no inverse?

Question

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?

Answer 1

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.

Answer 2

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.