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
top 3 comments
sorted by: hot top controversial new old
[–] bss03@infosec.pub 2 points 3 months ago

ghciwatch (https://mercury.com/blog/announcing-ghciwatch) sounds cool. I've been using HLS and ghcid for work.

[–] bss03@infosec.pub 2 points 3 months ago (1 children)

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.

[–] bss03@infosec.pub 2 points 3 months ago

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.