免费monad和仿函数的固定点之间的区别？

Question

我正在阅读http://www.haskellforall.com/2013/06/from-zero-to-cooperative-threads-in-33.html,其中抽象语法树派生为一个仿函数的自由monad,代表一组说明.我注意到,自由单子免费是不是来自固定点操作非常不同的仿函数修正.

本文使用monad操作和do语法以简洁的方式构建这些AST(fixpoints).我想知道这是免费monad实例的唯一好处吗？它还有其他有趣的应用程序吗？

Answer 1

(注意,这与我和@ 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,但它甚至没有意义Functor f => Fix f.

那么如何Free"修复"这些Fixed点缺陷呢？它使用Pure构造函数"扩充"我们的基础仿函数.因此,对于所有Functor f,Pure :: a -> Free f a.这是我们保证有限的类型居民.它还立即给我们一个良好的定义return.

return = Pure

因此,您可能会认为这个添加可能会消除由嵌入式Functors创建的嵌套s的潜在无限"树",Fix并混合在一些"活"芽中Pure.我们创建新的芽,使用return它可能被解释为一个承诺,以后"返回"到那个芽,并添加更多的计算.事实上,这正是flip (>>=) :: (a -> Free f b) -> (Free f a -> Free f b)如此.给定一个f :: a -> Free f b可以应用于类型的"continuation"函数a,我们递减返回到每个树的树,Pure a并用计算为的continuation替换它f a.这让我们"成长"了我们的树.

现在,Free显然比一般Fix.为了驾驶这个家,可以看到任何类型Functor f => Fix f作为相应的子类型Free f a!只需选择a ~ Void我们所拥有的位置data Void = Void Void(即,无法构造的类型,是空类型,没有实例).

为了使它更清楚,我们可以打破我们的Fix' Functors s 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呢？好吧,有时你只想要Free f Void由于分层fs的一些副作用而产生的属性.在这种情况下,调用它Fix f可以更清楚地表明我们不应该尝试(>>=)或fmap超过该类型.此外,因为Fix它只是一个newtype编译器可能更容易"编译"层,Fix因为它无论如何只扮演语义角色.

• 注意:我们可以更正式地讨论如何Void和forall a. a是同构类型,以便更清楚地看到类型affix和break和谐.例如,我们有absurd :: Void -> aas absurd (Void v) = absurd v和unabsurd :: (forall a. a) -> Voidas unabsurd a = a.但这些有点傻.

Answer 2

有一个深刻而"简单"的联系.

它是伴随仿函数定理的结果,左邻接保留了初始对象: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代数的最终目标也是Fix f(它们在Hask中重合),因此我们得到:Cofree 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 f是Cofree f虚拟值.

data Cofree f a 
  = a <: f (Cofree f a)