4

我遇到了一个结构，它看起来像具有单边逆元和一些附加属性的单子。我不确定这个结构的哪些属性是必不可少的，哪些是偶然的，所以我将在我的描述中遵循一个简单的例子。

我有一个基本类型a，它由排序的字符串（例如"aacdee"但不是"abca"）和来自的 monadM组成a，这只是 List monad:M a是排序字符串的列表。这个 monad 定义pure: a -> M a,fmap: (a -> a) -> M a -> M a和bind: (a -> M a) -> M a -> M a.

现在我定义extract: M a -> awhich 接受一个字符串列表，将它们连接起来并对结果进行排序。这是 的左逆pure，即extract . pure = idon a，但不是右逆。

我也想以extend: (M a -> a) -> M a -> M a这样的方式定义extract . (extend f) = f所有f: M a -> a.

虽然可以定义extend f = pure . f，但我不想这样做。例如，如果f是用字母表中的下一个字符替换每个字符、连接和排序的函数，我只想extend f用下一个字符替换每个字符。类似地，如果f从第一个字符串中删除所有“a”，从第二个字符串中删除所有“b”，等等。

举一个不那么简单的例子，f将第一个字符串作为函数，然后如果第二个字符串比第一个字符串长，则使用第二个字符串的最后一个元素扩展第一个字符串，依此类推。例如，f ["ab", "c", "def"] = "abf"。在这种情况下，我extend f只想拟合每个字符串，只留下对结果有贡献的字母，在示例中(extend f) ["ab", "c", "def"] = ["ab", "", "f"]。

所有这一切背后的想法是，一个人可以对M a多种.fextend fextend f = pure f

我extend不会满足comonad公理，但至少会满足以下条件（或非常相似的条件，我不完全确定关联性）：

  • (extend f) . pure = pure . f . pure，即在单个字符串上f并且extend f本质上是相同的，
  • extend (extract . (fmap h)) = fmap h, 即如果g = extract . (fmap h)分别作用于每个字符串，则extend g执行相同的操作，
  • (extend f) . (extend g) = extend (f . pure . g)，即关联性，或者可能是它的较弱形式。

我的问题。这是一个众所周知的结构吗？它有什么特别有趣的特性吗？

4

1 回答 1

1

单独看extract，我们看到了extract . pure = id。我们也看到了extract . join = extract . fmap extract。这对monadextract进行了代数[]。

特别是，[]monad 上的代数恰好对应于幺半群（范畴论解释：健忘函子Monoids -> Sets是 monadic，它的左伴随是[]，所以幺半群恰好是函子上的代数[]）。所以用明显的单位和合成法则extract定义了一个幺半群。a

至于extend，我认为您没有正确的类型。这是因为extend f :: M a -> M a, soextend f不能作为参数extract，因此extract (extend f)不进行类型检查。也许一旦你解决了这个问题，就会更容易理解这里发生了什么。

于 2021-07-14T19:45:47.240 回答