Tom Hawkins wrote:
data Expr :: * -> * where
Const :: a -> Term a
Equal :: Term a -> Term a -> Term Bool
Your basic problem is this:
p1 :: Term Bool
p1 = Equal (Const 3) (Const 4)
p2 :: Term Bool
p2 = Equal (Const "yes") (Const "no")
p1 and p2 have the same type, but you're not going to be able to compare
them unless you can compare an Int and a String. What do you want p1 ==
p2 to do?
If you want to just say that different types are always non-equal, the
simplest way is to create a witness type for your type-system. For instance:
data MyType a where
IntType :: MyType Int
StringType :: MyType String
Now you'll want to declare MyType as a simple witness:
instance SimpleWitness MyType where
matchWitness IntType IntType = Just MkEqualType
matchWitness StringType StringType = Just MkEqualType
matchWitness _ _ = Nothing
You'll need to include a witness wherever parameter types cannot be
inferred from the type of the object, as well as an Eq dictionary:
data Term :: * -> * where
Const :: a -> Term a
Equal :: Eq a => MyType a -> Term a -> Term a -> Term Bool
Now you can do:
instance Eq a => Eq (Term a) where
(Const p1) == (Const p2) = p1 == p2
(Equal w1 p1 q1) (Equal w2 p2 q2) = case matchWitness w1 w2 of
MkEqualType -> (p1 == p2) && (q1 == q2)
_ -> False -- because the types are different
_ == _ = False
Note: I haven't actually checked this. Use "cabal install witness" to
get SimpleWitness and EqualType.
--
Ashley Yakeley
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
