[Haskell-cafe] Re: Are GADTs what I need?

[Jason Dagit]

On Mon, Jul 13, 2009 at 10:52 PM, Ashley Yakeley <ashley at 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090714/91430642/attachment.html