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

Frank Wilson frank at thefixedpoint.me.uk
Mon Sep 22 17:01:53 EDT 2008

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,


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

More information about the Haskell-Cafe mailing list