Deriving a monad from a cofree comonad

Question

Edward Kmett writes on his blog that using the Co newtype (from the kan-extensions package), it's possible to derive a Monad from any Comonad. I'd like to learn how to mechanically do this for any Cofree f a, as for some Cofree types I don't know a different way to get a monad instance in a fool-proof way. For example the data type

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

is isomorphic to

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

and I find that type interesting as it can't be modeled as a Free monad, and also isn't Representable. My understanding is that Co Tree is also isomorphic to Tree, and has a monad instance. Phil Freeman has used Co extensively in his comonadic UI libraries, so it must be useful. In "Declarative UIs are the Future — And the Future is Comonadic!", he mentions:

In fact, under certain conditions on f, the Co (Cofree f) monad is isomorphic to a free monad which is determined by f.

While I could play type tetris to write functions to go between the two types, I'm not confident that that would necessarily lead to the correct implementation.

Answer 1

Out of the many possible angles for approaching your question, let's begin by having a closer look at Co Tree. Stripping the newtype wrappers and CoT machinery leaves us with the following isomorphism:

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

Now, what is a forall r. Tree (a -> r) -> r function like? If we are to obtain an r value, of whose type we have no prior knowledge, out of a Tree (a -> r), we need to have an a value (to which we can apply an a -> r function) and to choose a position in the tree (from which we will get said function). This suggests Co Tree a, rather than being isomorphic to Tree a, amounts to a tree position and a value. To confirm that, we can try to work out an isomorphism.

Tree positions can be expressed as a path from the root. For the sake of expediency, I'll use [Bool], with False and True standing for climbing the left and right branches respectively:

type Path = [Bool]

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

One potential complication is that, since the trees have variable size, indexing by tree positions is, in principle, not total. In this case, though, we can sneak out of trouble by returning whatever value is found in a leaf, even if there would be extra steps to take according to the supplied path:

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

Tree is, in some sense, almost representable. In particular, flip bring is surjective but not injective: it would be an adequate index weren't it for the handling of leaves, which are treated as if they were infinitely repeating subtrees.

bring allows us to have one direction of the isomorphism, in the manner outlined at the start of this answer:

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

As for the other direction, we can recover path and value out of a Co Tree a by feeding it specially crafted trees:

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, then, is isomorphic to Node, which in turn is isomorphic to (,) [Bool]. This suggests the monad instance of Co Tree should be equivalent to writer on the [Bool] monoid, and indeed sending return and (>>=) through the isomorphism confirms that.

This understanding of Co Tree in terms of positions in the "almost representable" Tree squares nicely with how it goes for actually representable comonads. If w is a representable comonad, there is a monoid m such that:

w ~ Traced m ~ (->) m

And therefore:

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

That is, if w is a representable comonad, Co w is isomorphic to the writer monad that is its left adjoint, and which can be taken to represent a specific site in the representable structure. As far as I can tell, the uses of Co in the Phil Freeman library you mention are in a similar spirit ("We can use Co w to explore the state space").

---

With all this discussion of Co, up to now I didn't get to consider a monad instance for Tree. It turns out Tree is a monad, with an instance given by the Cofree isomorphism. The relevant instance is Alternative f => Monad (Cofree f). It is a pretty interesting instance, actually: in Branch a l r >>= f, l and r are ignored unless f a is a leaf, in which case they will be used as a fallback to provide the subtrees:

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)

That is quite different from the usual concat-like monad instances for list-like and tree-like types. As a final illustration, we can see how the Monad instance for Cofree gives rise to a distinct non-empty list 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)