Haskell cata types

Question

After reading (and implementing) part of http://blog.sumtypeofway.com/recursion-schemes-part-2/ I still wonder how the types in the cata function work. The cata function is defined as:

mystery :: Functor f => (f a -> a) -> Term f -> a
mystery f = f . fmap (mystery f) . unTerm

I have something like Term Expr. After unpacking I get Expr (Term Expr). The algebra (f) is defined e.g. as f :: Expr Int -> Int. I know I could call the following easily:

x = Literal "literal" :: Expr a
f :: Expr Int -> Int
f x :: Int

I can also imagine:

x = Literal "literal" :: Expr (Term Expr)
f :: Expr a -> Int
f x :: Int

But the following I suppose wouldn't work:

x = Literal "literal" :: Expr (Term Expr)
f :: Expr Int -> Int
f x :: ???

However, I still don't get how it works in the cata function - how do I get from Expr (Term Expr) to Expr a. I understand that the values do work, but I just don't get the types - what happens in the leaves of the tree? This is indeed a mystery...

Edit: I'll try to state more clearly what I don't understand.

Mentally, the cata seems to work this way:

• Apply fmap f to leaves.
• Now I have Expr Int and I can call fmap f to the node I have and get way up.

It doesn't obviously work this way as I am applying fmap (cata f). However, ultimately the function f gets called with Expr Int as an argument (in the leaves). How was this type produced from Expr (Term Expr) that it was before?

Answer 1

This is how cata operates on leaves.

Assume f :: Expr Int -> Int. Then:

cata f :: Term Expr -> Int
fmap (cata f) :: Expr (Term Expr) -> Expr Int

Now, for any function g :: a -> b, we have

fmap g :: Expr a -> Expr b
fmap g (Literal n) = Literal n
...

So, on literals, g is immaterial. This means that, choosing a ~ Term Expr, b ~ Int and g = cata f we have

fmap (cata f) (Literal n) = Literal n  :: Term Int
f (fmap (cata f) (Literal n)) = f (Literal n) :: Int

So, roughly, on leaves fmap (cata f) is a no-op, but it changes the type from Expr (Term Expr) to Expr Int. This is a trivial transformation since Literal n :: Expr a for any a.