8

所以我知道一个自由对象被定义为一个附属物的左侧。但这如何引导您了解此类对象的 Haskell 定义？

更具体地说：给定一个从单子类别到内函子类别的“健忘函子”，

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

那么free 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

如果我们去掉Forgets，对于Control.Monad.Free我们拥有的自由单子fwd = foldFree和bwd = (. liftF)（我认为？）

但是这些法律是如何导致发现的Control.Monad.Free呢？你怎么想出来的data Free f a = Return a | Free (f (Free f a))？在你想出符合法律的东西之前，你肯定不会只是猜测吗？同样的问题也适用于图的自由类别、集合的自由幺半群以及您想命名的任何其他自由对象。

4

1 回答 1

5

我认为“免费”的概念并不像您所相信的那样定义明确。虽然我确实认为普遍的共识是它确实是健忘函子的左伴随物，但问题在于“健忘”的含义。在一些范围广泛的案例中有明确的定义，特别是对于具体的类别。

通用代数提供了一种范围广泛的方法，几乎​​涵盖了所有“代数”结构（过集）。结果得到一个“签名”，其中包含排序、运算和方程式，您构建运算的术语代数（即 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)

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

一种明确地改写它的方法是使用（稍微概括的）劳维尔理论的概念。给定具有一组排序S的签名，我们可以构建一个小类别，称为T，其对象是S的元素列表。这些小范畴统称为理论。操作被映射到其源和目标对应于适当的arities的箭头。我们自由地添加“tupling”和“projection”箭头，这样 [ A , B , A ] 就变成了 [ A ]×[ B ]×[ A]。最后，我们添加交换图（即箭头之间的方程）对应于签名中的每个方程。在这一点上，T本质上表示代数项。事实上，代数这个术语的实际解释或模型只是一个有限积保持函子T → Set ，对于来自T → Set的有限积保持函子的类别写Mod ( T ) 。在单排序的情况下，我们有一个底层集合函子，但通常我们得到一个S索引的集合族，即我们有一个函子U : Mod ( T ) → SetS我们在这里将S视为离散类别。U就是U (m)(s) = m([s])。我们实际上可以计算左伴随。首先，我们有一组由S的元素索引的集合，称为G。然后我们需要构建一个有限积保留函子T → Set，但任何进入Set的函子（即copresheaf）都是可表示的 colimit，在这种情况下，这意味着它是以下（相关）和类型的商：

自由( G )( s ) = Σ t : T。T ( t , s )×自由( G )( t )

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

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

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

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

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

还有其他事情需要验证来证明 Free ⊣ U但这并不难。一旦完成，U ∘Free 就是Set S上的一个单子。

Lawvere 理论方法的好处在于它很容易以多种方式进行概括。一种直接的方法是将Set替换为其他一些拓扑E。实际上，有向多重图的类别形成了一个拓扑，但我不相信您可以（轻松地）将类别视为Graph的理论。扩展 Lawvere 理论的另一个方向是考虑除有限乘积保持函子以外的学说，特别是有限限保持函子，即左精确函子或 lex 函子是一个有趣的观点。小类别和有向多重图（分类学家有时称之为颤动) 可以被视为具有有限限制的类别的模型。有向多图理论直接包含在小类别理论中。反过来，这仅通过预合成就可以诱导出函子cat → Graph 。然后（几乎）沿着该包含的左Kan 扩展。这些左 Kan 扩展将出现在Set中，因此最终它们只是 colimits，它们只是（相关）和类型的商。（从技术上讲，您需要验证所得到的 Kan 扩展是有限极限保持的。我们还受益于图论模型本质上是任意的这一事实图论中的函子。这是因为图论只包含一元运算。）

不过，这些都对免费的单子没有帮助。然而，事实证明，一种构造包含所有这些，包括自由单子。回到通用代数，每个没有方程的签名都会产生一个（多项式）函子，其初始代数是自由项代数。 Lambek 引理表明，很容易证明初始代数只是仿函数 重复应用的上界。上面的一般结果基于类似的方法，自由 monad 的相关案例是unpointed endofunctor case，在其中您开始看到Free您给出的定义，但实际上要完全解决它需要展开许多构造。

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

（'真的希望这个 StackExchange 支持 MathJax。）

于 2016-11-20T22:13:12.293 回答