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

[David Menendez]

On Mon, Sep 22, 2008 at 11:10 PM, Anatoly Yakovenko
<aeyakovenko at gmail.com> 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 <dave at zednenem.com>
<http://www.eyrie.org/~zednenem/>