40

我一直在玩Cofree，并不能完全了解它。

例如，我想Cofree [] Num在 ghci 中玩，却找不到任何有趣的例子。

例如，如果我构造一个 Cofree 类型：

let a = 1 :< [2, 3]

我希望extract a == 1，但我得到了这个错误：

No instance for (Num (Cofree [] a0)) arising from a use of ‘it’
    In the first argument of ‘print’, namely ‘it’
    In a stmt of an interactive GHCi command: print it

和一种：

extract a :: (Num a, Num (Cofree [] a)) => a

我能得到一些简单的例子，即使是微不足道的，关于如何使用 Cofree 和仿函数：[], or Maybe, or Either, 演示

  • extract
  • extend
  • unwrap
  • duplicate?

交叉发布：https ://www.reddit.com/r/haskell/comments/4wlw70/what_are_some_motivating_examples_for_cofree/

编辑：在 David Young 的评论的指导下，这里有一些更好的例子，说明我的第一次尝试被误导了，但是我仍然喜欢一些可以引导 Cofree 直觉的例子：

> let a = 1 :< []
> extract a
    1
> let b = 1 :< [(2 :< []), (3 :< [])]
> extract b
    1
> unwrap b
    [2 :< [],3 :< []]
> map extract $ unwrap b
    [2,3]
4

1 回答 1

61

让我们回顾一下Cofree数据类型的定义。

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

这至少足以用示例诊断问题。当你写

1 :< [2, 3]

您犯了一个小错误，该错误被报告得更巧妙，而不是有用。在这里，f = []anda是数字，因为1 :: a. 相应地你需要

[2, 3] :: [Cofree [] a]

因此

2 :: Cofree [] a

如果也Cofree [] a和Num. _ 因此，您的定义获得了一个不太可能满足的约束，实际上，当您使用您的值时，满足该约束的尝试会失败。

再试一次

1 :< [2 :< [], 3 :< []]

你应该有更好的运气。

现在，让我们看看我们有什么。从保持简单开始。是什么Cofree f ()？什么，特别是Cofree [] ()？后者与 的固定点同构[]：每个节点都是子树列表的树结构，也称为“未标记的玫瑰树”。例如，

() :< [  () :< [  () :< []
               ,  () :< []
               ]
      ,  () :< []
      ]

类似地，Cofree Maybe ()或多或少是Maybe: 自然数的副本的固定点，因为Maybe给了我们零或一个插入子树的位置。

zero :: Cofree Maybe ()
zero = () :< Nothing
succ :: Cofree Maybe () -> Cofree Maybe ()
succ n = () :< Just n

一个重要的小事是Cofree (Const y) ()，它是副本y。Const y函子没有给出子树的位置。

pack :: y -> Cofree (Const y) ()
pack y = () :< Const y

接下来，让我们忙于另一个参数。它会告诉您附加到每个节点的标签类型。重命名参数更具暗示性

data Cofree nodeOf label = label :< nodeOf (Cofree nodeOf label)

当我们标记(Const y)示例时，我们得到对

pair :: x -> y -> Cofree (Const y) x
pair x y = x :< Const y

当我们将标签附加到数字的节点时，我们会得到非空列表

one :: x -> Cofree Maybe x
one = x :< Nothing
cons :: x -> Cofree Maybe x -> Cofree Maybe x
cons x xs = x :< Just xs

对于列表，我们得到标记的玫瑰树。

0 :< [  1 :< [  3 :< []
             ,  4 :< []
             ]
     ,  2 :< []
     ]

这些结构总是“非空”的，因为至少有一个顶部节点，即使它没有子节点，并且该节点总是有一个标签。该extract操作为您提供顶部节点的标签。

extract :: Cofree f a -> a
extract (a :< _) = a

也就是说，extract丢弃顶部标签的上下文。

现在，该duplicate操作用自己的上下文装饰每个标签。

duplicate :: Cofree f a -> Cofree f (Cofree f a)
duplicate a :< fca = (a :< fca) :< fmap duplicate fca  -- f's fmap

