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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe