如何使用自由单子表达连续单子？

Question

如何使用自由单子表达连续单子？

27

据称，所有单子都可以使用Free表达（如果不是这样，那么有什么反例及其原因）？如何使用Free或FreeT表达连续体单子或其对应的变压器 - 对应的函子会是什么？如果它们不能，那么原因是什么？ 更新：通过“表达”，我基本上是指“同构于Free F”，其中F是我们正在寻找的函子，就像例如Writer w同构于Free ((,) w)。

- Petr

1

也许你应该将这个问题发布到计算机科学版块（https://scicomp.stackexchange.com/）- 那里很可能会有人回答你。 - Random Dev

2

但是 Writer w 并不同构于 Free ((,) w)，仅仅是它的商。毕竟，Writer w 就是 ((,) w)。此外，正如我下面所证明的那样，Cont r 同构于 Free (Cont r) 的商。你能进一步澄清吗？ - Tom Ellis

@TomEllis 很好的观点，我需要考虑一下。 - Petr

4个回答

3

这里有一个愚蠢的答案，用来说明你的问题以及我之前的回答都需要改进。使用Free可以轻松地表达Cont。

import Control.Monad.Free
import Control.Monad.Trans.Cont

type Cont' r = Free (Cont r)

quotient :: Cont' r a -> Cont r a
quotient = retract

Cont 是自由单子在自己上的（商），所以现在您需要明确“表达”是什么意思。

- Tom Ellis

我所说的“expressed”基本上是指与Free f同构，就像Maybe与Free MaybeF同构一样，其中data MaybeF a = MaybeF等。我会更新问题。 - Petr

Maybe 不是同构于 Free MaybeF，而只是它的商。 - Tom Ellis

1

如果 data MaybeF a = Nada，则 Maybe 同构于 Free MaybeF。 - Reid Barton

@ReidBarton：啊，是的，你和Petr关于“Maybe”是正确的。我想表达的是，一个单子不一般是Free f，其中f是某个生成操作的函子，而仅仅是它的商。你在这个答案中用State的例子也提到了同样的观点：https://dev59.com/SmUq5IYBdhLWcg3wQ-Xk#24918234 - Tom Ellis

2

请查看去年你的问题的我的回答。让我们考虑r = Bool（或更一般地，任何允许非平凡自同构的类型r）。

将m（新类型包装除外）定义为m :: (() -> Bool) -> Bool; m f = not (f ())。然后m是非平凡的，但m >> m是平凡的。因此，Cont Bool不同构于自由单子。

Haskell中的完整计算：

rwbarton@morphism:/tmp$ ghci
GHCi, version 7.8.3: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> import Control.Monad.Cont
Prelude Control.Monad.Cont> let m :: Cont Bool (); m = ContT (\f -> fmap not (f ()))
Loading package transformers-0.3.0.0 ... linking ... done.
Prelude Control.Monad.Cont> runCont m (const False) -- m not trivial
True
Prelude Control.Monad.Cont> runCont (m >> m) (const False)
False
Prelude Control.Monad.Cont> runCont (m >> m) (const True) -- (m >> m) trivial
True

- Reid Barton

确实，这是对我的问题的严谨回答。如果我的问题有意义，我可能需要仔细考虑一下，或者更深入地了解问题。正如你所说，大多数单子不能具有与它们同构的“Free”表示。另一方面，正如@TomEllis指出的那样，每个单子都是使用“retract”作为“Free m”的图像。因此，我正在寻找如何使用“Free F”表示单子“M”，使得“M”是“Free F”的同态图像，并且函子“F”在某种意义上是最小的。 - Petr

1

这里有一些微小的证明，证明不存在一个 Functor f，使得对于所有的 a :: * 和 m :: * ->*，使用 FreeT 的普通解释，FreeT f m a 等价于 ContT r m a。

设m :: * -> *，并且不存在Functor m实例。由于存在instance Functor (ContT r m)，因此存在Functor (ConT r m)实例。如果ContT r和FreeT f是等价的，则我们期望有Functor (FreeT f m)实例。然而，使用FreeT的正常解释，即instance (Functor f, Functor m) => Functor (FreeT f m)，由于没有Functor m实例，因此没有Functor (FreeT f m)实例。(我放松了对FreeT的正常解释，只要求Functor m，而不是要求Monad m，因为它只使用了liftM。)

让 m :: * -> *，使得没有实例 Monad m。由于 instance Monad (ContT r m)，因此存在实例 Monad (ConT r m)。如果 ContT r 和 FreeT f 是等效的，我们期望有 Monad (FreeT f m)。然而，使用 FreeT 的正常解释，即 instance (Functor f, Monad m) => Monad (FreeT f m)，因为不存在 Monad m 实例，所以也就没有 Monad (FreeT f m) 实例。

如果我们不想使用 Free 或 FreeT 的正常解释，我们可以拼凑出像 Cont r 或 ContT r 一样工作的怪物。例如，存在一个 Functor (f r)，使得使用 Free (f r) a 的异常解释，即 Cont r 本身，可以等价于 Cont r a。

- Cirdec

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Tom Ellis · Accepted Answer

续延单子就是你要找的反例。我不太了解，无法提供完整证明，但我会给你一些参考。

想法是单子与其关联的“级别”概念。 “等级”大致意味着提供单子的全部功能所需的操作数量。

我怀疑，除了续延衍生单子之外，在Haskell中处理的所有单子都具有等级，例如Identity、Maybe、State s、Either e，通过它们的变换器进行组合。例如，Identity由没有任何操作生成，Maybe由Nothing生成，State s由get和put s生成，Either e由Left e生成。(也许这表明它们实际上都具有有限的等级，或者put s对于每个s都计算为不同的操作，因此State s的等级为s的大小，我不确定。)

自由单子肯定具有等级，因为Free f是由f编码的操作显式生成的。

这里是等级的技术定义，但并没有多少启示作用：http://journals.cambridge.org/action/displayAbstract?aid=4759448

在这里，您可以看到关于 continuation monad 没有秩的说法：http://www.cs.bham.ac.uk/~hxt/cw04/hyland.pdf。我不确定他们是如何证明的，但是暗示着 continuation monad 不是通过任意一组操作生成的，因此不能被表示为（自由 monad 的商）。

希望有人能够理清我的技术问题，但这就是您想要证明的结构。