这种自由（更自由？） monad 的构造有效吗？
在过去的两年里，我对使用免费的 monad 来帮助我解决实际的软件工程问题很感兴趣。并使用一些基本范畴论提出了我自己的自由单子构造。
{-# LANGUAGE RankNTypes #-}
import Control.Monad
data Free f a = Free (forall m. Monad m => (forall x. f x -> m x) -> m a)
runFree :: forall f m. Monad m => (forall x. f x -> m x) -> (forall a. Free f a -> m a)
runFree f (Free g) = g f
instance Functor (Free f) where
fmap f (Free g) = Free $ \k -> fmap f (g k)
instance Applicative (Free f) where
pure = return
(<*>) = ap
instance Monad (Free f) where
return a = Free $ \_ -> return a
Free f >>= g = Free $ \k -> f k >>= \a -> runFree k (g a)
liftF :: forall f a. f a -> Free f a
liftF x = Free $ \k -> k x
直观地说。 免费 只需在上下文中传递解释器即可。解释器只是将函子（或类型构造函数）转换为实际的 monad。在范畴论中，这只是函子之间的自然变换。 runFree 函数只是解开它并应用解释器。
简而言之，在理论层面。考虑以下伴随函子：(Free : Endo -> Monad) ⊣ (Forgetful : Monad -> Endo)。我们有以下伴随函子： Monad(Free f, m) 〜Endo（f，健忘的m）。翻译成 haskell 的函数如下：
alpha :: forall f m. Monad m => (forall a. Free f a -> m a) -> (forall x. f x -> m x)
beta :: forall f m. Monad m => (forall x. f x -> m x) -> (forall a. Free f a -> m a)
然后我们可以基于 beta 构造 Free：
data Free f a = Free (forall m. Monad m => (forall x. f x -> m x) -> m a)
它只是将其包装在数据类型中。其余的就跟着吧。
所以我只是想知道这种自由单子的构造有多好（或多坏）。在我看来，具有更自由的 monad 的好处：不需要处理函子实例。看起来直观、直接、干净。在我看来，freer monad 最初需要处理的性能问题似乎也没有。所以不需要更多的复杂化。总的来说，对我来说看起来相当不错。
也因为我自己想到了它。我想知道有人已经在使用这种免费 monad 的构造了吗？您对此有何看法？谢谢！
编辑：
关于我自己在编程中关于自由 monad 构造的用法。我主要使用免费 monad 来表达 monadic DSL。后来我可以用多种方式解释它们，无论我想要什么。就像我想构建一个由 monadic DSL 定义的命令处理系统。并且还想将其元信息提取到树状结构（DSL 本身的反射）。所以我可以构建两个解释器来完成这项工作。一个用于执行命令，另一个用于将 DSL 转换为树状结构。或者也许我想在不同的运行时环境中运行相同的 DSL。然后我可以为它们每个人编写适当的解释器，而无需引入样板代码。我发现这些用例通常非常简单并且适合免费 monad 来处理。希望我的经验对你有用！
In the past 2 years, I was interested in using free monad to helping me to solve practical software engineering problem. And came up my own construction of free monad using some elementary category theory.
{-# LANGUAGE RankNTypes #-}
import Control.Monad
data Free f a = Free (forall m. Monad m => (forall x. f x -> m x) -> m a)
runFree :: forall f m. Monad m => (forall x. f x -> m x) -> (forall a. Free f a -> m a)
runFree f (Free g) = g f
instance Functor (Free f) where
fmap f (Free g) = Free $ \k -> fmap f (g k)
instance Applicative (Free f) where
pure = return
(<*>) = ap
instance Monad (Free f) where
return a = Free $ \_ -> return a
Free f >>= g = Free $ \k -> f k >>= \a -> runFree k (g a)
liftF :: forall f a. f a -> Free f a
liftF x = Free $ \k -> k x
Intuitively. Free just passing an interpreter around the context. The interpreter just transform a functor(or a type constructor) to the actual monad. In category theory, this is just a natural transformation between functors. runFree function just unravel it and apply the interpreter.
In short, at the theoretical level. Consider the following adjoint functor: (Free : Endo -> Monad) ⊣ (Forgetful : Monad -> Endo).We have the following adjunction isomorphism: Monad(Free f, m) ~ Endo(f, Forgetful m). Which translate to haskell are the following function:
alpha :: forall f m. Monad m => (forall a. Free f a -> m a) -> (forall x. f x -> m x)
beta :: forall f m. Monad m => (forall x. f x -> m x) -> (forall a. Free f a -> m a)
Then we can construct Free based on beta:
data Free f a = Free (forall m. Monad m => (forall x. f x -> m x) -> m a)
Which just wraps it in a data type. And the rest just follow.
So I'm just wondering how good(or bad) is this construction of free monad. It seems to me to have the benefit of freer monad: not need to deal with functor instance. Looks intuitive, straight and clean. It also seems to me have no performance problem that freer monad originally need to deal with. So no more complication needed. In total, looks pretty decent for me.
And also because I came up of it myself. I'm wondering did someone already using this construction of free monad? And what's your opinion about it? Thanks!
Edit:
About my own usage about this construction of free monad in programming. I'm mostly using free monad to express monadic DSLs. And later I can interpret them in multiple ways whatever I want. Like I want to build a command handling system defined by monadic DSL. And also want to extract it's meta information to tree like structure(reflection on DSL itself). So I can build two interpreter to do the job. One for executing command and another for transform DSL to tree like structure. Or maybe I want to run the same DSL in different runtime environment. Then I can write appropriate interpreter for each of them without introducing boilerplate code. I found out those use cases are in general very easy and suitable for free monad to deal with. Hope my experience will be useful to you!
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
是的，你的编码是正确的。末端函子
F上的自由单子Free F也是类别F-Mon的初始对象，其M配备了“代数”a :: forall x。 Fx-> M x（相当于M上的代数运算，即自然变换a' :: forall x。F (M x) -> ; M x满足a' 。 fmap join = join . a') 和宽松地说，您的编码
forall m。莫纳德 m => (对于所有x.F x -> mx) -> m a准确地表示类别F-Mon中的初始对象，就像forall x 一样。 x表示基本类别中的初始对象，表示所有 m。莫纳德 m => m a表示初始单子（恒等单子）。出于编程目的，此编码的行为类似于免费 monads
forall x 的 Church 编码。 (fx->x)-> (a→x)→ x（或传统自由单子的代码密度转换）：它们支持 O(1) 时间单子绑定，但不再支持 O(1) 模式匹配（因此它们不适合计算效果的浅层处理程序） 。我不记得有论文具体讨论过这种编码，但这可能是研究计算效应或代数理论的人们的民间传说。例如，在 Haskell 社区中，Wu 和 Schrijvers [2014]< /a> 使用我之前提到的类别来融合处理程序；在代数理论的研究中，Fiore 和 Hur [2009] 讨论了Σ-幺半群的更一般概念。
Yes, your encoding is correct. The free monad
Free Fover an endofunctorFis also the initial object of the categoryF-MonwhoseMequipped with "algebras"a :: forall x. F x -> M x(which are equivalently algebraic operations onM, ie, natural transformationsa' :: forall x. F (M x) -> M xsatisfyinga' . fmap join = join . a'), andLoosely speaking, your encoding
forall m. Monad m => (forall x. F x -> m x) -> m aexactly denotes the initial object in the categoryF-Mon, just likeforall x. xdenotes the initial object in the base category, andforall m. Monad m => m adenotes the initial monad (the identity monad).For programming purposes, this encoding behaves similarly to the Church encoding of free monads
forall x. (f x -> x) -> (a -> x) -> x(or the codensity transformation of the conventional free monads): they support O(1) time monadic binding, but no longer support O(1) pattern matching (thus they are not suitable for shallow handlers of computational effects).I don't remember papers discussing exactly this encoding, but it is probably folklore among people working on computational effects or algebraic theories. For example, in the Haskell community, Wu and Schrijvers [2014] used the category I mentioned earlier for the purpose of fusing handlers; and in the study of algebraic theories, Fiore and Hur [2009] discussed the more general notion of Σ-monoids.