从 cofree comonad 派生 monad

Question

Edward Kmett在他的博客中写道，使用 newtype Co（来自 kan-extensions 包），可以从任何 Comonad 派生出 Monad。我想学习如何机械地为 any 执行此操作Cofree f a，对于某些 Cofree 类型，我不知道以万无一失的方式获取 monad 实例的不同方法。例如数据类型

\n

data Tree a = Leaf a | Branch a (Tree a) (Tree a)\n

\n

同构于

\n

type Tree\' = Cofree (Compose Maybe V2)    -- V2 from `linear` package\n

\n

我发现这种类型很有趣，因为它不能建模为自由单子，而且也不可表示。我的理解是它Co Tree也与 Tree 同构，并且有一个 monad 实例。Phil Freeman 在他的共生 UI 库Co中广泛使用，因此它一定很有用。在“声明式 UI 是未来 \xe2\x80\x94 未来是 Comonadic！” 中，他提到：

\n

\n

事实上，在 f 的某些条件下，Co (Cofree f) 单子与由 f 决定的自由单子是同构的。

\n

\n

虽然我可以玩俄罗斯方块类型来编写在两种类型之间切换的函数，但我不确定这一定会导致正确的实现。

\n

Answer 1

在解决您的问题的许多可能的角度中，让我们首先仔细研究一下Co Tree。剥离新型包装和CoT机械给我们留下以下同构：

Co Tree a ~ forall r. Tree (a -> r) -> r

现在，forall r. Tree (a -> r) -> r函数是什么样的？如果我们要从 a 中获取一个r我们对其类型没有先验知识的值Tree (a -> r)，我们需要有一个a值（我们可以对其应用a -> r函数）并选择树中的一个位置（从中我们将得到说的功能）。这表明Co Tree a相当于Tree a一个树位置和一个值，而不是同构于 。为了证实这一点，我们可以尝试计算出同构。

树位置可以表示为从根开始的路径。为了方便起见，我将分别使用[Bool]、 withFalse和TrueStanding 来攀登左右分支：

type Path = [Bool]

data Node a = Node Path a
    deriving (Eq, Ord, Show, Functor)

一个潜在的复杂性是，由于树的大小可变，因此原则上按树位置进行索引并不是全部。不过，在这种情况下，我们可以通过返回在叶子中找到的任何值来摆脱麻烦，即使根据提供的路径需要采取额外的步骤：

bring :: Path -> Tree a -> a
bring (b : bs) (Branch _ l r) = bring bs (if b then r else l)
bring _ t = extract t

Tree从某种意义上说，这几乎是具有代表性的。特别是，flip bring它是满射的，但不是单射的：index对于处理叶子来说，这已经足够了，叶子被视为无限重复的子树。

bring允许我们以本答案开头概述的方式获得同构的一个方向：

fromNode :: Node a -> Co Tree a
fromNode (Node path a) = co $ \t -> bring path t a

至于另一个方向，我们可以Co Tree a通过向 a 提供特制的树来恢复 a 的路径和值：

toNode :: Co Tree a -> Node a
toNode k = Node (reverse (runCo k revPaths)) (runCo k (Leaf id))
    where
    revPaths = unfoldTree steps []
    steps bs = (const bs, Just (False : bs, True : bs))

unfoldTree :: (s -> (a, Maybe (s, s))) -> s -> Tree a
unfoldTree f s = case f s of
    (a, Nothing) -> Leaf a
    (a, Just (l, r)) -> Branch a (unfoldTree f l) (unfoldTree f r)

Co Tree，那么， 同构于Node， 又同构于(,) [Bool]。这表明 的 monad 实例Co Tree应该相当于幺半群上的 writer ，并且确实通过同构[Bool]发送return和证实了这一点。(>>=)

这种对Co Tree“几乎可表示”位置的理解Tree与它对实际可表示的共形体的理解非常吻合。如果w是一个可表示的共形体，则存在一个幺半群，m使得：

w ~ Traced m ~ (->) m

因此：

Co w a
~ forall r. (m -> (a -> r)) -> r
~ forall r. ((m, a) -> r) -> r
~ (m, a)

也就是说， ifw是一个可表示的comonad，Co w与作为其左伴随的writer monad 同构，并且可以用来表示可表示结构中的特定位点。据我所知，Co您提到的 Phil Freeman 库中的用途具有类似的精神（“我们可以用来Co w探索状态空间”）。

经过所有这些关于 的讨论Co，到目前为止我还没有考虑 的 monad 实例Tree。事实证明这Tree是一个单子，有一个由同构给出的实例Cofree。相关实例是Alternative f => Monad (Cofree f). 实际上，这是一个非常有趣的实例： in 和Branch a l r >>= f除非l是叶子，r否则将被忽略f a，在这种情况下，它们将用作提供子树的后备：

pattern JustV2 x y = Compose (Just (V2 x y))
pattern NoV2 = Compose Nothing

toCof :: Tree a -> Cofree (Compose Maybe V2) a
toCof = \case
    Leaf a -> a :< NoV2
    Branch a l r -> a :< JustV2 (toCof l) (toCof r)

fromCof :: Cofree (Compose Maybe V2) a -> Tree a
fromCof (a :< ts) = case ts of
    NoV2 -> Leaf a
    JustV2 l r -> Branch a (fromCof l) (fromCof r)

instance Applicative Tree where
    pure = Leaf
    (<*>) = ap

instance Monad Tree where
   t >>= f = fromCof (toCof t >>= toCof . f)

test_fun :: Integer -> Tree Integer
test_fun x = if x > 0 then Branch x (Leaf (2*x)) (Leaf (4*x)) else Leaf x

ghci> Branch 0 (Leaf 2) (Leaf 3) >>= test_fun
Branch 0 (Branch 2 (Leaf 4) (Leaf 8)) (Branch 3 (Leaf 6) (Leaf 12))
ghci> Branch 7 (Leaf 2) (Leaf 3) >>= test_fun
Branch 7 (Leaf 14) (Leaf 28)

concat这与通常的类列表和类树类型的 monad 实例有很大不同。作为最后一个例子，我们可以看到Monadfor 的实例如何Cofree产生一个独特的非空列表 comonad：

test_fun' :: Integer -> NonEmpty Integer
test_fun' x = if x > 0 then x :| [4*x] else pure x

-- Cofree Maybe ~ NonEmpty
test_fun'' :: Integer -> Cofree Maybe Integer
test_fun'' x = if x > 0 then x :< Just (4*x :< Nothing) else pure x

ghci> 0 :| [-1, 3, 5] >>= test_fun'
0 :| [-1,3,12,5,20]
ghci> 0 :< Just (-1 :< Just (3 :< Just (5 :< Nothing))) >>= test_fun''
0 :< Just (-1 :< Just (3 :< Just (12 :< Nothing)))
ghci> 7 N.:| [-1, 3, 5] >>= test_fun'
7 :| [28,-1,3,12,5,20]
ghci> 7 :< Just (-1 :< Just (3 :< Just (5 :< Nothing))) >>= test_fun''
7 :< Just (28 :< Nothing)