haskellcategory-theoryrecursion-schemesfixpoint-combinatorscatamorphism# How does compiler figure out fixed point of a functor and how cata work at leaf level?

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!

Solution

"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.

- Comparing lists in Haskell
- Is there a non-identity monad morphism M ~> M that is monadically natural in M?
- Problem with loading module ‘Distribution.Simple’
- Improving efficiency in Stirling numbers calculation
- Does sequencing an infinite list of IO actions by definition result in a never-ending action? Or is there a way to bail out?
- How to call pgQuery from postgresql-query?
- How to avoid whitespace after a tag (link) in Hamlet templates?
- Understanding type-directed resolution in Haskell with existential types
- Why is seq bad?
- Understanding bind function in Haskell
- How to create route that will trigger on any path in Servant?
- How do I use a global state in WAI middleware?
- nixos 23.11 cabal install mysql-simple problem - "Missing (or bad) C libraries"
- Is there a way to kill all forked threads in a GHCi session without restarting it?
- Why can an invalid list expression such as 2:1 be assigned to a variable, but not printed?
- Iterate over a type level list and call a function based on each type in the list
- How does this solution of Project Euler Problem 27 in the Haskell Wiki work?
- Why `Monad` is required to use `pure`?
- Can't do partial function definitions in GHCi
- recommended way to convert Double -> Float in Haskell
- Haskell profiling understanding cost centre summary for anonymous lambda
- Why is Haskell fully declarative?
- GHC Generating Redundant Core Operations
- Question about Event firing in reflex-frp
- Using Haskell's "Maybe", type declarations
- How can I elegantly invert a Map's keys and values?
- Why there is no output for wrapped IO in Haskell?
- What are the definitions of Weather and Memory in xmobar repo?
- Serializing a Data.Text value to a ByteString without unnecessary \NUL bytes
- Using Haskell with VS Code