[Haskell-cafe] Re: having fun with GADT's

[Frank Wilson]

Someone could probably give a better explanation but I'll give this a  
shot! :)

What you are actually doing is defining a "family" of types. Every  
value in the
type "Nat a" has it's own type. For instance "Z" has type "Nat Z", "(S  
Z)" or "one"
has type "Nat (S Z)",  "(S (S Z))" has type "Nat (S (S Z))" and so on.

In effect types "Z" and "(S a)" defined in those data declarations are  
"marker" types.

It might help you understand if you change the names of the types in  
the data
declarations to something else. It helps not to get confused between
types and constructors ;) .

I hope this was helpful,

Frank

On 22 Sep 2008, at 21:42, Anatoly Yakovenko wrote:

>> data Nat a where
>>   Z :: Nat a
>>   S :: Nat a -> Nat (S a)
>>
>> data Z
>> data S a
>
> I thought I was getting this, but this part is confusing.  What
> exactly does declaring "data Z" do?
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe