这种自由（更自由？） monad 的构造有效吗？

Question

在过去的两年里，我对使用免费的 monad 来帮助我解决实际的软件工程问题很感兴趣。并使用一些基本范畴论提出了我自己的自由单子构造。

\n

{-# LANGUAGE RankNTypes #-}\n\nimport Control.Monad\n\ndata Free f a = Free (forall m. Monad m => (forall x. f x -> m x) -> m a)\n\nrunFree :: forall f m. Monad m => (forall x. f x -> m x) -> (forall a. Free f a -> m a)\nrunFree f (Free g) = g f\n\ninstance Functor (Free f) where\n  fmap f (Free g) = Free $ \\k -> fmap f (g k)\n\ninstance Applicative (Free f) where\n  pure = return\n  (<*>) = ap\n\ninstance Monad (Free f) where\n  return a = Free $ \\_ -> return a\n  Free f >>= g = Free $ \\k -> f k >>= \\a -> runFree k (g a)\n\nliftF :: forall f a. f a -> Free f a\nliftF x = Free $ \\k -> k x\n

\n

直观地说。Free只是在上下文中传递一个解释器。解释器只是将函子（或类型构造函数）转换为实际的 monad。在范畴论中，这只是函子之间的自然变换。runFree 函数只是解开它并应用解释器。

\n

简而言之，在理论层面。考虑以下伴随函子：(Free : Endo -> Monad) \xe2\x8a\xa3 (Forgetful : Monad -> Endo)。我们有以下伴随同构：Monad(Free f, m) ~ Endo(f, Forgetful m)。翻译成 haskell 的函数如下：

\n

alpha :: forall f m. Monad m => (forall a. Free f a -> m a) -> (forall x. f x -> m x)\nbeta  :: forall f m. Monad m => (forall x. f x -> m x) -> (forall a. Free f a -> m a)\n

\n

然后我们可以Free基于以下构造beta：

\n

data Free f a = Free (forall m. Monad m => (forall x. f x -> m x) -> m a)\n

\n

它只是将其包装在数据类型中。其余的就跟着吧。

\n

所以我只是想知道这种自由单子的构造有多好（或多坏）。在我看来，具有更自由的 monad 的好处：不需要处理函子实例。看起来直观、直接、干净。在我看来，freer monad 最初需要处理的性能问题似乎也没有。所以不需要更多的复杂化。总的来说，对我来说看起来相当不错。

\n

而且也是因为我自己想出来的。我想知道是否有人已经使用了这种免费 monad 的构造？您对此有何看法？谢谢！

\n

编辑：

\n

关于我自己在编程中关于自由 monad 构造的用法。我主要使用免费 monad 来表达 monadic DSL。后来我可以用多种方式解释它们，无论我想要什么。就像我想构建一个由 monadic DSL 定义的命令处理系统。并且还想将其元信息提取到树状结构（DSL 本身的反射）。所以我可以构建两个解释器来完成这项工作。一个用于执行命令，另一个用于将 DSL 转换为树状结构。或者也许我想在不同的运行时环境中运行相同的 DSL。然后我可以为它们每个人编写适当的解释器，而无需引入样板代码。我发现这些用例通常非常简单并且适合免费 monad 来处理。希望我的经验对你有用！

\n

Answer 1

是的，你的编码是正确的。Free F内函子上的自由单子F也是该范畴的初始对象，F-Mon其

\n

\n
• 对象M是配备有“代数”的单子a :: forall x. F x -> M x（相当于 的代数运算，即满足 的M自然变换），并且a\' :: forall x. F (M x) -> M xa\' . fmap join = join . a\'
\n
• 箭头是自然变换，既是单子同态又是代数同态。
\n

\n

宽松地说，您的编码forall m. Monad m => (forall x. F x -> m x) -> m a准确地表示类别中的初始对象F-Mon，就像forall x. x表示基本类别中的初始对象一样，并forall m. Monad m => m a表示初始单子（身份单子）。

\n

出于编程目的，此编码的行为类似于自由单子的 Church 编码forall x. (f x -> x) -> (a -> x) -> x（或传统自由单子的代码密度转换）：它们支持 O(1) 时间单子绑定，但不再支持 O(1) 模式匹配（因此它们不适合计算效果的浅层处理程序）。

\n

我不记得有论文具体讨论过这种编码，但这可能是研究计算效应或代数理论的人们的民间传说。例如，在 Haskell 社区中，Wu 和 Schrijvers [2014]使用了我之前提到的类别来融合处理程序；在代数理论的研究中，Fiore 和 Hur [2009]讨论了更一般的概念\xce\xa3-monoids。

\n