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 

See also my other answer about catamorphisms.

Comment

:?: :razz: :sad: :evil: :!: :smile: :oops: :grin: :eek: :shock: :???: :cool: :lol: :mad: :twisted: :roll: :wink: :idea: :arrow: :neutral: :cry: :mrgreen: