Free和Cofree的定点函子

Question

为了说清楚,我不是在谈论自由monad看起来很像一个应用于仿函数的固定点组合器,即Free f基本上是一个固定点f.(不是说这不好玩!)

我正在谈论的是固定点Free, Cofree :: (*->*) -> (*->*),即仿函数f,使得Free f同构于f自身.

背景:今天,坚定了我对自由的单子,而缺乏把握,我决定只写了他们的出来不同的简单仿函数,既为Free与对Cofree,看看有什么更好的知名[合作]单子他们会在同构.是什么吸引了我特别的是发现那Cofree Empty是同构的Empty(意思是,Const Void的任何类型映射到无人居住的仿函数).好吧,也许这只是愚蠢 - 我发现如果你把空垃圾放进去,你就会把空垃圾拿出来,是的! - 但是,嘿,这是类别理论,整个宇宙从看似琐碎的事物中崛起......对吧？

当前的问题是,如果Cofree有这样一个固定点,那又怎么样Free？嗯,它当然不能是Empty那不是一个单子.快速嫌疑人将附近的东西像Const ()或者Identity,但没有:

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

实际上,Free总是添加额外构造函数的事实表明,任何一个固定点的仿函数的结构必须已经是无限的.但似乎奇怪的是,如果Cofree有这样一个简单的定点,Free应该只有一个更复杂的定义点(就像FixFree a = C (Free FixFree a)Reid Barton在评论中提出的修建一样).

是无聊的真相只是Free有没有 "偶然固定点",这是一个偶然的巧合的是Cofree有一个,还是我失去了一些东西？

Answer 1

你的观察Empty是一个固定点Cofree(在Haskell中并不是真的,但我想你想在一些忽略的模型中工作?,比如Set)归结为这样的事实:

有一个集合E(空集),使得对于每个集合X,投影p 2:X×E - > E是同构.

我们可以说在这种情况下,E是产品的吸收对象.对于任何带有产品的C类,我们可以用"C对象"替换"set"这个词,我们得到一个关于C的陈述,可能是也可能不是.对于Set,它恰好是真的.

如果我们选择C = Set ^op,它也有产品(因为Set有副产品),然后将语言二元化再次讨论集合,我们得到声明

有一个集合F,使得对于每个集合Y,包含i 2:F - > Y + F是同构.

显然,对于任何集合F,这个陈述都不正确(我们可以选择任何非空集Y作为任何F的反例).毫无疑问,毕竟Set ^op与Set不同.

所以,我们不会得到一个"平凡的固定点" Free在我们得到一个以同样的方式Cofree,因为集^运是从设置有质的不同.Set的初始对象是产品的吸收元素,但Set的终端对象不是副产品的吸收对象.

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

Haskell程序员之间有很多关于哪些结构是其他结构的"对偶"的讨论.大多数情况在正式意义上毫无意义,因为在类别理论中,将建筑工程二元化如下:

假设我有一个我可以对任何C类(或任何具有某些额外结构和/或属性的类别)执行的构造.然后C类的双重结构是相反类别C ^op的原始结构(如果有的话,最好具有我们需要的额外结构和属性).

例如:产品的概念在任何类别C中都有意义(尽管产品可能并不总是存在),通过通用属性定义产品.为了在C中获得副产品的双重概念,我们应该问一下C ^op中的产品是什么,我们刚刚定义了任何类别的产品,所以这个概念是有道理的.

将二元性应用于Haskell设置的麻烦在于,Haskell语言绝大多数只讨论Hask,我们在其中进行构造.这引发了关于二元性的两个问题:

• 为了获得如上所述的结构的双重性,我应该能够在任何类别或至少任何类别的特定形式中进行构造.因此,我们必须首先概括构造,通常,我们只在类别Hask中完成更大类别的构造.(并且已经这样做了,除了Hask ^op之外,还有许多其他有趣的类别我们可以解释所产生的概念,例如Kleisli monad类别.)

• Hask类别享有许多特殊属性,可以通过说(忽略?)Hask是笛卡尔闭合类别来概括.例如,这意味着初始对象是产品的吸收对象.Hask ^op没有这些属性,这意味着广义概念在Hask ^op中可能没有意义; 并且它也意味着在Hask中恰好相同的两个概念通常是不同的,并且具有不同的对偶.

以后者为例,拍摄镜片.在哈斯克,他们可以通过多种方式构建; 两种方式是getter/setter对和costatebras for costate comonad.前者推广到带有产品的类别,第二个推广到以Hask为特定方式的类别.如果我们将前一个构造应用于Hask ^op然后我们得到棱镜,但如果我们将后一个构造应用于Hask ^op,那么我们得到状态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的特殊功能)是一个创造性的过程,而不是机械过程.

在像你这样的问题中,以及许多其他喜欢它的问题,很明显双重意义是什么意思,仍然没有理由期望双重结构实际存在或具有与原始相同的属性的先验,因为Hask ^op定性表现与Hask完全不同.口号可能是

类别理论是自我对偶的,但任何特定范畴的理论都不是!

Answer 2

既然您询问了 的不动点的结构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给每个函数将产生f和之间的同构的每一边Fix g。替换将证明该主张Free。g当然，这个论点非常不切实际，因为 Haskell 是不一致的。