我们可以通过访问整个树来获得一个Functor实例Cofree f

fmap :: (a -> b) -> Cofree f a -> Cofree f b
fmap g (a :< fca) = g a :< fmap (fmap g) fca
    --                     ^^^^  ^^^^
    --                 f's fmap  ||||
    --                           (Cofree f)'s fmap, used recursively

不难看出

fmap extract . duplicate = id

因为duplicate用它的上下文装饰每个节点，然后fmap extract扔掉装饰。

请注意，fmapgets 仅查看输入的标签来计算输出的标签。假设我们想根据上下文中的每个输入标签计算输出标签？例如，给定一棵未标记的树，我们可能希望用其整个子树的大小来标记每个节点。多亏了 的Foldable实例Cofree f，我们应该能够计算节点。

length :: Foldable f => Cofree f a -> Int

所以这意味着

fmap length . duplicate :: Cofree f a -> Cofree f Int

comonads 的关键思想是它们捕获“具有某些上下文的事物”，并且它们允许您在任何地方应用上下文相关的映射。

extend :: Comonad c => (c a -> b) -> c a -> c b
extend f = fmap f       -- context-dependent map everywhere
           .            -- after
           duplicate    -- decorating everything with its context

更直接地定义extend可以为您省去重复的麻烦（尽管这仅相当于共享）。

extend :: (Cofree f a -> b) -> Cofree f a -> Cofree f b
extend g ca@(_ :< fca) = g ca :< fmap (extend g) fca

你可以duplicate通过采取回来

duplicate = extend id -- the output label is the input label in its context

此外，如果您选择extract对每个标签在上下文中执行的操作，您只需将每个标签放回它的来源：

extend extract = id

这些“上下文标签操作”被称为“co-Kleisli 箭头”，

g :: c a -> b

的工作extend是将 co-Kleisli 箭头解释为整个结构上的函数。该extract操作是恒等Kleisli 箭头，它被解释extend为恒等函数。当然，还有一个 co-Kleisli 组成

(=<=) :: Comonad c => (c s -> t) -> (c r -> s) -> (c r -> t)
(g =<= h) = g . extend h

并且comonad法则确保它=<=是结合和吸收extract的，给了我们co-Kleisli范畴。此外，我们有

extend (g =<= h)  =  extend g . extend h

所以这extend是一个从 co-Kleisli 范畴到集合和函数的函子（在范畴意义上）。这些定律不难检查Cofree，因为它们遵循Functor节点形状的定律。

现在，在 cofree 共体中查看结构的一种有用方法是作为一种“游戏服务器”。一种结构

a :< fca

代表游戏的状态。游戏中的移动包括“停止”，在这种情况下，您会得到a，或“继续”，通过选择 的子树fca。例如，考虑

Cofree ((->) move) prize

该服务器的客户端必须停止或继续通过给出一个move: 它是一个s列表。move比赛进行如下：

play :: [move] -> Cofree ((->) move) prize -> prize
play []       (prize :< _) = prize
play (m : ms) (_     :< f) = play ms (f m)

也许 amove是 aChar而 theprize是解析字符序列的结果。

如果你足够用力地盯着，你会发现那[move]是Free ((,) move) (). 自由单子代表客户策略。函子((,) move)相当于一个命令接口，只有命令“send a move”。函子((->) move)是相应的结构“响应一个move”的发送。

有些函子可以看作是捕获一个命令接口；这种函子的自由单子代表发出命令的程序；函子将有一个“对偶”，表示如何响应命令；对偶的 cofree comonad 是生成命令的程序可以在其中运行的一般环境概念，标签说明如果程序停止并返回一个值该怎么办，子结构说明如果出现以下情况如何继续运行程序它发出命令。

例如，

data Comms x = Send Char x | Receive (Char -> x)

描述被允许发送或接收字符。它的对偶是

data Responder x = Resp {ifSend :: Char -> x, ifReceive :: (Char, x)}

作为一个练习，看看你是否可以实现交互

chatter :: Free Comms x -> Cofree Responder y -> (x, y)
于 2016-08-07T19:41:25.237 回答