Unfolding trees breadth-first in Haskell

[Lysxia]

I wrote a blog post about a fancy way of writing breadth-first walks in Haskell: Lysxia - Unfolding trees breadth-first in Haskell

The code is also available as the weave library on Hackage. It was a good excuse to experiment with Backpack and multiple libraries in one package.

[raehik]

Thanks. That was an excellent read. One day my brain will be saturated with the various flavours of laziness in Haskell and then will I be enlightened like yourself.

[rhendric]

I’m deeply intrigued by the similarity between the shapes of Phases and WeaveL (with a flipping of the parameters to make things line up):

-- T = Phases
data T f a where
  _ :: f a -> T f a
  _ :: f (a -> b) ->    T f a  -> T f b

-- T = WeaveL
data T f a where
  _ ::   a -> T f a
  _ ::   (a -> b) -> f (T f a) -> T f b

I don’t know what it means, but it’s sticking in my mind. Is there some unifying concept to be found here that would bring the now, delay, and weft operations into some sort of inheritance hierarchy, with delay = weft . pure and now = weft . fmap pure as laws akin to the laws that relate pure, (<*>) and (>>=)?

[AntC2]

Ban recursion now. “It’s OK to ask others for help. Recusion … isn’t natural.”

[meooow]

Very nice, it’s quite fun to play around with these.

I found that implementing a specialized function for liftA2 (,) greatly helps with efficiency because 1. all the liftA2 (,) doesn’t allocate and 2. liftA2 can inline one level into weaveL (since it’s no longer recursive) and simplify which again saves allocations.

 instance Applicative m => Applicative (WeaveL m) where
   pure = EndL
   liftA2 f (EndL a) wb = f a <$> wb
   liftA2 f wa (EndL b) = flip f b <$> wa
   liftA2 f (WeftL wa g) (WeftL wb h)
-    = WeftL ((liftA2 . liftA2) (,) wa wb) (\ ~(a, b) -> f (g a) (h b))
+    = WeftL (liftA2 pair wa wb) (\ ~(a, b) -> f (g a) (h b))
+
+pair :: Applicative m => WeaveL m a -> WeaveL m b -> WeaveL m (a, b)
+pair (EndL a) wb = (,) a <$> wb
+pair wa (EndL b) = flip (,) b <$> wa
+pair (WeftL wa g) (WeftL wb h)
+  = WeftL (liftA2 pair wa wb) (\ ~(a, b) -> (g a, h b))

And from here, making the \ ~(a, b) -> ... strict as \(a, b) -> makes it faster than the global level-based unfold, which is similarly strict.

Q-1x:
G-1x:              2.07x
L-1x:              4.55x
L-pair-1x:         2.65x
L-pair-strict-1x:  1.74x
Q-10x:
G-10x:             1.76x
L-10x:             4.34x
L-pair-10x:        2.39x
L-pair-strict-10x: 1.55x

[Lysxia]

Is there some unifying concept to be found here that would bring the now, delay, and weft operations into some sort of inheritance hierarchy, with delay = weft . pure and now = weft . fmap pure as laws akin to the laws that relate pure, (<*>) and (>>=)?

The relation between now, delay, weft is closely connected to the Applicative-Monad hierarchy. There is a different presentation of these operations as follows.

An “applicative with f” is an applicative functor m with an embed :: forall a. f a -> m a:

class ApplicativeWith f m where
  pure :: a -> m a
  liftA2 :: (a -> b -> c) -> m a -> m b -> m c
  embed :: f a -> m a

A “monad with f” is a monad with embed.

class MonadWith f m where
  return :: a -> m a
  (>>=) :: m a -> (a -> m b) -> m b
  embed :: f a -> m a

Here the operations pure/liftA2/(>>=) should be thought concretely as those of the Free applicative and Free monad, which are different from those of Phases and Weave even though they are the same types (actually, there is a small difference between Phases and the Free applicative which is unimportant).

An applicative with f can implement now and delay: now = embed,
and delay appends pure () :: f () to a computation: delay = (pure () *>).

