Last 是一个自由幺半群吗?

Zhi*_*gor 8 haskell functor category-theory monoids

自由幺半群通常被视为“列表幺半群”。然而,我对其他可能给我们自由幺半群的可能结构感兴趣。

首先,让我们回顾一下自由幺半群的定义。我从来没有完全理解如何将一个自由幺半群定义为一个遵守幺半群定律而不是其他任何东西的结构。我们如何证明某事不遵守上述规则但不遵守规则?或者这只是一种直觉?

无论如何,我们将讨论函子。如果某个幺半群是免费的,我们就用一个免费的函子得到它。很明显,列表在这里非常方便:

free :: Set -> Mon
free a = ([a], (++), [])
Run Code Online (Sandbox Code Playgroud)

然而,一个人可能会想出其他几个。例如,这是其中Last之一Data.Monoid

freeLast :: Set -> Mon
freeLast a = (Last a, (<>) :: Last a -> Last a -> Last a, Last Nothing) 
Run Code Online (Sandbox Code Playgroud)

那么,这个函子会生成Last一个自由幺半群吗?更一般地说,如果 存在一个守法实例Monoid (T a),那么是T一个自由幺半群吗?

Bar*_*ski 11

这是理解自由幺半群的一种方式:如果有人给你一个值,你能推断出它是如何创建的?考虑一个自然数的可加幺半群。我给你一个 7 并问你我是怎么得到它的。我可以添加 4+3,或 3+4,或 2+5 等。有很多可能性。这些信息丢失了。另一方面,如果我给你一个 list [4, 3],你知道它是从单例[4][3]. 除了可能[]涉及一个单位。也许是[4]<>[3]<>[][4]<>[]<>[]<>[3]。但它绝对不是[3]<>[4]

对于更长的列表,[1, 2, 3],您有其他选项([1]<>[2]) <> [3], 或[1] <> ([2]<>[3]),以及空列表的所有可能插入。所以你丢失的信息遵循单位定律和结合性,但没有别的。自由幺半群值会记住它是如何创建的、模单位定律和结合性。