Что такое структуры с "вычитанием", но без обратного?

Question

Группа расширяет идею моноида, чтобы учесть обратное. Это позволяет:

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

Но как насчет структур, таких как натуральные числа, где нет обратного? Я думаю о:

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

с законами:

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

И дополнительно:

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)

Итак, мой вопрос: что MRemove?

Answer 1

Имя, которое вы ищете, - это отменный моноид, хотя, строго говоря, сокращающей полугруппы достаточно, чтобы уловить понятие вычитания. Я задавался вопросом об одном и том же вопросе год или около того назад, и я нашел ответ, копаясь в математическом жаргоне. Посмотрите на класс CancellativeMonoid в пакете incremental-parser. В настоящее время я готовлю новый пакет, который будет содержать только подклассы monoid и несколько их экземпляров, и я надеюсь выпустить его в ближайшее время.

Answer 2

Самая близкая общая структура, о которой я могу думать, - это торсор, но на самом деле это не относится к естественным признакам очевидным образом. Подумайте об операциях, которые вы можете выполнять над значениями времени:

• "Вычтите" два раза, получив интервал времени (другой тип)
• Добавьте интервал времени ко времени, чтобы получить другое время
• Добавьте или вычтите интервалы времени, чтобы получить другой интервал

Очень немногие другие операции над парами значений времени имеют смысл. Вы не можете добавлять времена, умножать их или что-то, к чему мы привыкли в алгебре. С другой стороны, тип интервала гораздо более гибкий, поддерживающий сложение, вычитание, инверсию и так далее. Таким образом, торсор может быть определен в Haskell как:

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

В любом случае, это попытка ответить на ваш прямой вопрос (вы можете найти больше на превосходной странице Джона Баеза о них), даже если это не покрывает ваш естественный пример.

Насколько мне известно, единственное, что близко подходит к ответу на ваш вопрос, - это решение для повторного использования кода в тактике Coq (полу) кольцевого решения. Они вводят понятие "почти кольца" с аксиомами, похожими на те, которые вы описываете, чтобы позволить им повторно использовать большую часть своего кода для натуральных чисел, а также для полных колец. Я не думаю, что идея очень широко распространена, хотя.

Answer 3

Подобный вопрос был задан здесь. Ответ, данный там, является коммутативным моноидом с monus.

Answer 4

РЕДАКТИРОВАТЬ: Этот ответ является неправильным. Смотрите мой комментарий ниже. Я сохраняю ответ на случай, если он будет интересным.

Взгляните на полугруппы вычитания. Это полугруппа с оператором вычитания, которая подчиняется этим законам:

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)

К сожалению, я не могу найти ресурсы, в которых обсуждается "моноид вычитания", но я полагаю, что он должен подчиняться следующему дополнительному закону:

x - x = 0