Cleaner Alternative to Extensive Pattern Matching in Haskell

Question

Right now, I have some code that essentially works like this:

data Expression 
    = Literal Bool 
    | Variable String
    | Not Expression 
    | Or Expression Expression 
    | And Expression Expression
    deriving Eq

simplify :: Expression -> Expression
simplify (Literal b) = Literal b
simplify (Variable s) = Variable s
simplify (Not e) = case simplify e of
    (Literal b) -> Literal (not b)
    e'          -> Not e'
simplify (And a b) = case (simplify a, simplify b) of
    (Literal False, _) -> Literal False
    (_, Literal False) -> Literal False
    (a', b')           -> And a' b'
simplify (Or a b) = case (simplify a, simplify b) of
    (Literal True, _) -> Literal True
    (_, Literal True) -> Literal True
    (a', b')          -> Or a' b'

And many more such patterns regarding all the ways one can simplify a boolean expression. As I add more operators and rules however, this grows immensely and feels.. clunky. Especially so since some rules need to be added twice to account for commutativity.

How can I nicely refactor lots and lots of patterns of which some (most, I'd say) are even symmetrical (take the And and Or patterns for example)?

Right now, adding a rule to simplify And (Variable "x") (Not (Variable "x")) to Literal False requires me to add two nested rules, which is all but optimal.

Answer 1

Basically the problem is that you have to write out simplify of the subexpressions in each clause, over and over again. It would be better to first get all the subexpressions done before even considering laws involving the top-level operator. One simple way is to add an auxiliary version of simplify, that doesn't recurse down:

simplify :: Expression -> Expression
simplify (Literal b) = Literal b
simplify (Variable s) = Variable s
simplify (Not e) = simplify' . Not $ simplify e
simplify (And a b) = simplify' $ And (simplify a) (simplify b)
simplify (Or a b) = simplify' $ Or (simplify a) (simplify b)

simplify' :: Expression -> Expression
simplify' (Not (Literal b)) = Literal $ not b
simplify' (And (Literal False) _) = Literal False
...

With the only small amount of operations you have in booleans, this is probably the most sensible approach. However with more operations, the duplication in simplify might still be worth to avoid. To that end, you can conflate the unary and binary operations to a common constructor:

data Expression 
    = Literal Bool 
    | Variable String
    | BoolPrefix BoolPrefix Expression 
    | BoolInfix BoolInfix Expression Expression 
    deriving Eq

data BoolPrefix = Negation
data BoolInfix  = AndOp | OrOp

and then you have just

simplify (Literal b) = Literal b
simplify (Variable s) = Variable s
simplify (BoolPrefix bpf e) = simplify' . BoolPrefix bpf $ simplify e
simplify (BoolInfix bifx a b) = simplify' $ BoolInfix bifx (simplify a) (simplify b)

Obviously this makes simplify' more awkward though, so perhaps not such a good idea. You can however get around this syntactical overhead by defining specialised pattern synonyms:

{-# LANGUAGE PatternSynonyms #-}

pattern Not :: Expression -> Expression
pattern Not x = BoolPrefix Negation x

infixr 3 :∧
pattern (:∧) :: Expression -> Expression -> Expression
pattern a:∧b = BoolInfix AndOp a b

infixr 2 :∨
pattern (:∨) :: Expression -> Expression -> Expression
pattern a:∨b = BoolInfix OrOp a b

For that matter, perhaps also

pattern F, T :: Expression
pattern F = Literal False
pattern T = Literal True

With that, you can then write

simplify' :: Expression -> Expression
simplify' (Not (Literal b)) = Literal $ not b
simplify' (F :∧ _) = F
simplify' (_ :∧ F) = F
simplify' (T :∨ _) = T
simplify' (a :∧ Not b) | a==b  = T
...

I should add a caveat though: when I tried something similar to those pattern synonyms, not for booleans but affine mappings, it made the compiler extremely slow. (Also, GHC-7.10 didn't yet support polymorphic pattern synonyms yet; this has changed quite a bit as of now.)

---

Note also that all this will not generally yield the simplest possible form – for that, you'd need to find the fixed point of simplify.

Answer 2

One thing you can do is simplify as you construct, rather than first constructing then repeatedly destructing. So:

module Simple (Expression, true, false, var, not, or, and) where

import Prelude hiding (not, or, and)

data Expression
    = Literal Bool
    | Variable String
    | Not Expression
    | Or Expression Expression
    | And Expression Expression
    deriving (Eq, Ord, Read, Show)

true = Literal True
false = Literal False
var = Variable

not (Literal True) = false
not (Literal False) = true
not x = Not x

or (Literal True) _ = true
or _ (Literal True) = true
or x y = Or x y

and (Literal False) _ = false
and _ (Literal False) = false
and x y = And x y

We can try it out in ghci:

> and (var "x") (and (var "y") false)
Literal False

Note that the constructors are not exported: this ensures that folks constructing one of these can't avoid the simplification process. Actually, this may be a drawback; occasionally it is nice to see the "full" form. A standard approach to dealing with this is to make the exported smart constructors part of a type-class; you can either use them to build a "full" form or a "simplified" way. To avoid having to define the type twice, we could either use a newtype or a phantom parameter; I'll elect for the latter here to reduce the noise in pattern-matching.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
module Simple (Format(..), true, false, var, not, or, and) where

import Prelude hiding (not, or, and)

data Format = Explicit | Simplified

data Expression (a :: Format)
    = Literal Bool
    | Variable String
    | Not (Expression a)
    | Or (Expression a) (Expression a)
    | And (Expression a) (Expression a)
    deriving (Eq, Ord, Read, Show)

class Expr e where
    true, false :: e
    var :: String -> e
    not :: e -> e
    or, and :: e -> e -> e

instance Expr (Expression Explicit) where
    true = Literal True
    false = Literal False
    var = Variable
    not = Not
    or = Or
    and = And

instance Expr (Expression Simplified) where
    true = Literal True
    false = Literal False
    var = Variable

    not (Literal True) = false
    not (Literal False) = true
    not x = Not x

    or (Literal True) _ = true
    or _ (Literal True) = true
    or x y = Or x y

    and (Literal False) _ = false
    and _ (Literal False) = false
    and x y = And x y

Now in ghci we can "run" the same term in two different ways:

> :set -XDataKinds
> and (var "x") (and (var "y") false) :: Expression Explicit
And (Variable "x") (And (Variable "y") (Literal False))
> and (var "x") (and (var "y") false) :: Expression Simplified
Literal False

You might want to add more rules later; for example, maybe you want:

and (Variable x) (Not (Variable y)) | x == y = false
and (Not (Variable x)) (Variable y) | x == y = false

Having to repeat both "orders" of patterns is a bit annoying. We should abstract over that! The data declaration and classes will be the same, but we'll add the helper function eitherOrder and use it in the definitions of and and or. Here's a more complete set of simplifications using this idea (and our final version of the module):

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
module Simple (Format(..), true, false, var, not, or, and) where

import Data.Maybe
import Data.Monoid
import Prelude hiding (not, or, and)
import Control.Applicative ((<|>))

data Format = Explicit | Simplified

data Expression (a :: Format)
    = Literal Bool
    | Variable String
    | Not (Expression a)
    | Or (Expression a) (Expression a)
    | And (Expression a) (Expression a)
    deriving (Eq, Ord, Read, Show)

class Expr e where
    true, false :: e
    var :: String -> e
    not :: e -> e
    or, and :: e -> e -> e

instance Expr (Expression Explicit) where
    true = Literal True
    false = Literal False
    var = Variable
    not = Not
    or = Or
    and = And

eitherOrder :: (e -> e -> e)
            -> (e -> e -> Maybe e)
            -> e -> e -> e
eitherOrder fExplicit fSimplified x y = fromMaybe
    (fExplicit x y)
    (fSimplified x y <|> fSimplified y x)

instance Expr (Expression Simplified) where
    true = Literal True
    false = Literal False
    var = Variable

    not (Literal True) = false
    not (Literal False) = true
    not (Not x) = x
    not x = Not x

    or = eitherOrder Or go where
        go (Literal True) _ = Just true
        go (Literal False) x = Just x
        go (Variable x) (Variable y) | x == y = Just (var x)
        go (Variable x) (Not (Variable y)) | x == y = Just true
        go _ _ = Nothing

    and = eitherOrder And go where
        go (Literal True) x = Just x
        go (Literal False) _ = Just false
        go (Variable x) (Variable y) | x == y = Just (var x)
        go (Variable x) (Not (Variable y)) | x == y = Just false
        go _ _ = Nothing

Now in ghci we can do more complicated simplifications, like:

> and (not (not (var "x"))) (var "x") :: Expression Simplified
Variable "x"

And even though we only wrote one order of the rewrite rule, both orders work properly:

> and (not (var "x")) (var "x") :: Expression Simplified
Literal False
> and (var "x") (not (var "x")) :: Expression Simplified
Literal False