18

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

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

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

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

3 回答 3

32

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

 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 中，这是唯一的例子。我们可以将 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。

于 2013-03-14T20:09:34.640 回答
13

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

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

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

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

在我看来，这尤其包含所有的 monoid 类。

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

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

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

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

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

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

于 2013-03-14T19:21:15.913 回答
3

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

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

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

你需要一些可拆分的东西（比如在@PhillipJF's 中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作为一个单子，split x = (x,x)你Reader又得到了正常的旧的。

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

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

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

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

于 2013-03-14T20:32:55.477 回答