Forgetting Cofree annotations using a catamorphism

Question

I have an AST that I'm annotating using Cofree:

data ExprF a
  = Const Int
  | Add a
        a
  | Mul a
        a
  deriving (Show, Eq, Functor)

I use type Expr = Fix ExprF to represent untagged ASTs, and type AnnExpr a = Cofree ExprF a to represent tagged ones. I've figured out a function to transform tagged ASTs into untagged ones by throwing away all the annotations:

forget :: Functor f => Cofree f a -> Fix f
forget = Fix . fmap uncofree . unwrap

This looks like it might be some sort of catamorphism (I'm using the definition from Kmett's recursion-schemes package).

cata :: (Base t a -> a) -> t -> a
cata f = c where c = f . fmap c . project

I'd think the above rewritten using a catamorphism would look something like this, but I can't figure out what to put for alg to make it typecheck.

forget :: Functor f => Cofree f a -> Fix f
forget = cata alg where
  alg = ???

Any help figuring out if this really is a cata/anamorphism, and some intuition for why it is/isn't would be greatly appreciated.

Answer 1

import Data.Functor.Foldable (cata)
import Control.Comonad.Cofree (Cofree)
import Control.Comonad.Trans.Cofree as CofreeT (CofreeF(..))
import Data.Fix (Fix(..))

forget :: Functor f => Cofree f a -> Fix f
forget = cata (\(_ CofreeT.:< z) -> Fix z)

N.B.: be careful where Cofree and :< are imported from. One is from Control.Comonad.Cofree, the other from Control.Comonad.Trans.Cofree (as part of the CofreeF data type).

If you import Cofree from ....Trans.Cofree instead, the cata looks like this instead:

import Data.Functor.Identity (Identity(..))
import Data.Functor.Compose (Compose(..))
import Data.Functor.Foldable (cata)
import Control.Comonad.Trans.Cofree as CofreeT (Cofree, CofreeF(..))
import Data.Fix (Fix(..))

forget :: Functor f => Cofree f a -> Fix f
forget = cata (\(Compose (Identity (_ CofreeT.:< z))) -> Fix z)

Explanation

Looking only at the types, we can show that there is really only one way to implement forget. Let's start with the type of cata:

cata :: Recursive t => (Base t b -> b) -> t -> b

Here t ~ Cofree f a and the type instance of Base for Cofree gives:

type instance Base (Cofree f a) = CofreeF f a

Where CofreeF is:

data CoFreeF f a b = a :< f b
-- N.B.: CoFree also defines a (:<) constructor so you have to be
-- careful with imports.

i.e., a fancy pair type. Let's replace it with an actual pair type to make things clearer:

cata :: Functor f => ((a, f b) -> b) -> Cofree f a -> b

Now we're really specializing cata with a more concrete b, namely Fix f:

-- expected type of `cata` in `forget`
cata :: Functor f => ((a, f (Fix f)) -> Fix f) -> Cofree f a -> Fix f

forget is parametric in a and f, so the function we give cata can do nothing with the a in the pair, and the only sensible way to implement the remaining f (Fix f) -> Fix f is the Fix wrapper.

Operationally, Fix is the identity, so (\(_ :< z) -> Fix z) is really (\(_ :< z) -> z) which corresponds to the intuition of removing the annotation, i.e., the first component of the pair (_ :< z).