在Haskell中Cofree CoMonad有哪些激励性的例子？

Question

我一直在玩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有,比方说,函子:[],或者Maybe,或者Either,演示

• extract
• extend
• unwrap
• duplicate？

Cross发布: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]

Answer 1

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

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

这至少足以通过示例来诊断问题.你写的时候

1 :< [2, 3]

你做了一个小错误,报告的内容相当微妙而不是有用.在这里,f = []并且a是数字的东西,因为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扔掉装饰.

请注意,fmap只能查看输入的标签来计算输出的标签.假设我们想根据其上下文中的每个输入标签计算输出标签？例如,给定一个未标记的树,我们可能希望用整个子树的大小标记每个节点.多亏了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 arrows",

g :: c a -> b

并且工作extend是将共同的Kleisli箭头解释为整个结构的函数.该extract操作是身份co-Kleisli箭头,它被解释extend为身份函数.当然,有一个合作Kleisli组成

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

并且comonad法律确保=<=联合和吸收extract,给我们共同Kleisli类别.而且我们有

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

所以这extend是一个从共同Kleisli类别到集合和函数的仿函数(在分类意义上).这些定律并不难检查Cofree,因为它们遵循Functor节点形状的定律.

现在,在cofree comonad中查看结构的一种有用方法是作为一种"游戏服务器".一个结构

a :< fca

代表游戏的状态.游戏中的一个动作包括"停止",在这种情况下你a通过选择一个子树来获得或"继续" fca.例如,考虑一下

Cofree ((->) move) prize

对于此服务器的客户端必须停止,或给予继续move:这是一个列表的move秒.游戏如下:

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

也许a move是a Char并且prize是解析字符序列的结果.

如果你足够努力,你会发现这[move]是一个版本Free ((,) move) ().免费monad代表客户策略.仿函数((,) move)相当于一个只带命令"send a move" 的命令接口.仿函数((->) move)是相应的结构"响应发送move".

一些仿函数可以被视为捕获命令接口; 这种仿函数的免费monad代表了制作命令的程序; 仿函数将具有"双重",表示如何响应命令; 双重的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)