# How does compiler figure out fixed point of a functor and how cata work at leaf level?

• A+
Category：Languages

I feel like understanding the abstract concept of fixed point of a functor, however, I am still struggling to figure out the exact implementation of it and its catamorphism in Haskell.

For example, if I define, as according to the book of "Category Theory for Programers" -- page 359, the following algebra

``-- (Int, LiftF e Int -> Int)  data ListF e a = NiLF | ConsF e a  lenAlg :: ListF e Int -> Int lenAlg (ConsF e n) -> n + 1 lenAlg NilF = 0 ``

by definition of catamorphism, the following function could be applied to ListF's fixed point, which is a List, to calculate its length.

``cata lenAlg :: [e] -> Int cata lenAlg = lenAlg . fmap (cata lenAlg) . unFix ``

I have two confusions. First, how does Haskell compiler know that List is THE fixed point of ListF? I know conceptually it is, but how does the compiler know, i.e., what if we define another List' that is everything the same as List, I bet compiler does not automatically infer that List' is the fixed point of ListF too, or does it? (I'd be amazed).

Second, due to the recursive nature of cata lenAlg, it always tries to unFix the outer layer of data constructor to expose the inner layer of functor (is this interpretation of mine even correct by the way?). But, what if we are already at the leaf, how could we invoke this function call?

``fmap (cata lenAlg) Nil ``

As an example, could someone help write an execution trace for the below function call to clarify?

``cata lenAlg Cons 1 (Cons 2 Nil) ``

I am probably missing something that is obvious, however I hope this question still makes sense for other people that share similar confusions.

The only way the compiler can know about the relationship between `ListF e` and `[e]` is if you tell it. You haven't provided enough context to answer exactly how, but I can infer that `unFix` has type

``unFix :: [e] -> ListF e [e] ``

that is, it unrolls the top layer. `unFix` may be more general, for example in `recursion-schemes` a type family is used to associate data types with their underlying functors. But this is where the two types are connected.

As for your second question, you need to be clearer about when you have a list and when you have a `ListF`. They are completely different.

``fmap (cata lenAlg) Nil ``

Here the functor you are mapping over is `ListF e` for whatever `e` you like. That is, it's this `fmap`:

``fmap :: (a -> b) -> ListF e a -> ListF e b ``

If you implement `instance Functor (ListF e)` yourself (always a good exercise) and get it to compile, you will find that `Nil` must map to `Nil`, so the `cata lenAlg` didn't matter at all.

Let's look at the type of `Cons 1 (Cons 2 Nil)`:

``Nil                 :: ListF e a Cons 2 Nil          :: ListF Int (ListF e a) Cons 1 (Cons 2 Nil) :: ListF Int (ListF Int (ListF e a)) ``

Something is awry here. The trouble is that we are forgetting to do the opposite of `unFix` to roll the `ListF` back up into a regular list. I will call this function

``roll :: ListF e [e] -> [e] ``

Now we have

``Nil                                      :: ListF e a roll Nil                                 :: [e] Cons 2 (roll Nil)                        :: ListF Int [Int] roll (Cons 2 (roll Nil))                 :: [Int] Cons 1 (roll (Cons 2 (roll Nil)))        :: ListF Int [Int] roll (Cons 1 (roll (Cons 2 (roll Nil)))) :: [Int] ``

The types are staying nice and small now, it's a good sign. For the execution trace, let's just note that `unFix . roll = id`, however they work. It's important here to notice that

``fmap f (Cons a b) = Cons a (f b) fmap f Nil        = Nil ``

That is, `fmap` on `ListF` just applies the function on the "recursive part" of the type.

I'm going to switch the `Cons` case to `lenAlg (ConsF e n) = 1 + n` to make the trace a tiny bit more readable. Still kind of a mess, good luck.

``cata lenAlg (roll (Cons 1 (roll (Cons 2 (roll Nil))))) (lenAlg . fmap (cata lenAlg) . unFix) (roll (Cons 1 (roll (Cons 2 (roll Nil))))) lenAlg (fmap (cata lenAlg) (unFix (roll (Cons 1 (roll (Cons 2 (roll Nil))))))) lenAlg (fmap (cata lenAlg) (Cons 1 (roll (Cons 2 (roll Nil))))) lenAlg (Cons 1 (cata lenAlg (roll (Cons 2 (roll Nil))))) 1 + cata lenAlg (roll (Cons 2 (roll Nil))) 1 + (lenAlg . fmap (cata lenAlg) . unFix) (roll (Cons 2 (roll Nil))) 1 + lenAlg (fmap (cata lenAlg) (unFix (roll (Cons 2 (roll Nil))))) 1 + lenAlg (fmap (cata lenAlg) (Cons 2 (roll Nil))) 1 + lenAlg (Cons 2 (cata lenAlg (roll Nil))) 1 + 1 + cata lenAlg (roll Nil) 1 + 1 + (lenAlg . fmap (cata lenAlg) . unFix) (roll Nil) 1 + 1 + lenAlg (fmap (cata lenAlg) (unFix (roll Nil))) 1 + 1 + lenAlg (fmap (cata lenAlg Nil)) 1 + 1 + lenAlg Nil 1 + 1 + 0 2 ``