Alternative approaches

[pete-murphy]

It's been pointed out that Fold is isomorphic to a Moore machine, and there's a purescript-folds package that doesn't use the existential type. According to Nate Faubion:

Note that Fold can admit more fusion simply because you can step multiple times without calling (x -> b), and maps can be fused. It essentially embeds coyoneda. Moore requires you to apply it at every step.

I still haven't digested that—does it mean the encoding using the existential type (this one as opposed to that in purescript-folds) is more efficient somehow?

Further reading:
Kmett on Moore & transducers: https://www.schoolofhaskell.com/user/edwardk/moore/for-less

Alternative fold libraries (since I don't know where else to track these):
https://github.com/metrix-ai/deferred-folds
https://github.com/effectfully/prefolds
https://github.com/ekmett/folds

[pete-murphy]

xgrommx
—
10/21/2022 11:03 AM
@pete (he/him) by the way this is just Moore's machine
xgrommx
—
10/21/2022 11:16 AM
@pete (he/him)

data Moore a b = Moore b (a -> Moore a b) -- ~ Fold a b
data Cofree f a = Cofree a (f (Cofree f a))

-- Moore a b ~ Cofree ((->) a) b
-- Nu f = exists x. Tuple (x -> f x) x
-- Cofree f a ~ Nu (Compose (Tuple a) f)
-- Cofree f a ~ exists x. Tuple (x -> Tuple a (f x)) x

-- Moore a b ~ Cofree ((->) a) b ~ exists x. Tuple (Tuple (x -> b) (x -> a -> x)) x
-- Moore a b ~ Cofree ((->) a) b ~ exists x. Tuple (Tuple (x -> a -> x) x) (x -> b)

data FoldF a b x = FoldF (x -> a -> x) x (x -> b)
type Fold a b = Exists (FoldF a b)

-- Moore a b ~ Fold a b

natefaubion
—
10/21/2022 12:46 PM
Note that Fold can admit more fusion simply because you can step multiple times without calling (x -> b), and maps can be fused. It essentially embeds coyoneda. Moore requires you to apply it at every step.

[pete-murphy]

The isomorphism between Moore and Fold is also an example in the paper Representing existential data types with isomorphic simple types

More generally, a package can be described as the following Haskell existential data type:

data CE i m o =
    forall x. CE x                      -- current state
                 (i -> x)               -- producer
                 (x -> m -> x)          -- transformer (`step')
                 (x -> o)               -- observer

Here, the type i is the type of the arguments to the constructor; the type m describes additional arguments to the transformer, and o is the type of observations. The corresponding simple data type is

data C1 m o = C1 (m -> C1 m o) o

To show the isomorphism between the existential package and its existential-free representation, we exhibit the following pair of total functions. The function iso_CEC1 converts the existential data type CE into a pair of the corresponding simple data type C1 and the constructor function. The latter creates the (initial) value of C1. The function iso_C1CE is the observational inverse.

iso_CEC1 :: CE i m o -> (C1 m o, i -> C1 m o)
iso_CEC1 (CE x init step observe) = (makeC1 x, \i -> makeC1 (init i))
 where makeC1 x = C1 (makeC1 . step x) (observe x)

iso_C1CE :: (C1 m o, i -> C1 m o) -> CE i m o
iso_C1CE (c1, makeC1) = CE c1 init step observe
 where init = makeC1
       step (C1 step1 _)   = step1
       observe (C1 _ obs1) = obs1

One may call C1 m o a Skolem function for the quantified type variable x.