Jason Dagit wrote:

Tom Hawkins wrote:

...

How do I compare a GADT type if a particular constructor returns a concrete type parameter?

For example:

data Expr :: * -> * where Const :: Expr a Equal :: Expr a -> Expr a -> Expr Bool -- If this read Expr a, the compiler has no problem.

instance Eq (Expr a) where Const == Const = True (Equal a b) (Equal x y) = a == x && b == y _ == _ = False

GHC throws:

Couldn't match expected type `a1' against inferred type `a2' `a1' is a rigid type variable bound by the constructor `Equal' at Test.hs:9:3 `a2' is a rigid type variable bound by the constructor `Equal' at Test.hs:9:18 Expected type: Expr a1 Inferred type: Expr a2 In the second argument of `(==)', namely `x' In the first argument of `(&&)', namely `a == x'

I believe I understand the reason for the problem; even though Equal has a type Expr Bool, two Equal expressions could have parameters of different types. But I'm not sure how to get around the problem. Any suggestions?

Equal :: Expr a -> Expr a -> Expr Bool

Makes the type parameter 'a' an existential type. You can think of it like this: data Expr a = Equal (forall a. Expr a Expr a)

I think that forall is in the right place.

You mean data ExprBool = forall a. Equal (Expr a) (Expr a)

This means that when you use the (Equal a b) pattern the 'a' has to be instantiated to some distinct rigid type, and similarly (Equal x y) instantiates 'a' again to some distinct rigid type. This is where your a1 and a2 in the error message come from.

So, in other words, in order to test whether terms constructed with Equal are equal, you have to compare two terms of different type for equality. Well, nothing easier than that: (===) :: Expr a -> Expr b -> Bool Const === Const = True (Equal a b) === (Equal a' b') = a === a' && b === b' _ === _ = False instance Eq (Expr a) where (==) = (===) Chances are that the equality test with different types is more useful in the rest of your program as well. Regards, apfelmus

Take a look at http://www.haskell.org/haskellwiki/GHC/AdvancedOverlap Tom Hawkins wrote:

On Mon, Sep 15, 2008 at 3:11 PM, apfelmus wrote:

...

So, in other words, in order to test whether terms constructed with Equal are equal, you have to compare two terms of different type for equality. Well, nothing easier than that:

(===) :: Expr a -> Expr b -> Bool Const === Const = True (Equal a b) === (Equal a' b') = a === a' && b === b' _ === _ = False

instance Eq (Expr a) where (==) = (===)

OK. But let's modify Expr so that Const carries values of different types:

data Expr :: * -> * where Const :: a -> Term a Equal :: Term a -> Term a -> Term Bool

How would you then define:

Const a === Const b = ...

-Tom _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On Mon, Sep 15, 2008 at 2:50 PM, Ryan Ingram wrote:

There are many papers that talk about using GADTs to reify types in this fashion to allow safe typecasting. They generally all rely on the "base" GADT, "TEq"; every other GADT can be defined in terms of TEq and existential types.

I just found that Tim Sheard has collected a nice list of papers on this subject: http://web.cecs.pdx.edu/~sheard/ Jason

On Mon, 15 Sep 2008, Tom Hawkins wrote:

OK. But let's modify Expr so that Const carries values of different types:

data Expr :: * -> * where Const :: a -> Term a Equal :: Term a -> Term a -> Term Bool

How would you then define:

Const a === Const b = ...

Apart from the suggestions about Data.Typeable etc, one possibility is to enumerate the different possible types that will be used as parameters to Const in different constructors, either in Expr or in a new type. So IntConst :: Int -> Expr Int, etc Or Const :: Const a -> Expr a and IntConst :: Int -> Const Int etc Not very pleasant though. Ganesh

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

Thanks for all the input. It helped me arrive at the following solution. I took the strategy of converting the parameterized type into an unparameterized type which can be easily compared for Eq and Ord. The unparameterized type enumerates the possible Const types with help from an auxiliary type class. -- The primary Expr type. data Expr a where Const :: ExprConst a => a -> Expr a Equal :: Expr a -> Expr a -> Expr Bool -- An "untyped" Expr used to compute Eq and Ord of the former. -- Note each type of constant is enumerated. data UExpr = UConstBool Bool | UConstInt Int | UConstFloat Float | UEqual UExpr UExpr deriving (Eq, Ord) -- A type class to assist in converting Expr to UExpr. class ExprConst a where uexprConst :: a -> UExpr instance ExprConst Bool where uexprConst = UConstBool instance ExprConst Int where uexprConst = UConstInt instance ExprConst Float where uexprConst = UConstFloat -- The conversion function. uexpr :: Expr a -> UExpr uexpr (Const a) = uexprConst a uexpr (Equal a b) = UEqual (uexpr a) (uexpr b) -- Finally the implementation of Eq and Ord for Expr. instance Eq (Expr a) where a == b = uexpr a == uexpr b instance Ord (Expr a) where compare a b = compare (uexpr a) (uexpr b)