logo标签列表

"Reader" Monad是什么？

haskellmonads
19

好的，那么写作单子允许您将一些内容写入[通常是]某种容器中，并在最后获取该容器。在大多数实现中，“容器”实际上可以是任何幺半群。

现在，还有一个“读者”单子。你可能认为它会提供逐个从某种容器中读取内容的对称操作。事实上，这并不是通常的读取器单子提供的功能。（相反，它仅提供对半全局常量的易于访问性）

要实际编写一个与通常的写作单子对称的单子，我们需要一些与幺半群对称的结构。

  1. 有人知道这个对称结构可能是什么吗？
  2. 有人写过这个单子吗？ 它有一个众所周知的名称吗？
5
写作器单子的对偶难道不是共写器余单子吗？（开玩笑的，我并不真正理解你想象的是什么。也许是消耗流的状态？） - Daniel Fischer
@DanielFischer 这听起来够疯狂，甚至可能是正确的... - MathematicalOrchid
第二个问题让我想到了人们提出的无限流处理库（Iteratee、pipes、conduits等）。 - hugomg
3
“读者”单子通常被称为环境单子（我认为后者的名称实际上可能早于前者 - 可以查看大卫·埃斯皮诺萨在90年代中期的论文进行早期参考），因此期望读者是“写者”的“对偶”可能期望过高。 - stephen tetley
3个回答
34

单子半群的对偶是余单子半群。回忆一下，一个单子半群被定义为（等同于某个东西）

 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中，这是唯一的实例。只有一个共同单子实例，我们可以将阅读器重新表述为编写者的确切对偶，但由于只有一个共同单子实例，我们得到了类似于标准阅读器类型的等同物。

所有类型都是共同单子是使类别“笛卡尔闭”（Cartesian）的原因。 “幺半闭类别”类似于CCC，但没有此属性，并且与子结构类型系统相关。 线性逻辑的吸引力之一就是增加了对称性。 而具有子结构类型则允许您定义具有更多有趣属性的共同单子（支持资源管理等），事实上，这为理解C ++中的复制构造函数和析构函数的角色提供了框架（尽管C ++不执行重要属性，因为存在指针）。

编辑：来自共同单子的阅读器

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

请注意，以上代码中每个变量绑定后仅使用一次（因此所有这些都可以用线性类型）。单子律证明是微不足道的，只需要遵守余元律即可。因此，Reader 真的是 Writer 的对偶。

这肯定不是唯一可能的 comonoid 实例吧？比如：instance Comonoid [a] where { delete = const () ; split [] = ([], []) ; split (x:xs) = ([x], xs) } - user1020786
3
@DarkOtter：这违反了所有三条法则。第一条法则规定idL.first delete $ split (x:xs)必须等于x:xs，但是idL.first delete $ split (x:xs) = idL $ first delete ([x],xs) = idL ((),xs) = xs ≠ x:xs。同样，idR.second delete $ split (x:xs) = idR $ second delete ([x],xs) = idR ([x],()) = [x] ≠ x:xs；而且assoc.first split $ split (x:y:zs) = assoc $ first split ([x],y:zs) = assoc (([x],[]),y:zs) = ([x],([],y:zs))，但是second split (split x:y:zs) = second split ([x],y:zs) = ([x],([y],zs)) ≠ ([x],([],y:zs))。（抱歉格式不好，但评论没有更好的方式。） - Antal Spector-Zabusky
2
@DarkOtter 假设完整性：delete 必须是 const()，对吧？这样我们就可以通过法则展示 fst . split = id 和 snd . split = id。这导致我们得出只有一个实例的结论。如果语言不是纯的，我们可能会有更有趣的实例。 - Philip JF
3
另外，您可以将“Comonoid”类的签名概括为使用除Haskell函数以外的态射，即：delete :: C m ()和split :: C m (m，m)。 - Gabriella Gonzalez
2
@GabrielGonzalez 当然，这让你可以做一些有趣的事情，但你必须在你所使用的类别中构建读取器单子，而不是在Hask中。共单子只是相反类别中的单子，因此我们可以定义一个单一的单子类并完成它。 - Philip JF
13

我不完全确定单子的对偶应该是什么，但是认为对偶（可能不正确）是某物的相反面（仅仅基于共单子是单子的对偶，并且具有相同的操作但方向相反）。与其基于 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上见过的幺半群阶乘类这里。

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

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

我不确定关于共单子的东西，但是供给单子看起来非常像我所想的。 - MathematicalOrchid
3

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

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

但是由于"Supply"基于状态，因此除了最左侧路径上的标签外，所有标签都将位于底部。

您需要一些可分割的东西（就像@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 成为一个单子，split x = (x,x)，这样你就又得到了普通的 Reader。
许多在 Haskell 中使用的单子并不是真正的单子——即它们只满足等价关系下的单子法则。例如，许多非确定性单子如果按照规则进行转换，将会以不同的顺序给出结果。但没关系，如果你只想知道某个特定元素是否存在于输出列表中，那么这仍然足够成为单子。
如果你允许 Supply 成为一种等价关系单子，那么你可以得到非平凡的分离。例如，value-supply 将构造可分离实体，它们将从未指定顺序的列表中分配唯一标签（使用 unsafe* 魔术）——因此，一个值供应单子的供应单子将是标签的置换单子。这对于许多应用程序来说已经足够了。实际上，有一个函数可以做到这一点。
runSupply :: (forall r. Eq r => Supply r a) -> a

该函数抽象了等价关系，提供了一个明确定义的纯接口。因为它只允许您查看标签并检查它们是否相等，这不会因为排列而改变。如果在Supply上仅允许使用runSupply观察，则在唯一标签的供应中使用Supply是一个真正的单子。

1
许多“单子”甚至在等价意义下也不是单子，而只是一种排序关系！也就是说，您必须使用某些“小于或等于”运算符来重写定律。许多单子，例如某些状态版本，在引入seq之前都是真正的单子，但此后几乎所有单子都被破坏了。即使是Id可能也不是单子，因为(.)和id不能形成一个范畴。我认为正确的理论方法可能是用二范畴重新表述所有法律，并在等式的位置上使用2-细胞。 - Philip JF
网页内容由stack overflow 提供, 点击上面的
可以查看英文原文，
原文链接