[Haskell-cafe] Re: having fun with GADT's
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
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
It might help you understand if you change the names of the types in
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
More information about the Haskell-Cafe