假设，所有单子都可以用Free（如果这不是真的，什么是反例，为什么）？如何使用or来表达延续单子或其对应的转换器- 对应的函子是什么？或者如果他们不能，原因是什么？FreeFreeT
更新：表达我的意思是基本上同构于Free FF我们正在寻找的仿函数where is，例如Writer w同构于Free ((,) w).
问问题
1386 次
4 回答
15
延续单子是您正在寻找的反例。我没有足够的知识来提供完整的证明，但我会给你一些参考资料以供查找。
这个想法是单子有一个与之相关的“等级”概念。“等级”大致表示提供 monad 的全部功能所需的操作数。
我怀疑，除了延续派生的 monad 之外，我们在 Haskell 中处理的所有 monad 都有等级，例如Identity, Maybe, State s, Either e, ..., 以及它们通过转换器的组合。例如，Identity由无操作生成，Maybe由Nothing、State s由get和由生成。（也许这表明它们实际上都有有限的排名，或者可能对每个 都算作不同的操作，所以大小的排名也是如此，我不确定。）put sEither eLeft eput ssState ss
自由单子当然有等级，因为Free f它是由 . 编码的操作显式生成的f。
这是排名的技术定义，但不是很有启发性： http://journals.cambridge.org/action/displayAbstract?aid= 4759448
在这里你可以看到延续单子没有等级的说法：http ://www.cs.bham.ac.uk/~hxt/cw04/hyland.pdf 。我不确定他们是如何证明这一点的，但这意味着延续单子不是由任何操作集合生成的，因此不能表示为自由单子的（商）。
希望有人能来整理我的技术细节，但这是你想要的证明的结构。
于 2014-09-14T10:25:03.630 回答
2
这是一个愚蠢的答案，表明您的问题和我之前的答案都需要工作。
Cont可以很容易地用 表示Free：
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是（当然）自由单子本身的（商）。所以现在你必须准确地澄清你所说的“表达”是什么意思。
于 2014-09-17T10:35:26.317 回答
2
请参阅我对您去年提出的问题的回答。让我们考虑r = Bool（或更一般地说，任何r承认非平凡自同构的类型）。
m将（直到 newtype 包装器）定义为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
于 2014-09-18T18:08:08.093 回答
1
这里有几个小证据，证明不存在一个Functor f这样的，对于所有人来说a :: *，m :: * -> * FreeT f m a相当于ContT r m a使用FreeT.
让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 (FreeT f m)实例，因为没有Functor m实例。（我放宽了FreeT从 requiresMonad m到 only requires 的正常解释，Functor 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 (FreeT f m)实例，因为没有Monad m实例。
如果我们不想使用 or 的正常解释，Free我们FreeT可以拼凑出类似Cont ror的怪物ContT r。例如，有一个Functor (f r)这样Free (f r) a可以等同于Cont r a使用 的异常解释Free，即Cont r它自己。
于 2014-09-17T02:50:04.227 回答