On Mon, Sep 15, 2008 at 2:25 PM, Tom Hawkins
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