I cannot implement an instance of Eq for the following typesafe DSL for expressions implemented with GADTs.
data Expr a where
Num :: Int -> Expr Int
Bool :: Bool -> Expr Bool
Plus :: Expr Int -> Expr Int -> Expr Int
If :: Expr Bool -> Expr a -> Expr a -> Expr a
Equal :: Eq a => Expr a -> Expr a -> Expr Bool
Expressions can be either of type Bool or Int. There are constructors for literals Bool and Num which have the corresponding types. Only Int expressions can be added up (constructor Plus). The condition in the If expression should have type Bool while both branches should have the same type. There is also an equality expression Equal whose operands should have the same type, and the type of the equality expression is Bool.
I have no problems implementing the interpreter eval for this DSL. It compiles and works like a charm:
eval :: Expr a -> a
eval (Num x) = x
eval (Bool x) = x
eval (Plus x y) = eval x + eval y
eval (If c t e) = if eval c then eval t else eval e
eval (Equal x y) = eval x == eval y
However, I struggle to implement an instance of Eq for the DSL. I tried the simple syntactic equality:
instance Eq a => Eq (Expr a) where
Num x == Num y = x == y
Bool x == Bool y = x == y
Plus x y == Plus x' y' = x == x' && y == y'
If c t e == If c' t' e' = c == c' && t == t' && e == e'
Equal x y == Equal x' y' = x == x' && y == y'
_ == _ = False
It does not typecheck (with ghc 8.6.5), the error is the following:
[1 of 1] Compiling Main ( Main.hs, Main.o )
Main.hs:17:35: error:
• Could not deduce: a2 ~ a1
from the context: (a ~ Bool, Eq a1)
bound by a pattern with constructor:
Equal :: forall a. Eq a => Expr a -> Expr a -> Expr Bool,
in an equation for ‘==’
at Main.hs:17:3-11
‘a2’ is a rigid type variable bound by
a pattern with constructor:
Equal :: forall a. Eq a => Expr a -> Expr a -> Expr Bool,
in an equation for ‘==’
at Main.hs:17:16-26
‘a1’ is a rigid type variable bound by
a pattern with constructor:
Equal :: forall a. Eq a => Expr a -> Expr a -> Expr Bool,
in an equation for ‘==’
at Main.hs:17:3-11
Expected type: Expr a1
Actual type: Expr a2
• In the second argument of ‘(==)’, namely ‘x'’
In the first argument of ‘(&&)’, namely ‘x == x'’
In the expression: x == x' && y == y'
• Relevant bindings include
y' :: Expr a2 (bound at Main.hs:17:25)
x' :: Expr a2 (bound at Main.hs:17:22)
y :: Expr a1 (bound at Main.hs:17:11)
x :: Expr a1 (bound at Main.hs:17:9)
|
17 | Equal x y == Equal x' y' = x == x' && y == y'
|
I believe the reason is that the constructor Equal "forgets" the value of the type parameter a of its subexpressions and there is no way for the typechecker to ensure subexpressions x and y both have the same type Expr a.
I tried adding one more type parameter to Expr a to keep track of the type of subexpressions:
data Expr a b where
Num :: Int -> Expr Int b
Bool :: Bool -> Expr Bool b
Plus :: Expr Int b -> Expr Int b -> Expr Int b
If :: Expr Bool b -> Expr a b -> Expr a b -> Expr a b
Equal :: Eq a => Expr a a -> Expr a a -> Expr Bool a
instance Eq a => Eq (Expr a b) where
-- same implementation
eval :: Expr a b -> a
-- same implementation
This approach does not seem scalable to me, once more constructors with subexpressions of different types are added.
All this makes me think that I do use GADTs incorrectly to implement this kind of DSL. Is there a way to implement Eq for this type? If not, what is the idiomatic way to express this kind of type constraint on the expressions?
Complete code:
{-# LANGUAGE GADTs #-}
module Main where
data Expr a where
Num :: Int -> Expr Int
Bool :: Bool -> Expr Bool
Plus :: Expr Int -> Expr Int -> Expr Int
If :: Expr Bool -> Expr a -> Expr a -> Expr a
Equal :: Eq a => Expr a -> Expr a -> Expr Bool
instance Eq a => Eq (Expr a) where
Num x == Num y = x == y
Bool x == Bool y = x == y
Plus x y == Plus x' y' = x == x' && y == y'
If c t e == If c' t' e' = c == c' && t == t' && e == e'
Equal x y == Equal x' y' = x == x' && y == y'
_ == _ = False
eval :: Expr a -> a
eval (Num x) = x
eval (Bool x) = x
eval (Plus x y) = eval x + eval y
eval (If c t e) = if eval c then eval t else eval e
eval (Equal x y) = eval x == eval y
main :: IO ()
main = do
let expr1 = If (Equal (Num 13) (Num 42)) (Bool True) (Bool False)
let expr2 = If (Equal (Num 13) (Num 42)) (Num 42) (Num 777)
print (eval expr1)
print (eval expr2)
print (expr1 == expr1)
