A traversal as data

Question

I heard about this construction which is loosely described as “a traversal represented in data, applied to some structure, without the need for the applicative”

It can be defined as:

data X a b r =
    | Done r
    | Step a (X a b (b -> r))

A word description would be as follows:

the type X a b r describes the shape of a structure
which contains things of type a
and for each a you get the opportunity to produce something of type b
and provided you do that for each a,
you get something of type r.

Thus a “traversal” of a list, [a], has type X a b [b], because if you can turn each a of the list into a b then you get a [b].

My question is: what is this thing called? Is there a reference to more information about it?

Example usage:

instance Functor (X a b) where
  fmap f (Done r) = f r
  fmap f (Step a next) = Step a (fmap (f .) next)

f :: [a] -> X a b [b]
f [] = Done []
f (a:as) = Step a (fmap (flip (:)) as)

g :: Applicative f => (a -> f b) -> X a b r -> f r
g f (Done r) = pure r
g f (Step a next) = g f next <*> f a

More generally:

instance Applicative (X a b) where
  pure x = Done x
  Done f <*> y = fmap (\y -> f y) y
  Step a next <*> y = Step a (fmap flip next <*> y)

t :: Traversable t => t a -> X a b (t b)
t = traverse (\a -> Step a (Done id))

And, assuming I haven’t made any errors, we should find that:

flip g . t == traverse

Edit: I’ve thought about this some more. There is something this doesn’t have which a traversal has: a traversal can split up the computation into something that isn’t “one at a time,” for example to traverse a binary tree one can traverse the left and right half “in parallel.” Here is a structure that I think gives the same effect:

data Y a b r =
  | Done r
  | One a (b -> r)
  | forall s t. Split (Y a b s) (Y a b t) (s -> t -> r)

(Slightly vague syntax as I don’t remember it and don’t want to write this as a gadt)

f1 :: X a b r -> Y a b r
f1 (Done x) = Done x
f1 (Step a next) = Split (One a id) (f1 next) (flip ($))

f2 :: Y a b r -> X a b r
f2 (Done x) = Done x
f2 (One a f) = Step a (Done f)
f2 (Split x y f) = f <$> f2 x <*> f2 y

A traversal as data

0 Answers