问题标签 [comonad]

让我们考虑一个在隧道中徘徊的侏儒。因此，我将定义一个代表这种情况的类型：

在这里，您可以在隧道的一部分看到一个矮人：

发现一个指向容器是 的一个实例Comonad。我可以在这里使用这个实例来定义一个模拟我的侏儒向右移动的函数：

看：

壮观的是，同样的操作适用于任意数量的矮人，在任何尖头容器中，因此如果需要，可以扩展到整个矮人堡垒。我可以类似地定义一个向左移动小矮人的函数，或者以任何其他确定性的方式。

但是现在如果我想让我的小矮人漫无目的地四处游荡怎么办？现在我的“随机移动”只能在同一个小矮人没有被放在左边的情况下把一个小矮人放在右边（因为这会使两个小矮人从一个小矮人中脱颖而出），而且它绝不能把两个小矮人放在同一个地方（这将使两个侏儒）。换句话说，“随机移动”必须是线性 的（就像在 “线性逻辑”中一样），当应用于一个 comonadic 堡垒时。

我想到的一种方法是为矮人分配某种状态，以跟踪矮人的可用动作，当我们决定该位置由其中一个人占据时，从每个相关矮人中删除动作。这样一来，剩下的矮人就无法采取这一行动了。或者我们可以跟踪位置的可用性。我在想某种“单子” extendM 可能有用。 （它会与通常extend相比traverse。fmap） 但我不知道任何现有技术。

一个尖的容器是一个comonad，这个观察可以用来获得一些有用的效果，比如模板卷积，几乎是免费的。此外还注意到，instance Comonad 可以通过Store 共单子 （通过部分应用的索引函数）以标准方式获得 an ，并且它的工作方式与手写定义一样好。

但是这种方式有个缺点：Store本质上是一个函数，一旦把东西做成函数，回去就不舒服了。而且我注意到在某些情况下，需求的微小变化需要完全放弃comonad的概念，并回到最初容器的考虑。我发现它类似于最终的无标签评估：本地转换很容易，但是它们需要的上下文越多，它就越复杂。可以通过在光标空间的相应子集上迭代提取来恢复初始容器的任何部分，但是为什么首先将初始类型换成最终类型呢？

换句话说，有 2 种方式来表示容器，并且都同样有利于 的定义instance Comonad：

1. 作为“初始”数据类型。如果没有依赖类型，Haskell 中的简单定义instance Comonad，当容器与索引配对时，是部分的（索引可能指向容器形状之外的位置），但它仍然可以工作。
2. 作为“最终”部分应用的索引函数。一个容器可以通过将其包裹在Store. 然后它会自动与索引配对。偏颇论点同样适用，因此无法获得安全性。

当初始类型与最终函数进行交换时，为初始类型定义的所有方法都将丢失，直到通过或多或少的精心设计恢复。鉴于对小型有限容器的访问是不安全的（大多数索引未定义），并且容器本身不可查询，因此编程变成了扫雷游戏。我没有有意放入的初始容器的任何属性EnvT，都会丢失。总而言之，无论 Store应该提供什么安全或便利利益，都受到处理容器最终表示的困难的挑战。

更简洁地说，一个尖头容器是一个comonad，但Store只是一个comonad。

那么，动机是Store什么？我们能得到一个instance Comonad，或者至少Extend，更便宜吗？

假设我有

• 一个comonadD
• 一个单子T
• l : D T -> T DcomonadD对 monad的 分配 律T.

我怎样才能定义comonad D T？

由于 State monad 可以分解为 Product（左 - Functor）和 Reader（右 - 可表示）。

1. 有没有办法分解Continuation Monad？下面的代码是我的尝试，它不会进行类型检查

2. 是否有形成单子的左右伴随的列表？

3. 我读过，给定一对伴随词，它们形成一个独特的 Monad 和 Comonad，但是，给定一个 Monad，它可以分解为多个因子。有这方面的例子吗？

在 Twitter 上，Chris Penner 为“使用默认值增强的地图”提出了一个有趣的comonad 实例。相关类型构造函数和实例在此处转录（有外观差异）：

我对这个comonad 实例有点怀疑，所以我尝试使用hedgehog-classes. 我选择了我能想到的最简单的仿函数f；共Identity轭：

