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

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

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?

Ответ 1

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

Ответ 2

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

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

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

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

Во всяком случае, попытка ответить на ваш прямой вопрос (вы можете найти на странице "Лучшая , хотя это не распространяется на ваш естественный пример.

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