Geeky things and other research from a work in progress

2009-04-12

Latest on the incremental fold and attributes

Inspired by Edward Kmett's adaptation of my incremental fold, I have developed new versions of the incremental fold and the incremental attributes. These use a style very much based on Edward's fixed-point representation (i.e. the Mu datatype). Normally, I would discuss the code in more depth, but my available time for this post is limited. So, I will just introduce the code and point to it for a more in-depth perusal if you so desire.

Fixed Point for an Incremental Fold

First, we have the fixed-point incremental fold. It is similar to Edward's, but rather than using a different fixed-point datatype (his (:>)), I use a datatype embedded in the typical Mu.

newtype Mu f = In { out :: f (Mu f) }

data Ext z f r = Ext { tag :: z, fun :: f r }

type EMu z f = Mu (Ext z f)

Also, I have renamed remember and forget to ein and eout, because they are simply the "in" and "out" for this extended fixed-point representation.

ein' :: (Functor f) => (f z -> z) -> f (EMu z f) -> EMu z f
ein' phiz x = emu (phiz (fmap result x)) x

ein :: (Algebra f z) => f (EMu z f) -> EMu z f
ein = ein' alg

eout :: EMu z f -> f (EMu z f)
eout = fun . out

As a learning experience, I implemented the catamorphism, anamorphism, hylomorphism, paramorphism, and zygomorphism for EMu. See the code for details.

To experiment with incremental folds, I implemented functions for three fixed-point datatypes, Nat, Tree, and List. Since we've been talking about trees, here's what the datatype looks like:

data TreeF a r = Bin a r r | Tip deriving (Eq, Ord, Show, Read)

instance Functor (TreeF a) where ...

type Tree a = Mu (TreeF a)
type ETree z a = EMu z (TreeF a)

Along with each datatype, there are functions that would potentially be part of a library. Though not necessary, I implemented some of these as catamorphisms, anamorphisms, and paramorphisms. It's actually quite nice to see these in use, especially when you can compare it to the implementation with implicit recursion. For an example, compare insert and insert_rec for trees.

Any of these datatypes and functions now support an incremental fold for a given algebra of type f a -> a where f is the functor of the datatype. I have included a few example algebra implementations.

Again, you can find the code for incremental fold on a fixed point here.

Fixed Point for Incremental Attributes

As I mentioned before, the fold is a specific instance of incremental attributes. Starting with the code for the incremental fixed-point fold, I put together a generalized version of incremental attributes for fixed-point datatypes. Much of the code is the same, so let me highlight the differences from the above.

We first take Ext and extend it further with an inherited attribute. Recall that the incremental catamorphism is strictly synthesized (from the children to the parent), and to generalize, we need to pass attributes from the parent to the children. This gives us Att, and the adaptation of EMu is now AMu

data Att i s f r = Att { itag :: i , stag :: s , fun :: f r }

type AMu i s f = Mu (Att i s f)

This causes our "in" and "out" isomorphism to be quite different.

ain' :: (Functor f, Zippable f) => (i -> f s -> (s, Maybe (f i))) -> i -> f (AMu i s f) -> AMu i s f
ain' rho i x = In (Att i s y)
where
fs = fmap sresult x
(s, fi) = rho i fs
push j = ain' rho j . fun . out
y = case fi of
Nothing -> x
Just fj -> fromMaybe x (zipWith push fj x)

ain :: (AAlgebra f i s) => i -> f (AMu i s f) -> AMu i s f
ain = ain' aalg

aout :: AMu i s f -> (f (AMu i s f), i)
aout = fork fun itag . out

Looking at the above, we need a zipWith for each datatype, and we have a different algebra as well. The type of the algebra is really the key to understanding what an implementation of incremental attributes does.

class (Functor f, Zippable f) => AAlgebra f i s where
aalg :: i -> f s -> (s, Maybe (f i))

It says that, given an inherited attribute (from the parent) and a functor of synthesized attributes (from the children), an algebra produces a pair of a synthesized attribute (for the parent) and a functor of inherited attributes (for the children). The Maybe is just an added convenience to allow synthesizing-only algebras the pleasure of not having to produce the inheritable functor.

I have provided much of the same set of examples in this module as in the fold one. Noticeably different, however, is the addition of the float differencing implementation and a counter that ranks in-order nodes. Both were described in the post on incremental attributes. It's also worth pointing out that several of the morphisms and algebras had to change due to the inherited attribute that must be provided as input.

Well, that's the current story on incremental attributes. I'm greatly appreciative to Edward Kmett for his article. I'm also currently working on the generic thoughts behind the idea. Perhaps there will be more to come...

2 comments:

  1. Good job adapting the incremental attribute stuff.

    I would point a caveat about the adaptation you made:

    Explicitly allowing access to ein' loses the enforced safety guarantee that I provided with remember and forget.

    You can now construct invalid members of the folded type. That was why I went off on the weird reflection tangent, because it let me have both enforced type safety and still provide algebras that needed context.

    Otherwise I only cringe a little at the more verbose fixpoint because it is harder to read the output of Show/Read, but thats a matter of personal style. =)

    P.S. Typo on my name in the wrapup. ;)

    ReplyDelete
  2. Thanks for the point about the type safety. It's certainly valid.

    The separation of the fixed point and the Ext/Att is (IMHO) better for clarity of presentation, though perhaps verbose for values. Also, I'm hesitant to forge new symbols for this without a context (at least, in my head) to provide for their meaning. Of course, styles differ. I'm still learning and adapting my own. :)

    Typo fixed. Thanks!

    ReplyDelete