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

Luke Palmer lrpalmer at gmail.com
Mon Sep 22 17:40:25 EDT 2008


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


More information about the Haskell-Cafe mailing list