[Haskell-cafe] Re: having fun with GADT's

[Luke Palmer]

On Mon, Sep 22, 2008 at 2:42 PM, Anatoly Yakovenko
<aeyakovenko at gmail.com> 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?

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