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

[Ryan Ingram]

On Mon, Sep 15, 2008 at 2:53 PM, Ganesh Sittampalam <ganesh at earth.li> wrote:
> 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.

You can actually generalize this quite a bit, as I touched on slightly
in my last post:

> data Expr a where
>    Const :: TypeRep a -> a -> Expr a
>    ...

> data TEq a b where Refl :: TEq a a

> data TypeRep a where
>    TInt :: TypeRep Int
>    TBool :: TypeRep Bool
>    TList :: TypeRep a -> TypeRep [a]
>    TArrow :: TypeRep a -> TypeRep b -> TypeRep (a -> b)
>    -- etc.

You can then implement the "cast" used in === in the following way:

> typeEq :: TypeRep a -> TypeRep b -> Maybe (TEq a b)
> typeEq TInt TInt = return Refl
> typeEq TBool TBool = return Refl
> typeEq (TList a) (TList b) = do
>    Refl <- typeEq a b
>    return Refl
> typeEq (TArrow a1 a2) (TArrow b1 b2) = do
>    Refl <- typeEq a1 b1
>    Refl <- typeEq a2 b2
>    return Refl
> -- etc.
> typeEq _ _ = fail "Types do not match"

You can use these to write "cast"

> cast :: TypeRep a -> TypeRep b -> a -> Maybe b
> cast ta tb =
>    case typeEq ta tb of
>        Just Refl -> \a -> Just a
>        _            -> \_ -> Nothing

You need a little more work to support equality; the easiest way is to
have an Eq constraint on Const, but you can also write a function
similar to typeEq that puts an Eq constraint into scope if possible.

Pay special attention to the cases in "typeEq" for TList and TArrow;
they make particular use of the desugaring of patterns in do.  A
desugared version of TList:

> typeEq a0@(TList a) b0@(TList b) =
>    typeEq a b >>= \x ->
>    case x of Refl -> return Refl
>                  _     -> fail "pattern match error"

In the Maybe monad, inlining (>>=), return, and fail, this reduces to
the following:

> case typeEq a b of
>    Nothing -> Nothing
>    Just x -> case x of
>      Refl -> Just Refl
>      _     -> Nothing

When we call typeEq, we have a0 :: TypeRep a0, and b0 :: TypeRep b0,
for some unknown types a0 and b0.

Then the pattern match on TList unifies both of these types with [a1]
and [b1] for some unknown types a1 and b1.  We then call typeEq on a
:: TypeRep a1, and b :: TypeRep b1.

Now, on the right hand side of the "Just x" case, TEq a b has only one
possible value, "Refl", so the failure case won't ever be executed.
However, the pattern match on Refl is important, because it unifies a1
and b1, which allows us to unify [a1] and [b1] and construct Refl ::
TEq [a1] [b1] (which is the same as TEq a0 b0).

    -- ryan