Free 和 Cofree 的不动点函子

The fixed point functors of Free and Cofree

为了说明这一点,我不是在谈论 free monad looks a lot like a fixpoint combinator applied to a functor,即 Free f 基本上是 f 的不动点。 (并不是说这不有趣!)

我说的是 Free, Cofree :: (*->*) -> (*->*) 的不动点,即函子 f 使得 Free f 同构于 f 本身。

背景:今天,为了巩固我对自由 monad 的相当缺乏的掌握,我决定只为不同的简单仿函数写出其中的一些,for Free and for Cofree and see what better-known [co]monads they'd be isomorphic to. What intrigued me particularly was the discovery that Cofree Empty is isomorphic to Empty(意思是,Const Void,将任何类型映射到无人居住的函子)。好吧,也许这很愚蠢——我发现如果你把空垃圾放进去,你就会得到空垃圾,是的! – 但是,嘿,这是范畴论,整个宇宙都是从看似微不足道的事物中崛起的……对吧?

直接的问题是,如果Cofree有这样一个不动点,那么Free呢?好吧,它肯定不能是 Empty 因为那不是 monad。快速怀疑是附近的东西,如 Const ()Identity,但不是:

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

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

无聊的事实只是 Free 没有 “意外不动点” 而 Cofree 有一个只是巧合,还是我遗漏了什么?

你观察到 EmptyCofree 的不动点(这在 Haskell 中不是真的,但我猜你想在忽略 ,就像 Set) 归结为

there is a set E (the empty set) such that for every set X, the projection p₂ : X × E -> E is an isomorphism.

在这种情况下,我们可以说 E 是产品的吸收对象。我们可以用产品的任何类别 C 将单词“集合”替换为“C 的对象”,然后我们得到关于 C 的陈述可能是正确的,也可能不是正确的。对于Set,恰好为真。

如果我们选择 C ​​= Setop,它也有积(因为 Set 有余积),然后将语言对偶化以再次讨论集合,我们得到语句

there is a set F such that for every set Y, the inclusion i₂ : F -> Y + F is an isomorphism.

显然,这个说法对任何集合F都不成立(我们可以选择任何非空集合Y作为任何F的反例)。这并不奇怪,毕竟 Setop 与 Set.

是不同的类别

因此,我们不会像 Cofree 那样得到 Free 的“平凡不动点”,因为 Setop 与 Set 有质的区别。 Set的初始对象是乘积的吸收元素,但Set的终结对象不是副积的吸收对象。


如果我可以上我的肥皂盒一会儿:

Haskell 程序员之间有很多关于哪些构造是哪些其他构造的“对偶”的讨论。其中大部分在形式上是毫无意义的,因为在范畴论中二元化一个结构是这样的:

Suppose I have a construction which I can perform on any category C (or any category with certain extra structure and/or properties). Then the dual construction on a category C is the original construction on the opposite category Cop (which had better have the extra structure and properties we needed, if any).

例如:通过通用 属性 定义产品,产品的概念在任何类别 C 中都有意义(尽管产品可能并不总是存在)。要在 C 中获得余积的对偶概念,我们应该问 Cop 中的积是什么,我们刚刚定义了任何类别中的积,所以这个概念是有道理的。

将对偶性应用于 Haskell 设置的问题在于 Haskell 语言压倒性地更喜欢只谈论一个类别,Hask,我们在其中进行构造。这导致谈论二元性的两个问题:

  • 要获得上述构造的对偶,我应该能够在任何类别中进行构造,或者在至少任何特定形式的类别。因此,我们必须首先将通常只在类别 Hask 中完成的构造概括为更大的 class 类别。 (这样做之后,除了 Haskop,还有许多其他有趣的类别我们可以潜在地解释由此产生的概念,例如单子的 Kleisli 类别。)

  • Hask 范畴享有许多特殊性质,可以概括为(忽略)Hask 是笛卡尔闭范畴。例如,这意味着初始对象是产品的吸收对象。 Haskop没有这些性质,这意味着广义的概念在Haskop中可能没有意义;这也可能意味着在 Hask 中碰巧等价的两个概念通常是不同的,并且具有不同的对偶。

以镜头为例。在 Hask 中,它们可以通过多种方式构建;两种方式是根据 getter/setter 对和作为 Coalgebra 的 Comonad。前者概括为包含产品的类别,第二个概括为通过 Hask 以特定方式丰富的类别。如果我们将前一个构造应用到 Haskop 然后我们得到棱镜,但是如果我们将后一个构造应用到 Haskop 然后我们得到代数state monad 和这些不是一回事。

一个更熟悉的例子可能是 comonads:从以 Haskell 为中心的展示开始

return :: a -> m a
(>>=) :: m a -> (a -> m b) -> m b

似乎需要一些洞察力来确定要反转哪些箭头才能获得

extract :: w a -> a
extend :: w a -> (w b -> a) -> w b

关键是从 join :: m (m a) -> m a 开始比 (>>=) 更容易;但是找到这种替代表示(由于 Hask 的特殊功能而等效)是一个创造性的过程,而不是机械的过程。

在像您这样的问题以及许多其他类似问题中,双重含义的含义非常清楚,但仍然绝对没有理由先验地期望双重构造实际存在或具有相同的属性和原来的一样,因为 Haskop 在性质上与 Hask 有很大不同。口号可能是

the theory of categories is self-dual, but the theory of any particular category is not!

既然你问的是Free的不动点的结构,那我就粗略地概括一下,Free只有一个不动点,就是Functor , 即类型

newtype FixFree a = C (Free FixFree a)

Reid Barton 所描述的。事实上,我提出了一个更有力的主张。让我们从几件开始:

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

如果我没记错(我可能是),将 fg f 之间的同构的每一边传递给这些函数中的每一个将产生 [= 之间的同构的每一边=17=] 和 Fix g。将 Free 替换为 g 将证明该声明。当然,这个论点非常牵强,因为Haskell不一致。