[Haskell-cafe] Proposal: Sum type branches as extended types (as Type!Constructor)

[Jake McArthur]

On 06/03/2010 10:14 AM, Gabriel Riba wrote:
> No need for runtime errors or exception control
>
>     hd :: List!Cons a ->  a
>
>     hd (Cons x _) = x

This is already doable using GADTs:

     data Z
     data S n

     data List a n where
       Nil :: List a Z
       Cons :: a -> List a n -> List a (S n)

     hd :: List a (S n) -> a
     hd (Cons x _) = x

     tl :: List a (S n) -> List a n
     tl (Cons _ xs) = xs

- Jake