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
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
