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

[Ryan Ingram]

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