14

为了清楚起见，我不是在谈论free monad 看起来很像应用于 functorFree f的定点组合器，即基本上是f. （并不是说这不有趣！）

我所说的是 的定点，即与自身同构的Free, Cofree :: (*->*) -> (*->*)函子。fFree ff

背景：今天，为了巩固我对自由 monad 相当缺乏的理解，我决定只为不同的简单函子写一些它们，forFree和forCofree，看看它们会同构到哪些更知名的 [co] monad . 令我特别感兴趣的是与（意思是，将任何类型映射到无人居住的函子）同构的发现。Cofree EmptyEmptyConst Void好吧，也许这只是愚蠢的——我发现如果你把空垃圾放进去，你就会把空垃圾拿出来，是的！——但是，嘿，这是范畴论，整个宇宙从看似微不足道的事物中升起……对吧？

直接的问题是，如果Cofree有这样一个固定点，那么Free呢？好吧，它当然不可能Empty，因为那不是单子。快速嫌疑人将是附近的东西，例如Const ()or Identity，但不是：

Free (Const ()) ~~ Either () ~~ Maybe
Free Identity   ~~ (Nat,)    ~~ Writer Nat

事实上，Free总是添加一个额外的构造函数的事实表明，任何作为不动点的函子的结构都必须已经是无限的。但奇怪的是，如果Cofree有这样一个简单的固定点，Free应该只有一个更复杂的固定点（就像FixFree a = C (Free FixFree a)Reid Barton 在评论中提出的修复）。

无聊的事实只是Free没有“偶然的固定点”，只是巧合而已Cofree，还是我错过了什么？

4

2 回答 2

5
于 2016-12-17T22:45:53.040 回答
1

既然你问了 的不动点的结构Free，我将勾勒出一个非正式的论点，它Free只有一个不动点是 a Functor，即类型

newtype FixFree a = C (Free FixFree a)

里德巴顿描述的。事实上，我提出了一个更强有力的主张。让我们从几个部分开始：

newtype Fix f a = Fix (f (Fix f) a)
instance Functor (f (Fix f)) => Functor (Fix f) where
  fmap f (Fix x) = Fix (fmap f x)

-- This is basically `MFunctor` from `Control.Monad.Morph`
class FFunctor (g :: (* -> *) -> * -> *) where
  hoistF :: Functor f => (forall a . f a -> f' a) -> g f b -> g f' b

尤其，

instance FFunctor Free where
  hoistF _f (Pure a) = Pure a
  hoistF f (Free fffa) = Free . f . fmap (hoistF f) $ fffa

然后

fToFixG :: (Functor f, FFunctor g) => (forall a . f a -> g f a) -> f a -> Fix g a
fToFixG fToG fa = Fix $ hoistF (fToFixG fToG) $ fToG fa

fixGToF :: forall f b (g :: (* -> *) -> * -> *) .
           (FFunctor g, Functor (g (Fix g)))
        => (forall a . g f a -> f a) -> Fix g b -> f b
fixGToF gToF (Fix ga) = gToF $ hoistF (fixGToF gToF) ga

如果我没记错的话（我可能是这样），将f和之间的同构的每一边传递g f给这些函数中的每一个将产生 and 之间的同构的每f一边Fix g。替换Free将g证明该声明。当然，这个论点是非常摇摆不定的，因为 Haskell 是不一致的。

于 2016-12-19T06:59:11.563 回答