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

[Anatoly Yakovenko]

> data Nat a where
>    Z :: Nat a
>    S :: Nat a -> Nat (S a)
>
> data Z
> data S a
>
> n00 = Z
> n01 = S n00
> n02 = S n01
> n03 = S n02
> n04 = S n03
>
> data MaxList t where
>   Nil :: MaxList a
>   Cons :: Nat a -> MaxList a -> MaxList a
>
> a = Cons n02 $ Cons n02 $ Cons n01 $ Nil
> --- ":t a" gives "forall a. MaxList (S (S a))" which tells you exactly
> --- what you want: elements are at least 2.
>
> mlTail :: forall t. MaxList t -> MaxList t
> mlTail (Cons h t) = t

Is there a way to define a function that only takes a list with a max
of 1?  Because

only1 :: MaxList (S a) -> String
only1 _ = "only1"

will work over
> a = Cons n02 $ Cons n02 $ Cons n01 $ Nil
without any problems