this post was submitted on 25 Jul 2024
5 points (100.0% liked)

Haskell

467 readers
6 users here now

founded 2 years ago
MODERATORS
you are viewing a single comment's thread
view the rest of the comments
[โ€“] bss03@infosec.pub 2 points 5 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 5 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.