[Haskell-cafe] Re: Comparing GADTs for Eq and Ord

[Ashley Yakeley]

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