自由物体是如何构建的？

所以我明白一个免费的对象被定义为一个副本的左侧。 但是，这是如何引导您了解这些对象的Haskell定义？

更具体地说：给予一个单子类型的“健忘的函数”到内生函数的范畴，

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 fa = Return a | Free (f (Free fa)) data Free fa = Return a | Free (f (Free fa)) ？ 当然，你不会猜测，直到你想出一些满足法律的东西吗？ 同样的问题也适用于图的自由类别，一个集合中的自由monoid，以及任何你关心的自由对象。

---

我不认为“自由”的概念与你似乎相信的一样明确。 虽然我认为普遍的共识是，它确实是一个健忘函子的左边伴随物，但问题在于“健忘”的含义。 在一些广泛的案例中有明确的定义，特别是对于具体类别。

通用代数提供了涵盖几乎所有“代数”结构（超过集合）的广泛范围的方法。 给出的结果是一个由签名组成的“签名”，它由类，操作和方程组成，你建立一个操作的术语代数（即AST），然后用等式生成的等式关系给它赋值。 这是从该签名生成的自由代数。 例如，我们通常将monoids作为一个装有关联乘法和单位的集合来讨论。 在代码中，商号之前的自由代数将是：

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 ，写出Mod （ T ）用于T → Set的有限乘积保留函数的范畴。 在单个排序的情况下，我们会有一个潜在的集合函数，但总的来说，我们得到一个S索引的集合，即我们有一个函数U： Mod （ T ）→ Set S，我们将S看作是离散类别在这里。 U仅仅是U（m）（s）= m（[s]）。 我们实际上可以计算左边的伴随。 首先，我们有一系列由S的元素索引的集合，称之为G.然后，我们需要构建一个保留函数T → Set的有限乘积，但是任何到Set （即copresheaf）中的函子都是可表达的集合，在这个集合中情况下，意味着它是以下（依赖）总和类型的商：

自由（G）（s）=Σt： T 。 T （t，s）×Free（G）（t）

例如，如果自由（G）是有限产品保留，那么在t = [A，B]的情况下，例如，我们有：

T（[A，B]，S）×免费（G）（[A，B]）= T（[A，B]，S）×免费（G）（[A]）×免费（G）（[ B]）

我们简单地定义S中每个A的自由（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]）的一个元素由T中的一个箭头到[A]，以及与该箭头的源相对应的适当集合的元素列表组成，即该元素的arity模方程式，使其表现合理，服从方程式，但我不打算详细说明。 对于一个幺半群的乘法，我们有一个箭头m：[A，A]→[A]，这将导致一个元组（m，x，y），其中x和y是G到像m(x, y)这样的术语。 将这个定义重新转换为递归的定义需要看看我们正在处理的方程式。

还有其他一些事情需要验证以显示Free＆dashv; ü但它并不太难。 一旦完成，U＆compfn; Free是Set S上的monad。

关于Lawvere理论方法的好处是很容易以多种方式推广。 一种简单的方法是用另一个topos E替换Set 。 事实上，有向多图的类型形成了一个topos，但我不认为你可以（很容易）将类视为关于Graph的理论。 延伸Lawvere理论的另一个方向是考虑除有限乘积保留函子之外的其他学说，特别是有限极限保留函子，左精确函数或lex函子是一个有趣的观点。 小分类和定向多图（这些分类有时称为颤抖）可以看作是具有有限极限的范畴的模型。 将有向多图的理论直接纳入小类理论。 这反过来导致一个函子猫 → 图形简单地通过预分解。 这个左边的伴随是（几乎）沿着这个包含的左边的Kan扩展。 这些左边的Kan扩展将出现在Set中，因此最终它们只是colimits，它们只是（依赖）求和类型的商。 （从技术上讲，您需要验证生成的Kan扩展是有限极限保持的，我们还得到了以下事实的帮助：图的理论模型基本上是图的理论中的任意函子，这是因为图的理论只包含一元操作。）

尽管如此，这对所有免费单人都没有帮助。 然而，事实证明，一个建筑包括所有这些包括免费monads。 回到通用代数，没有方程的每个签名都会产生一个（多项式）函子，其初始代数是自由项代数。 Lambek的引理指出，很容易证明初始代数只是仿函数的重复应用。 上面的总体结果是基于类似的方法，而免费单子的相关案例是未指明的endofunctor案例，在这个案例中，你开始看到你给出的Free的定义，但实际完成它的工作需要展开许多结构。

坦率地说，尽管如此，我非常确定在FP世界实际发生的事情如下。 如果你看PreFreeMonoid ，它实际上是一个免费的monad。 PreFreeMonoid Void是PreFreeMonoid Void函数的初始代数（减去方程）所引起的。 如果您熟悉初始代数的函子，并且您甚至开始考虑通用代数，那么您几乎可以肯定最终会定义类型data Term fa = Var a | Op (f (Term fa)) data Term fa = Var a | Op (f (Term fa)) 。 一旦你想问这个问题，很容易验证这是一个monad。 如果你甚至熟悉单子不得不代数结构或术语替代的关系，那么你可能会很快提出这个问题。 从编程语言实现的角度来看，也可能会遇到同样的结构。 如果你直接设定你的目标是在Haskell中获得免费的monad构造，有几种直观的方法可以得到正确的定义，特别是结合一些等式/参数驱动的推理。 事实上，“内部管理者类别中的单一对象”是非常具有启发性的。

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

链接地址: http://www.djcxy.com/p/37235.html

上一篇: How are free objects constructed?

下一篇: How to replace all roman numbers in a string for the arabic equivalent?