haskell - 自由对象是如何构造的？

Question

所以我明白自由对象被定义为附属的左侧。但这如何引导您找到此类对象的 Haskell 定义？

更具体地说:给定一个从单子(monad)范畴到内仿函数范畴的“健忘仿函数”，

newtype Forget m a = Forget (m a)
instance Monad m => Functor (Forget m) where
    fmap f (Forget x) = Forget (liftM f x)

然后是免费的 monad Free :: (* -> *) -> (* -> *)是一种允许(一个 Monad 实例和)以下同构的类型:

type f ~> g = forall x. f x -> g x

fwd :: (Functor f, Monad m) => (f ~> Forget m) -> (Free f ~> m)
bwd :: (Functor f, Monad m) => (Free f ~> m) -> (f ~> Forget m)

fwd . bwd = id = bwd . fwd

如果我们删除 Forget s，对于 Control.Monad.Free 中的自由 monad我们有 fwd = foldFree和 bwd = (. liftF) (我认为？)

但是这些定律是如何导致 Control.Monad.Free 中发现的结构的？ ?你是怎么想出来的 data Free f a = Return a | Free (f (Free f a)) ?当然你不会只是猜测，直到你想出满足法律的东西吗？同样的问题也适用于图的自由范畴、集合的自由幺半群以及您想命名的任何其他自由对象。

Answer 1

我认为“免费”的概念并不像您认为的那样明确。虽然我确实认为普遍的共识是它确实是健忘仿函数的左伴随，但问题在于 "forgetful"方法。在一些范围广泛的情况下有明确的定义，特别是对于 concrete categories .

通用代数提供了涵盖几乎所有“代数”结构(集合)的广泛方法。结果给出了一个“签名”，它由排序、运算和方程组成，您可以构建运算的项代数(即 AST)，然后通过方程生成的等价关系对它进行商。这是从该签名生成的自由代数。例如，我们通常将幺半群称为配备有关联乘法和单位的集合。在代码中，商之前的自由代数将是:

data PreFreeMonoid a
  = Unit
  | Var a
  | Mul (PreFreeMonid a) (PreFreeMonoid a)

然后我们将通过从等式生成的等价关系来商:

Mul Unit x = x
Mul x Unit = x
Mul (Mul x y) z = Mul x (Mul y z)

但是您可以证明结果商类型与列表同构。在多重排序的情况下，我们会有一系列术语代数，每种类型一个。

明确地重新定义这一点的一种方法是使用 a(稍微概括)的概念 Lawvere theory .给定一个带有一组排序的签名，S，我们可以构建一个小类别，称为 电话 ，其对象是 S 的元素列表。这些小类别将被称为 理论一般来说。操作被映射到箭头，其源和目标对应于适当的参数。我们自由添加“元组”和“投影”箭头，例如[A,B,A] 变成 [A]×[B]×[A] 的乘积。最后，我们添加对应于签名中的每个方程的交换图(即箭头之间的方程)。此时， 电话 本质上代表术语代数。事实上，这个术语代数的实际解释或模型只是一个有限积保留仿函数 电话 → 套装 , 写 模组 ( T ) 用于来自 的有限积保留仿函数的类别电话 → 套装 .在单一排序的情况下，我们有一个底层的集合仿函数，但通常我们得到一个 S 索引的集合族，即我们有一个仿函数 U : 模组 ( T ) → 套装 S 在这里，我们将 S 视为一个离散类别。 U 就是 U(m)(s) = m([s])。我们实际上可以计算左伴随。首先，我们有一个由 S 的元素索引的集合族，称为 G。然后我们需要构建一个有限积保留仿函数 电话 → 套装 , 但任何仿函数变成 套装 (即 copresheaf )是 a colimit of representables在这种情况下，这意味着它是以下(相关)和类型的商:

Free(G)(s) = Σt:T.T(t,s)×Free(G)(t)

如果 Free(G) 是有限积保留，那么在 t = [A,B] 的情况下，例如，我们将有:

T([A,B],s)×Free(G)([A,B]) = T([A,B],s)×Free(G)([A])×Free(G)([B])

我们简单地为 S 中的每个 A 定义 Free(G)([A]) = G(A) 产生:

T([A,B],s)×Free(G)([A])×Free(G)([B]) = T([A,B],s)×G(A)×G(B)

总而言之，Free(G)([A]) 的元素由 的箭头组成。电话 进入 [A] 和与该箭头的来源相对应的适当集合的元素列表，即术语模方程的数量，使其行为合理并遵守签名中的方程，但我不打算详细说明在。对于幺半群的乘法，我们有一个箭头 m : [A,A] → [A] 这将导致一个元组 (m, x, y)，其中 x 和 y 是 G(A) 对应的元素像 m(x, y) 这样的术语.将这个定义重新定义为递归定义需要查看我们正在计算的方程。

还有其他一些事情需要验证来证明 Free ⊣ U 但这并不难。一旦完成，U∘Free 是 上的单子(monad)套装 S。

Lawvere 理论方法的好处在于它很容易以多种方式概括。一种直接的方法是替换 套装通过其他一些拓扑 E .实际上，有向多重图的范畴形成了一个拓扑，但我不相信你可以(轻松地)将范畴视为超过 的理论。图 .扩展 Lawvere 理论的另一个方向是考虑 doctrines除了有限乘积保持仿函数，特别是有限限保持仿函数，也就是 left exact or lex functors是一个有趣的点。小类别和有向多重图(分类者有时称之为 quivers)都可以被视为具有有限限制的类别的模型。有向多重图理论直接包含在小范畴理论中。这与逆变器相反，会产生一个仿函数 猫 → 图简单地通过预组合。 left adjoint of this然后(几乎)是 left Kan extensions沿着那个包容。这些左 Kan 扩展将出现在 套装所以最终它们只是colimits，它们只是(依赖)和类型的商。 (从技术上讲，您需要验证所产生的 Kan 扩展是有限极限保持的。图论的模型本质上是图论中的任意仿函数这一事实也对我们有所帮助。发生这种情况是因为图论仅由一元运算组成。)

尽管如此，这些都对免费 monad 没有帮助。然而，事实证明 one construction包含所有这些，包括自由 monad。回到通用代数，情况是每个没有方程的签名都会产生一个(多项式)仿函数，其 initial algebra是自由项代数。 Lambek's lemma建议并且很容易证明 the initial algebra is just colimit of repeated applications of the functor .上面的一般结果基于类似的方法，免费 monad 的相关案例是 unpointed endofunctor case ，在其中你开始看到 Free 的定义你给出的，但实际上要完全解决它需要展开许多结构。

不过，坦率地说，我很确定在 FP 世界中实际发生的事情如下。如果你看 PreFreeMonoid ，它实际上是一个免费的 monad。 PreFreeMonoid Void是幺半群签名(减去方程)将产生的仿函数的初始代数。如果您熟悉将仿函数用于初始代数，并且您甚至开始考虑通用代数，那么您几乎肯定会最终定义像 data Term f a = Var a | Op (f (Term f a)) 这样的类型。 .一旦你想提出这个问题，就很容易验证这是一个 monad。如果您甚至对 monad 与代数结构或术语替换之间的关系有些熟悉，那么您可能会很快提出这个问题。从编程语言实现的角度可以偶然发现相同的结构。如果你只是直接设定你的目标是在 Haskell 中导出自由 monad 结构，那么有几种直观的方法可以得到正确的定义，特别是结合一些等式/参数驱动的推理。事实上，“内仿函数范畴中的幺半群对象”是很有启发性的。

('真的希望这个 StackExchange 有 MathJax 支持。)