这是自由(自由)的建筑吗？蒙纳德工作吗？
在过去的两年里，我有兴趣使用免费的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凭直觉。Free只是在上下文中传递一个解释器。解释器只是将函子(或类型构造函数)转换为实际的monad。在范畴理论中，这只是函子之间的一种自然变换。runFree函数只需要解压它并应用解释器。
总之，在理论层面上。考虑下面的伴随函子：(Free : Endo -> Monad) ⊣ (Forgetful : Monad -> Endo)，.We有以下的伴随同构：Monad(Free f, m) ~ Endo(f, Forgetful 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)然后，我们可以构建基于Free的beta。
data Free f a = Free (forall m. Monad m => (forall x. f x -> m x) -> m a)它只是将它封装在数据类型中。剩下的就跟着走。
所以我只是想知道这个自由单体的结构到底有多好(或有多糟)。在我看来，它具有更自由的monad的好处:不需要处理函子实例。看上去直观，笔直，干净。在我看来，在我看来，自由人最初需要解决的性能问题也没有。所以不需要再出现并发症了。总的来说，对我来说还算不错。
也是因为我自己想出来的。我在想是不是有人已经在使用这种免费的单曲了？你对此有什么看法？谢谢!
编辑：
关于我自己在程序设计中使用这种免费的monad的方法。我主要是用免费的单播来表达一元DSL。以后我可以用多种方式来解释我想要的东西。就像我想构建一个由一元DSL定义的命令处理系统一样。并希望将其元信息提取为树状结构(反映在DSL本身上)。所以我可以建立两个解释器来完成这项工作。一个用于执行命令，另一个用于将DSL转换为树状结构。或者我想在不同的运行时环境中运行相同的DSL。然后，我可以为其中每一个编写适当的解释器，而无需引入样板代码。我发现这些用例在一般情况下非常容易处理，并且适合于免费的monad处理。希望我的经验对你有帮助！
Stack Overflow用户
发布于 2022-03-21 21:38:24
是的，你的编码是正确的。内函数Free F上的自由单模F也是类别F-Mon的初始对象，其
- objects是带有“代数”
a :: forall x. F x -> M x的单模M(与M上的代数运算等价，即满足a' . fmap join = join . a'的自然变换a' :: forall x. F (M x) -> M x)，以及 - 箭头是自然变换，它既是单同态，又是代数同态。
松散地说，编码forall m. Monad m => (forall x. F x -> m x) -> m a准确地表示类别F-Mon中的初始对象，就像forall x. x表示基类别中的初始对象一样，forall m. Monad m => m a表示初始的monad (标识单)。
出于编程目的，这种编码的行为类似于forall x. (f x -> x) -> (a -> x) -> x的丘奇编码(或者传统的自由monads的共密度转换)：它们支持O(1)时间一元绑定，但不再支持O(1)模式匹配(因此它们不适合计算效果的浅层处理程序)。
我不记得关于这种编码的文章，但这可能是研究计算效果或代数理论的人们的民间传说。例如，在Haskell社区中，Wu和Schrijvers [2014年]使用我前面提到的类别来融合处理程序；在代数理论的研究中，Fiore和Hur [2009]讨论了Σ-一元的更广泛的概念。
https://stackoverflow.com/questions/71562355
复制相似问题
腾讯云开发者
