haskell - 这种自由(更自由？)单子(monad)的构造有效吗？

Question

在过去的 2 年里，我对使用免费的 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

直觉上。 Free只是在上下文中传递一个解释器。解释器只是将仿函数(或类型构造函数)转换为实际的 monad。在范畴论中，这只是仿函数之间的自然转换。 runFree函数只是解开它并应用解释器。
简而言之，在理论层面。考虑以下伴随仿函数:(Free : Endo -> Monad) ⊣ (Forgetful : Monad -> Endo) .我们有以下附加同构: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 的好处是:不需要处理仿函数实例。看起来直观、笔直、干净。在我看来，freer monad 最初需要处理的性能问题也没有。所以不需要更多的复杂性。总的来说，对我来说看起来很不错。
也因为我自己想出了它。我想知道有人已经在使用这种免费的单子(monad)结构了吗？您对此有何看法？谢谢!
编辑:
关于我自己在编程中构建自由单子(monad)的用法。我主要使用免费的 monad 来表达 monadic DSL。后来，我可以随心所欲地以多种方式解释它们。就像我想构建一个由 monadic DSL 定义的命令处理系统。并且还希望将其元信息提取为树状结构(对 DSL 本身的反射(reflection))。所以我可以建立两个解释器来完成这项工作。一个用于执行命令，另一个用于将 DSL 转换为树状结构。或者也许我想在不同的运行时环境中运行相同的 DSL。然后我可以为它们中的每一个编写适当的解释器，而无需引入样板代码。我发现这些用例通常非常容易并且适合免费的 monad 处理。希望我的经验对你有用!

Answer 1

是的，您的编码是正确的。免费的单子(monad)Free F在一个内仿函数上F也是类别F-Mon的初始对象谁的

对象 是单子(monad)M配备“代数”a :: forall x. F x -> M x (它们等价于 M 上的代数运算，即满足 a' :: forall x. F (M x) -> M x 的自然变换 a' . fmap join = join . a')和

箭头 是自然变换，既是单子(monad)同态又是代数同态。

粗略地说，您的编码 forall m. Monad m => (forall x. F x -> m x) -> m a准确地表示类别 F-Mon 中的初始对象, 就像 forall x. x表示基类中的初始对象，forall m. Monad m => m a表示初始单子(monad)(身份单子(monad))。
出于编程目的，此编码的行为类似于自由单子(monad)的 Church 编码 forall x. (f x -> x) -> (a -> x) -> x (或传统自由单子(monad)的共密度变换):它们支持 O(1) 时间单子(monad)绑定(bind)，但不再支持 O(1) 模式匹配(因此它们不适合计算效果的浅处理程序)。
我不记得有论文讨论过这种编码，但它可能是从事计算效应或代数理论工作的人们的民间传说。例如，在 Haskell 社区中，Wu 和 Schrijvers [2014]使用我之前提到的类别来融合处理程序；在代数理论研究中，Fiore 和 Hur [2009]讨论了 Σ-monoids 的更一般的概念。