On Mon, Sep 22, 2008 at 2:42 PM, Anatoly Yakovenko
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?
Well, in Haskell without closed type families, it's not doing all that much. You could use Int or IO Elephant if you wanted to, as long as its head is not S. But it's documentation, because we're really declaring the dependent type (in pseudohaskell): data Nat = Z | S Nat data Bounded :: Nat -> * where BZ :: Bounded n BS :: Bounded n -> Bounded (S n) So Z and S are the data constructors for Nat, and Bounded *should* only be able to take Nats as arguments. But we cannot express that in Haskell, we just have to be disciplined and never give anything else to Bounded. Luke