On Mon, Jul 13, 2009 at 10:52 PM, Ashley Yakeley <ashley@semantic.org> 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