Which functions would you want to see?

– https://byorgey.github.io/blog/posts/2024/07/18/River.html

Since it’s a (uniformly) recursive data type, I want to see the underlying functor

data RiverF x r = CF !x | ConsF !x !r deriving Functor

projection and embedding functions:

project :: River a -> RiverF a (River a)
project = \case
  C x -> CF x
  Cons x r -> ConsF x r

embed :: RiverF a (River a) -> River a
embed = \case
  CF x -> C x
  ConsF x r -> x ::= r -- Choosing to normalize, here.

And then generalized fold / unfold:

fold :: (RiverF a r -> r) -> River a -> r
fold alg = f
  where f = alg . fmap f . project

unfold :: (s -> RiverF a s) -> s -> River a
unfold coalg = u
  where u = embed . fmap u . coalg

Note that since we chose a normalizing embed, the result of an unfold is also always normalized.

I would also not be opposed to a alternate definition that took a proof of normality for the Cons, but I know that would take some higher-rank types, at least.