36

我正在阅读http://www.haskellforall.com/2013/06/from-zero-to-cooperative-threads-in-33.html，其中抽象语法树派生为代表一组的函子的自由单子指示。我注意到自由单子Free与函子Fix上的定点运算符没有太大区别。

本文使用 monad 操作和do语法以简洁的方式构建这些 AST（固定点）。我想知道这是否是免费 monad 实例的唯一好处？它还支持其他有趣的应用程序吗？

4

2 回答 2

18

（注意，这结合了我的和@Gabriel 上面的评论。）

Fixa 的ed 点的每个居民都可能Functor是无限的，即let x = (Fix (Id x)) in x === (Fix (Id (Fix (Id ...))))是 的唯一居民Fix Identity。Free与 的直接不同之处在于Fix，它确保 至少有一个有限的居民Free f。事实上，如果Fix f有任何无限的居民，那么Free f就有无限多的有限居民。

这种无限性的另一个直接副作用Functor f => Fix f是不再是一个Functor。我们需要实现fmap :: Functor f => (a -> b) -> (f a -> f b)，但Fix已经“填补了所有的漏洞”，f a因为它曾经包含' a，所以我们不再有任何as 可以应用我们fmap的 'd 函数。

这对于创建Monads 很重要，因为我们想实施return :: a -> Free f a并拥有，比如说，这条定律成立fmap f . return = return . f，但它甚至在 a 中都没有意义Functor f => Fix f。

那么如何Free“修复”这些Fixed point 弱点呢？它用构造函数“增强”了我们的基础仿Pure函数。因此，对于所有Functor f，Pure :: a -> Free f a。这是我们保证成为有限类型的居民。它也立即为我们提供了一个良好的定义return。

return = Pure

因此，您可能会认为这种添加是取出Functor由 s 创建的嵌套 s 的潜在无限“树”Fix并混合一些“活”芽，由 表示Pure。我们使用它创建新的芽，return这可能被解释为以后“返回”到该芽并添加更多计算的承诺。事实上，这正是这样flip (>>=) :: (a -> Free f b) -> (Free f a -> Free f b)做的。f :: a -> Free f b给定一个可以应用于 types的“continuation”函数a，我们向下递归我们的树，返回到 eachPure a并将其替换为计算为 的 continuation f a。这让我们“长出”我们的树。

现在，Free显然比Fix. 要开车回家，可以将任何类型Functor f => Fix f视为相应的子类型Free f a！只需选择a ~ Void我们拥有的位置data Void = Void Void（即，无法构造的类型，是空类型，没有实例）。

为了更清楚，我们可以用 打破我们Fix的 'd Functor，break :: Fix f -> Free f a然后尝试用 反转它affix :: Free f Void -> Fix f。

break (Fix f) = Free (fmap break f) 
affix (Free f) = Fix (fmap affix f)

首先注意affix不需要处理这种Pure x情况，因为在这种情况下x :: Void并因此不能真正存在，所以Pure x很荒谬，我们将忽略它。

另请注意，break的返回类型有点微妙，因为该a类型仅出现在返回类型中Free f a，因此任何用户都无法访问break. “完全不可访问”和“无法实例化”给了我们第一个暗示，尽管类型affix和break是逆的，但我们可以证明它。

(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)

这应该显示（可能是共同归纳，或者只是直观地）这(break . affix)是一个身份。另一个方向以完全相同的方式通过。

所以，希望这表明这Free f比Fix f所有人都大Functor f。

那么为什么要使用Fix呢？好吧，有时您只需要 s 的属性，这是Free f Void由于 layering 的一些副作用f。在这种情况下，调用它Fix f可以更清楚地表明我们不应该尝试(>>=)或fmap超过类型。此外，因为Fix它只是一个newtype，编译器可能更容易“编译掉”层，Fix因为它无论如何只扮演语义角色。

  • 注意：我们可以更正式地讨论一下Void和forall a. a是同构类型，以便更清楚地看到affix和的类型是如何break和谐的。例如，我们有absurd :: Void -> aasabsurd (Void v) = absurd v和unabsurd :: (forall a. a) -> Voidas unabsurd a = a。但是这些有点傻。
于 2013-07-04T18:04:15.350 回答
10

有一种深刻而“简单”的联系。

这是伴随函子定理的结果，左伴随保留初始对象：L 0 ≅ 0.

明确地说，Free f是一个从一个范畴到它的 F 代数的函子（Free f与一个相反的健忘函子相伴而行）。在Hask中工作，我们的初始代数是Void

Free f Void ≅ 0

F-代数范畴的初始代数是Fix f：Free f Void ≅ Fix f

import Data.Void
import Control.Monad.Free

free2fix :: Functor f => Free f Void -> Fix f
free2fix (Pure void) = absurd void
free2fix (Free body) = Fix (free2fix <$> body)

fixToFree :: Functor f => Fix f -> Free f Void
fixToFree (Fix body) = Free (fixToFree <$> body)

类似地，右伴随（Cofree f，从Hask到 F- co代数范畴的函子）保留最终对象：R 1 ≅ 1。

在Hask 中这是单位：并且 F- co()代数的最终对象也是（它们在Hask中重合）所以我们得到：Fix fCofree f () ≅ Fix f

import Control.Comonad.Cofree

cofree2fix :: Functor f => Cofree f () -> Fix f
cofree2fix (() :< body) = Fix (cofree2fix <$> body)

fixToCofree :: Functor f => Fix f -> Cofree f ()
fixToCofree (Fix body) = () :< (fixToCofree <$> body)

看看定义有多相似！

newtype Fix f 
  = Fix (f (Fix f))

Fix f没有Free f变量。

data Free f a 
  = Pure a 
  | Free (f (Free f a))

Fix fCofree f带有虚拟值。

data Cofree f a 
  = a <: f (Cofree f a)
于 2017-04-04T09:21:37.600 回答