根据hedgehog-classes，除了代表关联性的“双重复制”之外，所有测试都通过了：

不幸的是，即使对于所示的极其简单的输入，这个反例也很难解析。

幸运的是，我们可以通过注意到f参数是一个红鲱鱼来稍微简化问题。如果comonad 实例适用于显示的类型，它也应该适用于Identitycomonad。而且对于 any f，Map f k a可以分解成Compose (Map Identity k a) f，所以我们不失一般性。

f因此，我们可以通过将其专门化来摆脱它Identity：

正如我们所料，这再次失败了相同的结合律，但这次反例更容易阅读：

使用show-ingMapF'的一些组合语法，可以更容易地阅读反例：

所以我们可以看到不匹配是由于在duplicate.

所以看起来那个comonad不太有效。但是，鉴于结果非常接近，我很想看看是否有某种方法可以挽救它。例如，如果我们只保留地图而不是删除键会发生什么？

令我惊讶的是，这通过了所有测试（包括重复/重复测试）：

奇怪的是，这个实例与 s 没有任何关系Map了。它所需要的只是第二个字段中的东西是我们可以克服的东西fmap，即Functor. 所以这个类型的一个更贴切的名字可能是NotQuiteCofree：

现在我们可以测试一堆随机选择f的 s（包括Map ks）的共单子定律：

瞧，刺猬班发现这些实例中的任何一个都没有问题。

NotQuiteCofree从所有这些函子生成所谓有效的共单子的事实让我有点担心。NotQuiteCofree f a很明显不与 同构Cofree f a。

根据我有限的理解，从Functors 到Comonads 的 cofree 函子必须是唯一的，直到唯一的同构，因为它根据定义是附加的右半部分。NotQuiteCofree与 很明显不同Cofree，所以我们希望至少有f一些NotQuiteCofree f不是comonad。

现在来回答实际问题。事实上，我没有发现任何失败是因为我编写生成器的方式有误，或者可能是刺猬类中的错误，或者只是盲目的运气？如果不是，而且NotQuiteCofree {Identity | Const x | [] | Map k}确实是共单胞，你能想出其他不是f共单胞的吗？NotQuiteCofree f

或者，对于每一个可能的情况，是否真的f是NotQuiteCofree f一个共胞？如果是这样，我们如何解决两个不同的 cofree 共单胞之间没有自然同构的矛盾？

我刚从 Agda 开始，但了解一些 Haskell，并想知道如何在 Agda 中定义 Store Comonad。

这是我到目前为止所拥有的：

现在我收到以下错误：

我不太确定我做错了什么。任何帮助，将不胜感激！谢谢！

编辑

我想我越来越近了。我使用匹配的 lambda 替换了记录中的字段：

RawComonad来自https://github.com/agda/agda-stdlib/blob/master/src/Category/Comonad.agda 并具有签名

并且Store基于type Store s a = (s -> a, s)Haskell。

现在我得到的错误是：

我想知道这个错误是否与这一行有关：

我发现 Agda 中的编译错误消息并没有给出太多线索，或者我还没有能够很好地理解它们。

在论文中，声明式 UI 是未来——未来是由 Phil Friedman 提出的，他在介绍 cofree comonad 时声称：

这种说法在其他几个地方得到了回应，我假设源于这篇论文，直到最近我才把它放在我的“以后再想一想”堆上，因为我不熟悉卤素的工作原理。但是，现在我对卤素有些熟悉，我尝试更多地研究这个问题。然而，即使现在我了解了卤素的基础知识，这种说法对我来说仍然不是很明显，至少就我搜索而言，我还没有在网上找到任何地方试图详细说明或解释两者之间的这种联系cofree comonad 和卤素。

有没有人尝试过使用 cofree comonad 实际构建一个 UI 框架？如果没有，至少有人可以帮助更好地解释这个想法吗？例如，通过使用卤素中的一个组件的一些基本示例，并使用 cofree comonad 构建一个描述该组件的结构？或者更好的是，描述如何以类似于如何组合卤素组件的方式组合这些“cofree 组件”？

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

我有一个基本类型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)，即关联性，或者可能是它的较弱形式。

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