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

Question

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.

---

answer summary

---

@n.m. answered my first question by pointing out that in order for Haskell compiler to figure out Functor A is a fixed point of Functor B, we need to be explicit. In this case, it is

type List e = Fix (ListF e)

@luqui and @Will Ness pointed out that calling fmap (cata lenAlg) on the leaf, which is NilF in this case, will return NilF back, because of the definition of fmap.

-- f :: a -> b
fmap f (ConsF e a) = ConsF e (f b)
fmap f NilF        = NilF

I'd accept @n.m.'s answer as it directly addressed my first (bigger) question, but I do like all three answers. Thanks a lot for all your help!

Answer 1

"List is the fixed point of ListF" is a fast-and-loose figure of speech. While fast and loose reasoning is morally correct, you always need to keep in mind the boring correct thing. Which is as follows:

any least fixpoint of ListF e is isomorphic to [e].

Now "the compiler" (that's a fast-and-loose word for "the Haskell language" by the way) is not aware of isomorphisms of this kind. You can write isomorphic types all day

data []    x = []   | (:)   x ([]    x)    -- the imaginary built-in definition of []
data ListA x = NilA | ConsA x (ListA x)
data ListB x = NilB | ConsB x (ListB x)
data ListC x = NilC | ConsC x (ListC x)

and the compiler will never treat them as "the same type". Nor will it know that the fixpoint of ListF e is the same as [e], or indeed what a fixpoint is. If you want to use these isomorphisms, you need to teach the compiler about them by writing some code (e.g. by defining instances of Data.Types.Isomorphic), and then specifying the isomorphism explicitly each time you want to use it!

Having this is mind, let's look at cata you have defined. The first thing that mets the eye is that the attempt at defining the type signature is a syntax error. Let's remove it and just define the function in GHCi (I changed the name of the parameter to f to avoid confusion, and fixed a few typos in the definition of ListF)

Main> data ListF e a = NilF | ConsF e a
Main> let lenAlg :: ListF e Int -> Int
Main|     lenAlg (ConsF e n) = n + 1
Main|     lenAlg NilF = 0
Main|
Main>
Main> :m + Data.Fix
Main Data.Fix> cata f = f . fmap (cata f) . unFix
Main Data.Fix> :t cata
cata :: Functor f => (f b -> b) -> Fix f -> b
Main Data.Fix> :t cata lenAlg
cata lenAlg :: Functor (ListF e) => Fix (ListF e) -> Int

This says that in order to use lenAlg, you need to:

• define an instance of Functor for ListF e
• use Fix (ListF e) (which is a fixpoint of ListF) explicitly. Wishing "the fixpoint of ListF" into existence just doesn't work. There's no magic.

So let's do this:

Main Data.Fix> instance Functor (ListF e) where
Main Data.Fix|     fmap f NilF = NilF
Main Data.Fix|     fmap f (ConsF e a) = ConsF e (f a)
Main Data.Fix>
Main Data.Fix> :t cata lenAlg
cata lenAlg :: Fix (ListF e) -> Int

Great, now we can calculate the length of a ListF-based Fix-wrapped list. But let's define a few helper definitions first.

Main Data.Fix> type List e = Fix (ListF e)
Main Data.Fix> nil = Fix (NilF)
Main Data.Fix> let infixr 7 ~~                   -- using an infix operator for cons
Main Data.Fix|     h ~~ t = Fix (ConsF h t)
Main Data.Fix|
Main Data.Fix>
Main Data.Fix> myList = (1::Int) ~~ 2 ~~ 3 ~~ 4 ~~ nil
Main Data.Fix> :t myList
myList :: Fix (ListF Int)

Here's our "list" (a member of a type that is isomorphic to [Int] to be precise). Let's cata lenAlg it:

Main Data.Fix> cata lenAlg myList
4

Success!

Bottom line: the compiler knows nothing,you need to explain it everything.