Since it’s a (uniformly) recursive data type, I want to see the underlying functor
dataRiverF x r = CF !x | ConsF !x !r derivingFunctor
projection and embedding functions:
project :: River a -> RiverF a (River a)
project = \caseC x -> CF x
Cons x r -> ConsF x r
embed :: RiverF a (River a) -> River a
embed = \caseCF 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.
– 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.
Actually, unless we want to adopt and propagate the
Eq
constraint, we can’t normalize inembed
. Maybe it would be worth it to have a normal proof.