Recursive bottom-up traversal of algebraic data types

Question

When dealing with sizeable algebraic data types in Haskell, there is a particular recursive traversal not captured by folding over the data type. For instance, suppose I have a simple data type representing formulas in propositional logic, and a fold defined over it:

type FAlgebra α φ =
 (φ, φ,                -- False, True
  α -> φ,              -- Atom
  φ -> φ,              -- Negation
  φ -> φ -> φ,         -- Conjunction
  φ -> φ -> φ,         -- Disjunction
  φ -> φ -> φ,         -- Implication
  φ -> φ -> φ)         -- Bi-implication

fold :: FAlgebra α φ -> Form α -> φ
fold (f,t,lit,not,con,dis,imp,iff) = fold' where
 fold' (Fls)     = f
 fold' (Tru)     = t
 fold' (Lit α)   = lit α
 fold' (Not φ)   = not (fold' φ)
 fold' (Con φ ψ) = con (fold' φ) (fold' ψ)
 fold' (Dis φ ψ) = dis (fold' φ) (fold' ψ)
 fold' (Imp φ ψ) = imp (fold' φ) (fold' ψ)
 fold' (Iff φ ψ) = iff (fold' φ) (fold' ψ)

This recursion scheme provides a succinct answer to recursions like evaluation or finding literals:

eval :: (Ord α) => Map α Bool -> Form α -> Bool
eval v = fold (False, True, (fromJust . flip M.lookup v),
               not, (&&), (||), ((||) . not), (==))

literals :: (Ord α) => Form α -> Set α
literals = fold (S.empty, S.empty, S.singleton, id,
                 S.union, S.union, S.union, S.union)

However, it doesn't fare so well when I wish to "sweep" the data type. In the following, simp is an auxiliary function defined by necessary pattern-matching:

simplify :: Form α -> Form α
simplify (Not φ)   = simp (Not (simplify φ))
simplify (Con φ ψ) = simp (Con (simplify φ) (simplify ψ))
simplify (Dis φ ψ) = simp (Dis (simplify φ) (simplify ψ))
simplify (Imp φ ψ) = simp (Imp (simplify φ) (simplify ψ))
simplify (Iff φ ψ) = simp (Imp (simplify φ) (simplify ψ))
simplify φ         = φ

Using a fold to define simplify, of course, generates incorrect results. For instance, the following is not equivalent:

simplify = fold (Fls, Tru, Lit, (simp . Not), con Con, con Dis, con Imp, con Iff)
 where con f φ ψ = simp (f φ ψ)

What is the best solution to recursions like simplify? Should I define a generic traversal similar to the fold over the data type, or is there a standard recursion pattern for defining such functions?

Answer 1

Did you try Uniplate? For operations that only work on a single type it can perform bottom-up rewrites and rewrites until a fixed point.

For example:

import Data.Generics.Uniplate.Direct
import qualified Data.Map as M

data Form a = Fls | Tru | Lit a
            | Not (Form a)
            | Con (Form a) (Form a)
            | Dis (Form a) (Form a)
            -- etc.
  deriving (Show, Eq)

instance Uniplate (Form a) where
  uniplate (Not f) = plate Not |* f
  uniplate (Con f1 f2) = plate Con |* f1 |* f2
  uniplate (Dis f1 f2) = plate Dis |* f1 |* f2
  -- one case for each constructor that may contain nested (Form a)s
  uniplate x = plate x

simplify :: Form a -> Form a 
simplify = transform simp
 where
   simp (Not (Not f)) = f
   simp (Not Fls) = Tru
   simp (Not Tru) = Fls
   simp x = x

test =
  simplify (Not (Not (Not (Not (Lit "a"))))) == Lit "a"

The relevant functions for you are transform and rewrite.

For a more in-depth documentation about Uniplate there's also a paper (PDF).