On Mon, Jul 13, 2009 at 10:52 PM, Ashley Yakeley <[email protected]>wrote:
> 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 Is there any reason to prefer this over: data EqualType a b where MkEqualType :: EqualType a a In the darcs source code we use a definition similar to the one I just gave. I never thought about making the definition like you gave. I wonder if it would have changed things, but I'm not sure what. Your example type checks the same with both versions of EqualType and a type signature is required for matchWitness with both definitions. Playing with the two, I don't really see any way in which they are different. Certainly, both versions of MkEqualType have the same type, but I'm just surprised you don't have to involve a or b in the type of MkEqualType. After playing with both definitions for a bit, I think I see why they have the same type and behave the same way. Initially I was thinking t was an existential type, but because of where it appears it is actually universally quantifed, like the type variable 'a' in my version, so they end up being equivalent. Jason
_______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
