[Haskell-cafe] Re: Comparing GADTs for Eq and Ord
Ryan Ingram
ryani.spam at gmail.com
Mon Sep 15 17:50:30 EDT 2008
On Mon, Sep 15, 2008 at 2:25 PM, Tom Hawkins <tomahawkins at gmail.com> 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
More information about the Haskell-Cafe
mailing list