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

3 Jun 2010


      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

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

Jake McArthur