Q:

Pattern match with GADTs

I am implementing an Expression solver, but I am having some problems with pattern matching. 
I have the following code
data Expression a where
                Const   ∷  Int → Expression Int
                Add ∷  Expression Int → Expression Int → Expression Int
                Sub ∷  Expression Int → Expression Int → Expression Int

eval ∷  Expression a → a
eval (Const a) = a

eval (Add exp1 exp2) = (val1 + val2)
  where
    val1 = eval exp1
    val2 = eval exp2

eval (Sub exp1 exp2) = (val1 - val2)
  where
    val1 = eval exp1
    val2 = eval exp2

But since eval Add and eval Sub are very similar and I could want another operations I though of doing a more generic implementation, but I am having some problems.  
I though of doing like
data Op = Add | Sub

data Expression a where
                Const   ∷  Int → Expression Int
                Op ∷  Expression Int → Expression Int → Expression Int

eval (Op exp1 exp2) = case Op of
                           Add → (val1 + val2)
                           Sub → (val1 - val2)
                      where
                        val1 = eval exp1
                        val2 = eval exp2 

But it doesn't work.  Is it possible to do something like this? 
Thanks in advance

A:

This does not work because you are defining Op as both a data constructor
and a type.  The type Op has two constructors Add and Sub, but the
Expression type has an Op constructor.  This code is confusing the two. 
The case statement of your eval function attempts to match of the value
Op, but Op is a constructor that takes two arguments in this context,
so you can't pattern match on it.  I suspect you are going for something like
this
data Op = Add | Sub

data Expression a where
                Const ::  Int -> Expression Int
                Op ::  Op -> Expression Int -> Expression Int -> Expression Int

eval (Const c)         = c
eval (Op op exp1 exp2) = case op of
                           Add -> (val1 + val2)
                           Sub -> (val1 - val2)
                      where
                        val1 = eval exp1
                        val2 = eval exp2

You will have to include a field in the Op constructor that denotes what
operation is to be performed.  Since you have to match on the that operation
anyway, it would probably be nicer to stick with the original definition of
Expression. 
Another possibility that is simpler and easier to extend might be something like
the following
data Expression a where
    Const ::  Int -> Expression Int
    Op    ::  (a -> b -> c) -> Expression a -> Expression b -> Expression c

eval :: Expression a -> a
eval (Const c)        = c
eval (Op f exp1 exp2) = f (eval exp1) (eval exp2)

where an Op wraps the actual function up with it.  You would not be able to
do nice things like print out the expression and know what function it
corresponds to though. 

A:

Riffing on the comments:
data Op a b c where
    Add :: Op Int Int Int
    Sub :: Op Int Int Int
    Less :: Op Int Int Bool

interpretOp :: Op a b c -> a -> b -> c
interpretOp Add = (+)
interpretOp Sub = (-)
interpretOp Less = (<)

data Expression a where
    Const :: Int -> Expression Int
    Op :: Op a b c -> Expression a -> Expression b -> Expression c

eval :: Expression a -> a
eval (Const x) = x
eval (Op op a b) = interpretOp op (eval a) (eval b)

