this post was submitted on 25 Jul 2024
6 points (100.0% liked)
Haskell
457 readers
1 users here now
founded 1 year ago
MODERATORS
you are viewing a single comment's thread
view the rest of the comments
view the rest of the comments
-- 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
projection and embedding functions:
And then generalized fold / unfold:
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.