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:
fmap f to leaves. 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?
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.