A monad with f can implement weft = join . embed. A “monad with f” is of course also an “applicative with f”, so it also implements now and delay.

With that, the equations relating weft to now and delay can be derived from the definitions of pure and liftA2/(<*>) using return and (>>=).

---

I’m deeply intrigued by the similarity between the shapes of Phases and WeaveL (with a flipping of the parameters to make things line up):

-- T = Phases
data T f a where
  _ :: f a -> T f a
  _ :: f (a -> b) ->    T f a  -> T f b

-- T = WeaveL
data T f a where
  _ ::   a -> T f a
  _ ::   (a -> b) -> f (T f a) -> T f b

The lining up of (a -> b)/a in the second constructor is because both involve a “Day convolution”, which is a product-like operation on functors.

data Day :: (Type -> Type) -> (Type -> Type) -> (Type -> Type) where
  Day :: f (a -> b) -> g a -> Day f g b

(There is a slightly different definition of Day in the library kan-extensions which generalizes further to non-functors.)

In a way, the fact that the pattern _ (a -> b) -> _ a -> _ b appears in both Phases and WeaveL just says that they both involve a certain notion of “multiplication”, which is Day convolution. That common point is very visible because the definition of multiplication is inlined in both, but it is not a super deep common point because multiplication is a quite common operation.

The difference between WeaveS and WeaveL is the difference between y and 1 \times y, where 1 is the functor Identity, \times is Day convolution, and y is the functor f . T f. On a semantic level, the fact that WeaveS and WeaveL have the same “meaning” is as obvious as x = 1 \times x. Thus the occurrence of Day convolution in WeaveL is not as meaningful as it is in Phases.

-- These constructors of WeaveL and WeaveS are semantically equivalent
Weft :: (a -> b) -> f (T f a) -> T f b  -- 1 × y = Day Identity (f :.: T f)
Weft ::             f (T f a) -> T f a  --     y = f :.: T f

Another way to line up weaves and phases which I mention briefly at the end of my post is

-- Phases with a simplified base case
data T f a where
  _ :: a -> T f a
  _ :: (f `Day` T f) a -> T f a

-- WeaveS
data T f a where
  _ :: a -> T f a
  _ :: (f :.:   T f) a -> T f a

Those types correspond to two interpretations of the equation T = 1 + f \times T as an equation between functors:

• if \times is Day, then T is Phases f;
• if \times is (:.:) (aka. Compose), then T is Weave f.

You may have seen that equation elsewhere, as an equation between types:

• if \times is (,) (the product of types), then T is [f], the type of lists of f.

Phases and Weave are just lists in a different category!

---

Re @meooow: that’s an awesome find! This will be a fine addition to the weave library.

[rhendric]

@Lysxia

Here the operations pure/liftA2/(>>=) should be thought concretely as those of the Free applicative and Free monad, which are different from those of Phases and Weave even though they are the same types (actually, there is a small difference between Phases and the Free applicative which is unimportant).

An applicative with f can implement now and delay: now = embed,
and delay appends pure () :: f () to a computation: delay = (pure () *>).

A monad with f can implement weft = join . embed. A “monad with f” is of course also an “applicative with f”, so it also implements now and delay.

With that, the equations relating weft to now and delay can be derived from the definitions of pure and liftA2/(<*>) using return and (>>=).

This sounds very compelling, but I haven’t been able to figure out how it works.

You’ve defined delay = (pure () *>)—if that isn’t a mistake, it must be tied up in the difference you mention between the free-like instances and the weave-like instances, because from a surface read that sure looks like it has to be identity in any single lawful Applicative. But pure is the same in both instances—it’s just the first constructor. So I don’t see how this could be correct, regardless of whether you take the free-like definition of (*>) or the weave-like one.

There’s got to be a now in there somewhere, right? Because we want to show that delay == weft . pure, and you’ve given me weft = join . now, and how are we going to show delay == join . now . pure otherwise if now is an axiom?

[Lysxia]

My bad, I made a typo. It should have been delay = (embed (pure ()) *>)