[Haskell-cafe] Re: Are GADTs what I need?
Ashley Yakeley
ashley at semantic.org
Tue Jul 14 01:52:26 EDT 2009
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
More information about the Haskell-Cafe
mailing list