haskell - 什么是 "subtraction"但没有反转的结构？

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

我能想到的最接近的常见结构是躯干，但它并不真正以明显的方式适用于自然。想想您可以对时间值执行的操作:

“减去”两次，产生一个时间间隔(不同类型)

给一个时间加上一个时间间隔得到另一个时间

添加或减去时间间隔以获得另一个间隔

对时间值对的其他操作很少有意义。你不能加时间，或者乘它们，或者我们在代数中习惯的任何东西。另一方面，区间类型更加灵活，支持加法、减法、反演等。因此，在 Haskell 中，torsor 可以定义为:

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

无论如何，这是回答您直接问题的尝试(您可以在 John Baez 的优秀 page on them 中找到更多信息)，即使它没有涵盖您的自然示例。

据我所知，唯一接近回答您的问题的另一件事是 Coq's (semi)ring solver tactic 中代码重用的解决方案。 .他们引入了一个“几乎环”的概念，其公理类似于您所描述的公理，以允许他们将大部分代码重用于自然环和完整环。不过，我不认为这个想法很普遍。