这是一个啥样的结构？ （具有部分逆但不是共单子的单子）

Posted 2023-03-15

【中文标题】这是一个啥样的结构？ （具有部分逆但不是共单子的单子）

【英文标题】：What kind of structure is this? (Monad with a partial inverse but not a comonad)这是一个什么样的结构？ （具有部分逆但不是共单子的单子）

【发布时间】：2021-09-22 05:33:56

【问题描述】：

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

我有一个基本类型a，它由排序的字符串组成（例如"aacdee"，但不是"abca"）和来自a 的monad M，它只是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 -> a，它接受一个字符串列表，将它们连接起来并对结果进行排序。这是pure 的左逆，即a 上的extract . pure = id，但不是右逆。

我还想以extract . (extend f) = f 为所有f: M a -> a 的方式定义extend: (M a -> a) -> M a -> M 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 中可以对多种f 进行并行优化，我想将extend f 定义为针对许多特定情况的优化实现，回退到@987654348 @ 仅在未优化的情况下。

我的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)，即关联性，或者可能是一种较弱的形式。

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

【参考方案1】：

单独看extract，我们看到extract . pure = id。我们还看到extract . join = extract . fmap extract。这使得extract 成为algebra over the [] monad。

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

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

【讨论】：

对不起，我的符号可能不准确。我的意思是作文：extract ((extend f) x) = f x 代表M a 中的所有x。我现在在问题中添加了函数组合