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