ghciwatch (https://mercury.com/blog/announcing-ghciwatch) sounds cool. I've been using HLS and ghcid for work.
this post was submitted on 25 Jul 2024
5 points (100.0% liked)
Haskell
448 readers
2 users here now
founded 1 year ago
MODERATORS
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 in embed
. Maybe it would be worth it to have a normal proof.