什么是"减法"但没有逆的结构？

Question

一个小组扩展了monoid的概念以允许反转.这允许:

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的优秀页面上找到更多信息),尽管它不包括你的自然例子.

据我所知,接近回答你问题的唯一另一件事就是Coq(半)环解算器策略中代码重用的解决方案.他们引入了一个"几乎环"的概念,其公理类似于你描述的公理,允许他们将大部分代码重用于自然以及完整的环.不过,我不认为这个想法非常普遍.

Answer 2

你正在寻找的名字是取消的幺半群,但严格来说,取消的半群足以捕捉减法的概念.大约一年前我对同一个问题感到疑惑,我通过挖掘数学术语找到了答案.查看incremental-parser包中的CancellativeMonoid类.我目前正在准备一个新的包,它只包含monoid子类和一些实例,我希望尽快发布它.