问题描述
我正在阅读，其中抽象语法树是作为代表一组指令的函子的自由单子派生的。我注意到免费的monad 与函子上的fixpoint运算符没有多大区别。
本文使用monad操作和的 Fix code>无限，即 let x =（Fix（Id x））in x ===（Fix（Id（Fix（Id ...））））是 居民修复身份。 自由与 Fix 之间的差异在于确保至少有一个有限居民免费f 。事实上，如果 Fix f 有任何无限的居民，那么 Free f 有无限多的有限居民。
这个无界的另一个直接副作用是 Functor f =>修复f 不再是 Functor >。我们需要实现 fmap :: Functor f => （a - > b） - > （fa - > fb），但 Fix 在 fa 的c>，所以我们不再有任何 a s来应用我们的 fmap 'd函数。
这对于创建 Monad s非常重要因为我们想实现 return :: a - >免费f a 并且拥有，例如，这个法则保存 fmap f。返回=返回。 f ，但它在 Functor f =>修正f 。
那么 Free 如何修复这些修正编辑点缺陷？它用 Pure 构造函数扩充我们的基函子。因此，对于所有 Functor f ， Pure :: a - >免费f a 。这是我们保证有限的这种类型的居民。它也立即给我们一个行为良好的定义 return 。
return = Pure
所以你可能会想到这个附加操作会把嵌套的 Functor 由 Fix 创建，并混合一些有生命力的芽，由> Pure 。我们使用 return 创建新芽，这可能会被解释为稍后返回该芽的承诺并添加更多计算。事实上，这正是翻转（>> =）::（a - > Free f b） - > （Free f a - > Free f b）确实。给定一个延续函数 f :: a - >可以应用于类型 a 的免费fb ，我们将树返回到每个 Pure a 并将其替换为计算为 fa 的延续。这让我们增长我们的树。
现在，空闲显然比 Fix 更普遍。为了驱动这个家，可以看到任何类型的 Functor f =>将f 修正为相应的 Free f a 的子类型！只要选择 a〜Void 我们有数据Void = Void Void （即一个不能构造的类型，
为了使它更清楚，我们可以打破我们的 Fix 'd Functor s with break :: Fix f - >免费f a ，然后尝试用 affix反转它：Free f Void - >修正f 。
break（Fix f）= Free（fmap break f）
词缀（Free f）= Fix（fmap词缀f）
请注意， affix 不会需要处理 Pure x 的情况，因为在这种情况下 x :: Void 并且因此不能 be there，所以 Pure x 是荒谬的，我们会忽略它。 code> break 的返回类型有点微妙，因为 a 类型只出现在返回类型中， Free fa ，这样任何 break 的用户都无法访问它。 完全无法访问和无法实例化为我们提供了第一个提示，尽管类型为附加并且 break 我们可以证明这一点。
（break。affix）（免费f）
=== [定义词缀]
break（Fix（fmap affix f））
=== [break的定义]
Free（fmap break（fmap affix f））
== = [定义（。）]
自由（（fmap break。fmap affix）f）
=== [functor coherence laws]
Free（fmap（break。affix）f）
应该显示（可能是共同感应式或直觉式 （break。affix）是一个身份。另一个方向是以完全相同的方式。
所以，希望这表明 Free f 大于为所有 Functor f 修正f 。
那为什么要用 Fix ？那么，有时你只需要 Free f Void 的属性，这是由于分层 f s的某些副作用。在这种情况下，调用它 Fix f 可以更清楚地表明我们不应该尝试（>> =）或 fmap 。此外，由于 Fix 只是 newtype ，编译器可能更容易编译< Fix ，因为它只能扮演语义角色。
- 注意：我们可以更正式地讨论如何 Void 和全部a。一个是同构类型，以便更清楚地看到词缀和 break 的类型。是和谐的。例如，我们有 absurd :: Void - >一个为荒谬（Void v）=荒谬v 和 unabsurd ::（forall a。a） - > Void 为 unabsurd a = a 。但这些有点傻。
I was reading http://www.haskellforall.com/2013/06/from-zero-to-cooperative-threads-in-33.html where an abstract syntax tree is derived as the free monad of a functor representing a set of instructions. I noticed that the free monad Free is not much different from the fixpoint operator on functors Fix.
The article uses the monad operations and do syntax to build those ASTs (fixpoints) in a concise way. I'm wondering if that's the only benefit from the free monad instance? Are there any other interesting applications that it enables?
(N.B. this combines a bit from both mine and @Gabriel's comments above.)
It's possible for every inhabitant of the Fixed point of a Functor to be infinite, i.e. let x = (Fix (Id x)) in x === (Fix (Id (Fix (Id ...)))) is the only inhabitant of Fix Identity. Free differs immediately from Fix in that it ensures there is at least one finite inhabitant of Free f. In fact, if Fix f has any infinite inhabitants then Free f has infinitely many finite inhabitants.
Another immediate side-effect of this unboundedness is that Functor f => Fix f isn't a Functor anymore. We'd need to implement fmap :: Functor f => (a -> b) -> (f a -> f b), but Fix has "filled all the holes" in f a that used to contain the a, so we no longer have any as to apply our fmap'd function to.
This is important for creating Monads because we'd like to implement return :: a -> Free f a and have, say, this law hold fmap f . return = return . f, but it doesn't even make sense in a Functor f => Fix f.
So how does Free "fix" these Fixed point foibles? It "augments" our base functor with the Pure constructor. Thus, for all Functor f, Pure :: a -> Free f a. This is our guaranteed-to-be-finite inhabitant of the type. It also immediately gives us a well-behaved definition of return.
return = Pure
So you might think of this addition as taking out potentially infinite "tree" of nested Functors created by Fix and mixing in some number of "living" buds, represented by Pure. We create new buds using return which might be interpreted as a promise to "return" to that bud later and add more computation. In fact, that's exactly what flip (>>=) :: (a -> Free f b) -> (Free f a -> Free f b) does. Given a "continuation" function f :: a -> Free f b which can be applied to types a, we recurse down our tree returning to each Pure a and replacing it with the continuation computed as f a. This lets us "grow" our tree.
Now, Free is clearly more general than Fix. To drive this home, it's possible to see any type Functor f => Fix f as a subtype of the corresponding Free f a! Simply choose a ~ Void where we have data Void = Void Void (i.e., a type that cannot be constructed, is the empty type, has no instances).
To make it more clear, we can break our Fix'd Functors with break :: Fix f -> Free f a and then try to invert it with affix :: Free f Void -> Fix f.
break (Fix f) = Free (fmap break f) affix (Free f) = Fix (fmap affix f)
Note first that affix does not need to handle the Pure x case because in this case x :: Void and thus cannot really be there, so Pure x is absurd and we'll just ignore it.
Also note that break's return type is a little subtle since the a type only appears in the return type, Free f a, such that it's completely inaccessible to any user of break. "Completely inaccessible" and "cannot be instantiated" give us the first hint that, despite the types, affix and break are inverses, but we can just prove it.
(break . affix) (Free f) === [definition of affix] break (Fix (fmap affix f)) === [definition of break] Free (fmap break (fmap affix f)) === [definition of (.)] Free ( (fmap break . fmap affix) f ) === [functor coherence laws] Free (fmap (break . affix) f)
which should show (co-inductively, or just intuitively, perhaps) that (break . affix) is an identity. The other direction goes through in a completely identical fashion.
So, hopefully this shows that Free f is larger than Fix f for all Functor f.
So why ever use Fix? Well, sometimes you only want the properties of Free f Void due to some side effect of layering fs. In this case, calling it Fix f makes it more clear that we shouldn't try to (>>=) or fmap over the type. Furthermore, since Fix is just a newtype it might be easier for the compiler to "compile away" layers of Fix since it only plays a semantic role anyway.
- Note: we can more formally talk about how Void and forall a. a are isomorphic types in order to see more clearly how the types of affix and break are harmonious. For instance, we have absurd :: Void -> a as absurd (Void v) = absurd v and unabsurd :: (forall a. a) -> Void as unabsurd a = a. But these get a little silly.
这篇关于自由单子和函子固定点之间的区别？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！