@EricRogstad - I want to follow up and ellaborate on your question (and clear things up, mostly for my own edification).

> How do we know that Fix is an initial algebra?

Bartosz just pointed out that we _don't always know_ if `Fix :: f (Fix f) -> Fix f` is initial, because we don't always know if the type `Fix f` is inhabited. For example if we define the type

data Pair a b = Pair a b

...then neither `Fix (Pair a)` nor `Pair a (Fix (Pair a)` are inhabited by a terminating program. So you couldn't do anything meaningful with one in PureScript, and we have to leverage lazy evaluation in Haskell to make use of it.

The restriction that we only consider terminating programs comes from page 33 of [the companion notes](http://brendanfong.com/programmingcats_files/cats4progs-DRAFT.pdf), as mentioned elsewhere on this forum.

Since `Fix (Pair a)` has no inhabitants, it's like `Void`. `Void` is the empty datatype defined like this:

data Void

----------------------------------------

> But how do we know that the converse is true? Just because something is a fixed point, does that also mean it will be an initial algebra?

I started answering this yesterday but I'll finish today, starting from the top. Define:

data Fix f = Fix { unfix :: f (Fix f) }

And let's suppose that `f` is a functor and the type `Fix f` is inhabited. We want to show that the F-algebra

Fix :: f (Fix f) -> Fix f

is initial.

**Proof.** In order to show it's initial, then for each F-algebra `g :: f a -> a` we must find a function `m :: Fix f -> a` such that `m . Fix = g . fmap m`

Here's how we do it. First define `cata` as follows (I'm stealing this from Bartosz's writings on [www.schoolofhaskell.com](https://www.schoolofhaskell.com/user/bartosz/understanding-algebras#catamorphisms)):

cata :: Functor f => (f a -> a) -> Fix f -> a

cata alg = alg . fmap (cata alg) . unFix

_**This is exactly what we need!**_

Let `m` be `cata g :: Fix f -> a`. We need to show that `cata g . Fix = g . fmap (cata g)`, which is pretty straight-forward:

cata g . Fix

= g . fmap (cata g) . unFix . Fix

= g . fmap (cata g)

...since `unFix . Fix = id`. So there we go, we have a constructive proof that `Fix :: f (Fix f) -> Fix f` is initial. \\(\Box\\)

[EDIT: typos]

> How do we know that Fix is an initial algebra?

Bartosz just pointed out that we _don't always know_ if `Fix :: f (Fix f) -> Fix f` is initial, because we don't always know if the type `Fix f` is inhabited. For example if we define the type

data Pair a b = Pair a b

...then neither `Fix (Pair a)` nor `Pair a (Fix (Pair a)` are inhabited by a terminating program. So you couldn't do anything meaningful with one in PureScript, and we have to leverage lazy evaluation in Haskell to make use of it.

The restriction that we only consider terminating programs comes from page 33 of [the companion notes](http://brendanfong.com/programmingcats_files/cats4progs-DRAFT.pdf), as mentioned elsewhere on this forum.

Since `Fix (Pair a)` has no inhabitants, it's like `Void`. `Void` is the empty datatype defined like this:

data Void

----------------------------------------

> But how do we know that the converse is true? Just because something is a fixed point, does that also mean it will be an initial algebra?

I started answering this yesterday but I'll finish today, starting from the top. Define:

data Fix f = Fix { unfix :: f (Fix f) }

And let's suppose that `f` is a functor and the type `Fix f` is inhabited. We want to show that the F-algebra

Fix :: f (Fix f) -> Fix f

is initial.

**Proof.** In order to show it's initial, then for each F-algebra `g :: f a -> a` we must find a function `m :: Fix f -> a` such that `m . Fix = g . fmap m`

Here's how we do it. First define `cata` as follows (I'm stealing this from Bartosz's writings on [www.schoolofhaskell.com](https://www.schoolofhaskell.com/user/bartosz/understanding-algebras#catamorphisms)):

cata :: Functor f => (f a -> a) -> Fix f -> a

cata alg = alg . fmap (cata alg) . unFix

_**This is exactly what we need!**_

Let `m` be `cata g :: Fix f -> a`. We need to show that `cata g . Fix = g . fmap (cata g)`, which is pretty straight-forward:

cata g . Fix

= g . fmap (cata g) . unFix . Fix

= g . fmap (cata g)

...since `unFix . Fix = id`. So there we go, we have a constructive proof that `Fix :: f (Fix f) -> Fix f` is initial. \\(\Box\\)

[EDIT: typos]