“读者”单子

Question

好的，因此 writer monad 允许您将内容写入 [通常] 某种容器，并在最后取回该容器。在大多数实现中，“容器”实际上可以是任何幺半群。

现在，还有一个“读者”单子。这，您可能会认为，将提供双重操作 - 从某种容器增量读取，一次一个项目。事实上，这不是通常的 reader monad 提供的功能。 （相反，它只是提供对半全局常量的轻松访问。）

要真正编写一个 与通常的 writer monad 对偶的 monad，我们需要某种与 monoid 对偶的结构。

1. 有人知道这种双重结构可能是什么吗？
2. 有人写过这个单子吗？它有一个众所周知的名字吗？

Answer 1

幺半群的对偶是一个类群。回想一下，幺半群被定义为（同构的东西）

 class Monoid m where
    create :: () -> m
    combine :: (m,m) -> m

根据这些法律

 combine (create (),x) = x
 combine (x,create ()) = x
 combine (combine (x,y),z) = combine (x,combine (y,z))

因此

 class Comonoid m where
    delete :: m -> ()
    split :: m -> (m,m)

需要一些标准操作

 first :: (a -> b) -> (a,c) -> (b,c)
 second :: (c -> d) -> (a,c) -> (a,d)

 idL :: ((),x) -> x
 idR :: (x,()) -> x

 assoc :: ((x,y),z) -> (x,(y,z))

有类似的法律

idL $ first delete $ (split x) = x
idR $ second delete $ (split x) = x
assoc $ first split (split x) = second split (split x)

这个类型类看起来很奇怪是有原因的。它有一个实例

instance Comonoid m where
   split x = (x,x)
   delete x = ()

在 Haskell 中，这是 only 实例。我们可以将 reader 重铸为 writer 的精确对偶，但由于 comonoid 只有一个实例，因此我们得到了与标准 reader 类型同构的东西。

让所有类型都是共形是使“笛卡尔封闭类别”中的类别“笛卡尔”的原因。 “Monoidal Closed Categories”类似于 CCC，但没有此属性，并且与子结构类型系统有关。线性逻辑的部分吸引力在于增加的对称性，这是一个例子。同时，具有子结构类型允许您定义具有更有趣属性的 comonoids（支持资源管理之类的东西）。事实上，这为理解 C++ 中复制构造函数和析构函数的作用提供了一个框架（尽管由于指针的存在，C++ 并没有强制执行重要的属性）。

编辑：comonoids 的读者

newtype Reader r x = Reader {runReader :: r -> x}
forget :: Comonoid m => (m,a) -> a
forget = idL . first delete

instance Comonoid r => Monad (Reader r) where
   return x = Reader $ \r -> forget (r,x)
   m >>= f = \r -> let (r1,r2) = split r in runReader (f (runReader m r1)) r2

ask :: Comonoid r => Reader r r
ask = Reader id

请注意，在上面的代码中，每个变量在绑定后只使用一次（因此这些变量都将使用线性类型）。 monad 定律证明是微不足道的，只需要 comonoid 定律起作用。因此，Reader 确实是 Writer 的对偶。

Answer 2

我不完全确定幺半群的对偶应该是什么，但认为对偶（可能是错误的）是某物的对立面（仅仅基于 Comonad 是 Monad 的对偶，并且具有所有相同的操作，但相反）。而不是基于mappend 和mempty 我会基于：

fold :: (Foldable f, Monoid m) => f m -> m

如果我们在这里将 f 专门化为一个列表，我们会得到：

fold :: Monoid m => [m] -> m

在我看来，这尤其包含所有的幺半群类。

mempty == fold []
mappend x y == fold [x, y]

那么，我猜这个不同的幺半群类的对偶将是：

unfold :: (Comonoid m) => m -> [m]

这很像我在 hackage here 上看到的 monoid 阶乘类。

因此，在此基础上，我认为您描述的“读者”单子将是supply monad。 supply monad 实际上是一个值列表的状态转换器，因此在任何时候我们都可以选择从列表中获取一个项目。在这种情况下，列表将是展开.supply monad 的结果

我应该强调，我不是 Haskell 专家，也不是专家理论家。但这是你的描述让我想到的。

Answer 3

Supply 是基于 State 的，这使得它对于某些应用程序来说不是最理想的。例如，我们可能想要创建一个提供值的无限树（例如随机数）：

tree :: (Something r) => Supply r (Tree r)
tree = Branch <$> supply <*> sequenceA [tree, tree]

但由于 Supply 是基于 State 的，所有标签都将位于底部，除了树下最左边路径的标签。

你需要一些可拆分的东西（比如@PhillipJF 的Comonoid）。但是如果你试图把它变成一个 Monad 就会出现问题：

newtype Supply r a = Supply { runSupply :: r -> a }

instance (Splittable r) => Monad (Supply r) where
    return = Supply . const
    Supply m >>= f = Supply $ \r ->
        let (r',r'') = split r in
        runSupply (f (m r')) r''

因为单子定律需要f >>= return = f，所以这意味着r'' = r 在(>>=) 的定义中。但是，单子定律也需要return x >>= f = f x，所以r' = r 也是如此。因此，Supply 成为一个 monad，split x = (x,x)，因此您又得到了常规的旧 Reader。

Haskell 中使用的许多 monad 并不是真正的 monad —— 即它们只满足规则直到某些等价关系。例如。如果您根据法律进行转换，许多非确定性单子将以不同的顺序给出结果。不过没关系，如果您只是想知道 是否 特定元素出现在输出列表中，而不是 where 中，这仍然是 monad。

如果您允许Supply 成为具有某种等价关系的单子，那么您可以获得非平凡的拆分。例如。 value-supply 将构造可拆分实体，这些实体将以未指定的顺序从列表中分配唯一标签（使用 unsafe* 魔法）——因此价值供应的供应单子将是标签排列的单子。这就是许多应用程序所需要的。而且，其实还有一个功能

runSupply :: (forall r. Eq r => Supply r a) -> a

它抽象了这种等价关系以提供定义明确的纯接口，因为它允许您对标签做的唯一事情是查看它们是否相等，并且如果您置换它们，这不会改变。如果 runSupply 是您在 Supply 上允许的唯一观察，那么 Supply 提供的唯一标签就是一个真正的 monad。