Why would an algebraic type be only an initial algebra (or vice versa)?

Question

In the recursion-schemes package we can express the fact that a (strictly-positive) algebraic data type

1. has a signature functor, f
2. is the initial f-algebra, and
3. is the final f-coalgebra

For instance, we can do so for [a] with the following code

-- (1) define and declare the signature functor, here called Base

data instance Prim [a] x = Nil | Cons a x deriving Functor
type instance Base [a] = Prim [a]

-- (2) demonstrate the initial algebra
instance Foldable [a] where
  project []     = Nil
  project (a:as) = Cons a as

-- (3) demonstrate the final coalgebra
instance Unfoldable [a] where
  embed Nil         = []
  embed (Cons a as) = a:as

Notably, for any type where we have (1), (2), and (3) we ought to have that (project, embed) witnesses an isomorphism.

It's my understanding that data types at large (or at least strictly-positive ones) are always final/initial co/algebras of some signature functor—in fact, they are always both.

So my question is: why have Foldable and Unfoldable as separate classes? When would a data type be just one or the other?

Currently I can imagine this might be valuable for abstract data types which only want to provide either a folding or unfolding interface, but are there other times as well?

Answer 1

This might not be an answer to your question, but it is not really true that strictly positive Haskell data types are initial algebras. The reason for this is that even in the total subset of Haskell (which is what we want to work in when reasoning!) you have infinite data.

For example, the fold of an infinite list is partial.