Simplifying a GADT with Uniplate

Question

I'm trying to answer this stackoverflow question, using uniplate as I suggested, but the only solution I've come up with so far is pretty ugly.

This seems like a fairly common issue, so I wanted to know if there was a more elegant solution.

Basically, we've got a GADT which resolves to either Expression Int or Expression Bool (ignoring codataIf = If (B True) codataIf codataIf):

data Expression a where
    I :: Int -> Expression Int
    B :: Bool -> Expression Bool
    Add :: Expression Int  -> Expression Int  -> Expression Int
    Mul :: Expression Int  -> Expression Int  -> Expression Int
    Eq  :: Expression Int  -> Expression Int  -> Expression Bool
    And :: Expression Bool -> Expression Bool -> Expression Bool
    Or  :: Expression Bool -> Expression Bool -> Expression Bool
    If  :: Expression Bool -> Expression a    -> Expression a -> Expression a

And (in my version of the problem) we want to be able to evaluate the expression tree from the bottom-up using a simple operation to combine leaves into a new leaf:

step :: Expression a -> Expression a
step = \case
  Add (I x) (I y)   -> I $ x + y
  Mul (I x) (I y)   -> I $ x * y
  Eq (I x) (I y)    -> B $ x == y
  And (B x) (B y)   -> B $ x && y
  Or (B x) (B y)    -> B $ x || y
  If (B b) x y      -> if b then x else y
  z                 -> z

I had some difficulty using DataDeriving to derive Uniplate and Biplate instances (which maybe should have been a red flag), so I rolled my own Uniplate instances for Expression Int, Expression Bool, and Biplate instances for (Expression a) (Expression a), (Expression Int) (Expression Bool), and (Expression Bool) (Expression Int).

This let me come up with these bottom-up traversals:

evalInt :: Expression Int -> Expression Int
evalInt = transform step

evalIntBi :: Expression Bool -> Expression Bool
evalIntBi = transformBi (step :: Expression Int -> Expression Int)

evalBool :: Expression Bool -> Expression Bool
evalBool = transform step

evalBoolBi :: Expression Int -> Expression Int
evalBoolBi = transformBi (step :: Expression Bool -> Expression Bool)

But since each of these can only do one transformation (combine Int leaves or Bool leaves, but not either), they can't do the complete simplification, but must be chained together manually:

λ example1
If (Eq (I 0) (Add (I 0) (I 0))) (I 1) (I 2)
λ evalInt it
If (Eq (I 0) (I 0)) (I 1) (I 2)
λ evalBoolBi it
If (B True) (I 1) (I 2)
λ evalInt it
I 1
λ example2
If (Eq (I 0) (Add (I 0) (I 0))) (B True) (B False)
λ evalIntBi it
If (Eq (I 0) (I 0)) (B True) (B False)
λ evalBool it
B True

My hackish workaround was to define a Uniplate instance for Either (Expression Int) (Expression Bool):

type  WExp = Either (Expression Int) (Expression Bool)

instance Uniplate WExp where
  uniplate = \case
      Left (Add x y)    -> plate (i2 Left Add)  |* Left x  |* Left y
      Left (Mul x y)    -> plate (i2 Left Mul)  |* Left x  |* Left y
      Left (If b x y)   -> plate (bi2 Left If)  |* Right b |* Left x  |* Left y
      Right (Eq x y)    -> plate (i2 Right Eq)  |* Left x  |* Left y
      Right (And x y)   -> plate (b2 Right And) |* Right x |* Right y
      Right (Or x y)    -> plate (b2 Right Or)  |* Right x |* Right y
      Right (If b x y)  -> plate (b3 Right If)  |* Right b |* Right x |* Right y
      e                 -> plate e
    where i2 side op (Left x) (Left y) = side (op x y)
          i2 _ _ _ _ = error "type mismatch"
          b2 side op (Right x) (Right y) = side (op x y)
          b2 _ _ _ _ = error "type mismatch"
          bi2 side op (Right x) (Left y) (Left z) = side (op x y z)
          bi2 _ _ _ _ _ = error "type mismatch"
          b3 side op (Right x) (Right y) (Right z) = side (op x y z)
          b3 _ _ _ _ _ = error "type mismatch"

evalWExp :: WExp -> WExp
evalWExp = transform (either (Left . step) (Right . step))

Now I can do the complete simplification:

λ evalWExp . Left $ example1
Left (I 1)
λ evalWExp . Right $ example2
Right (B True)

But the amount of error and wrapping/unwrapping I had to do to make this work just makes this feel inelegant and wrong to me.

Is there a right way to solve this problem with uniplate?

Answer 1

There isn't a right way to solve this problem with uniplate, but there is a right way to solve this problem with the same mechanism. The uniplate library doesn't support uniplating a data type with kind * -> *, but we can create another class to accommodate that. Here's a little minimal uniplate library for types of kind * -> *. It is based on the current git version of Uniplate that has been changed to use Applicative instead of Str.

{-# LANGUAGE RankNTypes #-}

import Control.Applicative
import Control.Monad.Identity

class Uniplate1 f where
    uniplate1 :: Applicative m => f a -> (forall b. f b -> m (f b)) -> m (f a)

    descend1 :: (forall b. f b -> f b) -> f a -> f a
    descend1 f x = runIdentity $ descendM1 (pure . f) x

    descendM1 :: Applicative m => (forall b. f b -> m (f b)) -> f a -> m (f a)
    descendM1 = flip uniplate1

transform1 :: Uniplate1 f => (forall b. f b -> f b) -> f a -> f a
transform1 f = f . descend1 (transform1 f)

Now we can write a Uniplate1 instance for Expression:

instance Uniplate1 Expression where
    uniplate1 e p = case e of
        Add x y -> liftA2 Add (p x) (p y)
        Mul x y -> liftA2 Mul (p x) (p y)
        Eq  x y -> liftA2 Eq  (p x) (p y)
        And x y -> liftA2 And (p x) (p y)
        Or  x y -> liftA2 Or  (p x) (p y)
        If  b x y -> pure If <*> p b <*> p x <*> p y
        e -> pure e

This instance is very similar to the emap function I wrote in my answer to the original question, except this instance places each item into an Applicative Functor. descend1 simply lifts its argument into Identity and runIdentity's the result, making desend1 identical to emap. Thus transform1 is identical to postmap from the previous answer.

Now, we can define reduce in terms of transform1.

reduce = transform1 step

This is enough to run an example:

"reduce"
If (And (B True) (Or (B False) (B True))) (Add (I 1) (Mul (I 2) (I 3))) (I 0)
I 7