On Mon, Sep 15, 2008 at 2:25 PM, Tom Hawkins <[EMAIL PROTECTED]> 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 = ...
You can't. But you can do so slightly differently: > import Data.Typeable > > data Expr :: * -> * where > Const :: (Eq a, Typeable a) => a -> Term a > Equal :: Term a -> Term a -> Term Bool > > (===) :: Expr a -> Expr b -> Bool > Const a === Const b = > case cast a of > Nothing -> False > Just a' -> a' == b > Equal l1 r1 === Equal l2 r2 = l1 === l2 && r1 === r2 > _ === _ = False You can also represent Const as follows: > Const :: TypeRep a -> a -> Term a 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. > data TEq :: * -> * -> * where Refl :: TEq a a As an example, here is Expr defined in this fashion: > data Expr a = > (Eq a, Typeable a) => Const a > | forall b. Equal (TEq a Bool) (Expr b) (Expr b) > equal :: Expr a -> Expr a -> Expr Bool > equal = Equal Refl -- ryan _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
