ghciwatch (https://mercury.com/blog/announcing-ghciwatch) sounds cool. I’ve been using HLS and ghcid for work.
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.
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.