[Haskell-cafe] Re: Are GADTs what I need?

[Ashley Yakeley]

Ryan Ingram wrote:

>> data Type a where
>>    TInt :: Type Int
>>    TBool :: Type Bool
>>    TChar :: Type Char
>>    TList :: Type a -> Type [a]
>>    TFun :: Type a -> Type b -> Type (a -> b)

"Type" here is what I call a simple type witness. Simple type witnesses 
are useful because they can be compared by value, and if they have the 
same value, then they have the same type.

So you can write this:

   data EqualType a b where
     MkEqualType :: EqualType t t

   matchWitness :: Type a -> Type b -> Maybe (EqualType a b)
   matchWitness TInt TInt = Just MkEqualType
   matchWitness TBool TBool = Just MkEqualType
   matchWitness TChar TChar = Just MkEqualType
   matchWitness (TList w1) (TList w2) = do
     MkEqualType <- matchWitness w1 w2
     return MkEqualType
   matchWitness (TFun wa1 wb1) (TFun wa2 wb2) = do
     MkEqualType <- matchWitness wa1 wa2
     MkEqualType <- matchWitness wb1 wb2
     return MkEqualType
   matchWitness _ _ = Nothing

Now whenever you match some value with MkEqualType, the compiler will 
infer the identity of the two types. See my "witness" package:
http://hackage.haskell.org/cgi-bin/hackage-scripts/package/witness

-- 
Ashley Yakeley