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