On Mon, Sep 22, 2008 at 11:10 PM, Anatoly Yakovenko <[EMAIL PROTECTED]> wrote: >> type One = S Z >> type Two = S One >> etc. > > why does: > > data Nat a where > Z :: Nat a > S :: Nat a -> Nat (S a) > > data Z > data S a > > type One = S Z > n00 = Z > n01::One = S n00 > > give me: > > test.hs:10:11: > Couldn't match expected type `One' > against inferred type `Nat (S a)' > In the expression: S n00 > In a pattern binding: n01 :: One = S n00 > Failed, modules loaded: none. > > > or better yet, how is type S Z different from, n01 :: forall a. Nat (S a) >
In short, S Z is a type and n01 is a value. One point that's important to keep in mind is that types and data constructors have disjoint namespaces, so you can have a type Z and a data constructor Z which do not need to have any connection. It may be clearer if we rename the data constructors for Nat. data Z data S n type One = S Z data Nat :: * -> * where Zero :: Nat Z Succ :: Nat n -> Nat (S n) one :: Nat One one = Succ Zero Similarly, One is a type (One :: *) and one is a value (one :: Nat One and Nat One :: *). Note also that Z and S are declared here as empty types, using a common extension. That means there are no (non-bottom) values that have type Z or S a. This means that Z and S are only used as arguments to other type constructors or in class contexts. As long as we're discussing type-level naturals, you may find this old post of mine interesting. <http://www.haskell.org/pipermail/haskell/2005-May/015815.html> -- Dave Menendez <[EMAIL PROTECTED]> <http://www.eyrie.org/~zednenem/> _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe