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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
