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?

Mcclintock

The Expression type you're using can be expressed without the GADTs, at which point the solution is much simpler. Is there a specific need for GADTs in your AST? – Sybyl

Stephen Diehl: the non-GADT versions I can think of seem verbose. What are you thinking of? – Mcclintock

Like for instance why the GADT over a closed datatype like: data Expr = I Int | B Bool | Add Expr Expr ...? – Sybyl

Stephen Diehl: but that allows the illegal expression Add (B True) (B True) which the GADT doesn't – Mcclintock

Well javascript also supports adding up nonsense, so I do not see why this would be bad ;) – Petcock

@Petcock Hehehe. Folk should watch Gary Bernhardt's Wat?! talk if they haven't already. – Mani

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

Handshake

Nice. It's a bit of a letdown for me, because I intended to post this exact same solution, but then I compulsively tried to implement all of the uniplate API in this lens style, and found out that holes and contexts cannot be done. So I postponed posting my answer, until I sorted out that issue (and I sorted it out: we need a classic-style uniplate that returns lists of children indexed by a type-level list of the type indices of the children). – Bookman

I'd guess that you can do holes and contexts two ways. In one way, you'd lose all the type information about the contained type. In the other you'd require a constraint on f. Typeable1 f, forall a. Typeable f a should be more than adequate. – Handshake

I mean, it's not possible to implement a holes returning even existentially quantified types in the lens style, without demanding Typeable1, while this is quite possible with a uniplate style implementation. Here's the source. As a side note, with GADTs it's fine most of the time with just existentials (and without Typeable), because the type information is usually available from the GADT constructors. – Bookman

I have a working holes1 right now. You defined exactly the same type for Hole that I initially did. The trick is to recognize that the return from the function isn't necessarily in f. data Hole f a where Hole :: f b -> (f b -> a) -> Hole f a – Handshake

I asked and answered another question for how to define holes and contexts. #25394370 – Handshake