• bss03@infosec.pub
    link
    fedilink
    English
    arrow-up
    2
    ·
    3 months ago

    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
      link
      fedilink
      arrow-up
      2
      ·
      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.